MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ordthmeolem Structured version   Visualization version   Unicode version
Theorem ordthmeolem 21604
Description: Lemma for ordthmeo 21605. (Contributed by Mario Carneiro, 9-Sep-2015.)
Hypotheses
Ref Expression
ordthmeo.1 |- X = dom R
ordthmeo.2 |- Y = dom S
Assertion
Ref Expression
ordthmeolem |- ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> F e. ( (ordTop ` R ) Cn (ordTop ` S ) ) )
Proof of Theorem ordthmeolem
Dummy variables x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isof1o 6573 . . . 4 |- ( F Isom R , S ( X , Y ) -> F : X -1-1-onto-> Y )
213ad2ant3 1084 . . 3 |- ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> F : X -1-1-onto-> Y )
3 f1of 6137 . . 3 |- ( F : X -1-1-onto-> Y -> F : X --> Y )
42, 3syl 17 . 2 |- ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> F : X --> Y )
5 fimacnv 6347 . . . . . . 7 |- ( F : X --> Y -> ( `' F " Y ) = X )
64, 5syl 17 . . . . . 6 |- ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> ( `' F " Y ) = X )
7 ordthmeo.1 . . . . . . . . 9 |- X = dom R
87ordttopon 20997 . . . . . . . 8 |- ( R e. V -> (ordTop ` R ) e. (TopOn ` X ) )
983ad2ant1 1082 . . . . . . 7 |- ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> (ordTop ` R ) e. (TopOn ` X ) )
10 toponmax 20730 . . . . . . 7 |- ( (ordTop ` R ) e. (TopOn ` X ) -> X e. (ordTop ` R ) )
119, 10syl 17 . . . . . 6 |- ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> X e. (ordTop ` R ) )
126, 11eqeltrd 2701 . . . . 5 |- ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> ( `' F " Y ) e. (ordTop ` R ) )
13 elsni 4194 . . . . . . 7 |- ( z e. { Y } -> z = Y )
1413imaeq2d 5466 . . . . . 6 |- ( z e. { Y } -> ( `' F " z ) = ( `' F " Y ) )
1514eleq1d 2686 . . . . 5 |- ( z e. { Y } -> ( ( `' F " z ) e. (ordTop ` R ) <-> ( `' F " Y ) e. (ordTop ` R ) ) )
1612, 15syl5ibrcom 237 . . . 4 |- ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> ( z e. { Y } -> ( `' F " z ) e. (ordTop ` R ) ) )
1716ralrimiv 2965 . . 3 |- ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> A. z e. { Y } ( `' F " z ) e. (ordTop ` R ) )
18 cnvimass 5485 . . . . . . . . . 10 |- ( `' F " { y e. Y | -. y S x } ) C_ dom F
19 f1odm 6141 . . . . . . . . . . . 12 |- ( F : X -1-1-onto-> Y -> dom F = X )
202, 19syl 17 . . . . . . . . . . 11 |- ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> dom F = X )
2120adantr 481 . . . . . . . . . 10 |- ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) -> dom F = X )
2218, 21syl5sseq 3653 . . . . . . . . 9 |- ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) -> ( `' F " { y e. Y | -. y S x } ) C_ X )
23 sseqin2 3817 . . . . . . . . 9 |- ( ( `' F " { y e. Y | -. y S x } ) C_ X <-> ( X i^i ( `' F " { y e. Y | -. y S x } ) ) = ( `' F " { y e. Y | -. y S x } ) )
2422, 23sylib 208 . . . . . . . 8 |- ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) -> ( X i^i ( `' F " { y e. Y | -. y S x } ) ) = ( `' F " { y e. Y | -. y S x } ) )
252ad2antrr 762 . . . . . . . . . . . 12 |- ( ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) /\ z e. X ) -> F : X -1-1-onto-> Y )
26 f1ofn 6138 . . . . . . . . . . . 12 |- ( F : X -1-1-onto-> Y -> F Fn X )
2725, 26syl 17 . . . . . . . . . . 11 |- ( ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) /\ z e. X ) -> F Fn X )
28 elpreima 6337 . . . . . . . . . . 11 |- ( F Fn X -> ( z e. ( `' F " { y e. Y | -. y S x } ) <-> ( z e. X /\ ( F ` z ) e. { y e. Y | -. y S x } ) ) )
2927, 28syl 17 . . . . . . . . . 10 |- ( ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) /\ z e. X ) -> ( z e. ( `' F " { y e. Y | -. y S x } ) <-> ( z e. X /\ ( F ` z ) e. { y e. Y | -. y S x } ) ) )
30 simpr 477 . . . . . . . . . . 11 |- ( ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) /\ z e. X ) -> z e. X )
3130biantrurd 529 . . . . . . . . . 10 |- ( ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) /\ z e. X ) -> ( ( F ` z ) e. { y e. Y | -. y S x } <-> ( z e. X /\ ( F ` z ) e. { y e. Y | -. y S x } ) ) )
324adantr 481 . . . . . . . . . . . . 13 |- ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) -> F : X --> Y )
3332ffvelrnda 6359 . . . . . . . . . . . 12 |- ( ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) /\ z e. X ) -> ( F ` z ) e. Y )
34 breq1 4656 . . . . . . . . . . . . . 14 |- ( y = ( F ` z ) -> ( y S x <-> ( F ` z ) S x ) )
3534notbid 308 . . . . . . . . . . . . 13 |- ( y = ( F ` z ) -> ( -. y S x <-> -. ( F ` z ) S x ) )
3635elrab3 3364 . . . . . . . . . . . 12 |- ( ( F ` z ) e. Y -> ( ( F ` z ) e. { y e. Y | -. y S x } <-> -. ( F ` z ) S x ) )
3733, 36syl 17 . . . . . . . . . . 11 |- ( ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) /\ z e. X ) -> ( ( F ` z ) e. { y e. Y | -. y S x } <-> -. ( F ` z ) S x ) )
38 simpll3 1102 . . . . . . . . . . . . . 14 |- ( ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) /\ z e. X ) -> F Isom R , S ( X , Y ) )
39 f1ocnv 6149 . . . . . . . . . . . . . . . . 17 |- ( F : X -1-1-onto-> Y -> `' F : Y -1-1-onto-> X )
40 f1of 6137 . . . . . . . . . . . . . . . . 17 |- ( `' F : Y -1-1-onto-> X -> `' F : Y --> X )
412, 39, 403syl 18 . . . . . . . . . . . . . . . 16 |- ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> `' F : Y --> X )
4241ffvelrnda 6359 . . . . . . . . . . . . . . 15 |- ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) -> ( `' F ` x ) e. X )
4342adantr 481 . . . . . . . . . . . . . 14 |- ( ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) /\ z e. X ) -> ( `' F ` x ) e. X )
44 isorel 6576 . . . . . . . . . . . . . 14 |- ( ( F Isom R , S ( X , Y ) /\ ( z e. X /\ ( `' F ` x ) e. X ) ) -> ( z R ( `' F ` x ) <-> ( F ` z ) S ( F ` ( `' F ` x ) ) ) )
4538, 30, 43, 44syl12anc 1324 . . . . . . . . . . . . 13 |- ( ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) /\ z e. X ) -> ( z R ( `' F ` x ) <-> ( F ` z ) S ( F ` ( `' F ` x ) ) ) )
46 f1ocnvfv2 6533 . . . . . . . . . . . . . . . 16 |- ( ( F : X -1-1-onto-> Y /\ x e. Y ) -> ( F ` ( `' F ` x ) ) = x )
472, 46sylan 488 . . . . . . . . . . . . . . 15 |- ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) -> ( F ` ( `' F ` x ) ) = x )
4847adantr 481 . . . . . . . . . . . . . 14 |- ( ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) /\ z e. X ) -> ( F ` ( `' F ` x ) ) = x )
4948breq2d 4665 . . . . . . . . . . . . 13 |- ( ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) /\ z e. X ) -> ( ( F ` z ) S ( F ` ( `' F ` x ) ) <-> ( F ` z ) S x ) )
5045, 49bitrd 268 . . . . . . . . . . . 12 |- ( ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) /\ z e. X ) -> ( z R ( `' F ` x ) <-> ( F ` z ) S x ) )
5150notbid 308 . . . . . . . . . . 11 |- ( ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) /\ z e. X ) -> ( -. z R ( `' F ` x ) <-> -. ( F ` z ) S x ) )
5237, 51bitr4d 271 . . . . . . . . . 10 |- ( ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) /\ z e. X ) -> ( ( F ` z ) e. { y e. Y | -. y S x } <-> -. z R ( `' F ` x ) ) )
5329, 31, 523bitr2d 296 . . . . . . . . 9 |- ( ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) /\ z e. X ) -> ( z e. ( `' F " { y e. Y | -. y S x } ) <-> -. z R ( `' F ` x ) ) )
5453rabbi2dva 3821 . . . . . . . 8 |- ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) -> ( X i^i ( `' F " { y e. Y | -. y S x } ) ) = { z e. X | -. z R ( `' F ` x ) } )
5524, 54eqtr3d 2658 . . . . . . 7 |- ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) -> ( `' F " { y e. Y | -. y S x } ) = { z e. X | -. z R ( `' F ` x ) } )
56 simpl1 1064 . . . . . . . 8 |- ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) -> R e. V )
577ordtopn1 20998 . . . . . . . 8 |- ( ( R e. V /\ ( `' F ` x ) e. X ) -> { z e. X | -. z R ( `' F ` x ) } e. (ordTop ` R ) )
5856, 42, 57syl2anc 693 . . . . . . 7 |- ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) -> { z e. X | -. z R ( `' F ` x ) } e. (ordTop ` R ) )
5955, 58eqeltrd 2701 . . . . . 6 |- ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) -> ( `' F " { y e. Y | -. y S x } ) e. (ordTop ` R ) )
6059ralrimiva 2966 . . . . 5 |- ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> A. x e. Y ( `' F " { y e. Y | -. y S x } ) e. (ordTop ` R ) )
61 ordthmeo.2 . . . . . . . . . 10 |- Y = dom S
62 dmexg 7097 . . . . . . . . . 10 |- ( S e. W -> dom S e. _V )
6361, 62syl5eqel 2705 . . . . . . . . 9 |- ( S e. W -> Y e. _V )
64633ad2ant2 1083 . . . . . . . 8 |- ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> Y e. _V )
65 rabexg 4812 . . . . . . . 8 |- ( Y e. _V -> { y e. Y | -. y S x } e. _V )
6664, 65syl 17 . . . . . . 7 |- ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> { y e. Y | -. y S x } e. _V )
6766ralrimivw 2967 . . . . . 6 |- ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> A. x e. Y { y e. Y | -. y S x } e. _V )
68 eqid 2622 . . . . . . 7 |- ( x e. Y |-> { y e. Y | -. y S x } ) = ( x e. Y |-> { y e. Y | -. y S x } )
69 imaeq2 5462 . . . . . . . 8 |- ( z = { y e. Y | -. y S x } -> ( `' F " z ) = ( `' F " { y e. Y | -. y S x } ) )
7069eleq1d 2686 . . . . . . 7 |- ( z = { y e. Y | -. y S x } -> ( ( `' F " z ) e. (ordTop ` R ) <-> ( `' F " { y e. Y | -. y S x } ) e. (ordTop ` R ) ) )
7168, 70ralrnmpt 6368 . . . . . 6 |- ( A. x e. Y { y e. Y | -. y S x } e. _V -> ( A. z e. ran ( x e. Y |-> { y e. Y | -. y S x } ) ( `' F " z ) e. (ordTop ` R ) <-> A. x e. Y ( `' F " { y e. Y | -. y S x } ) e. (ordTop ` R ) ) )
7267, 71syl 17 . . . . 5 |- ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> ( A. z e. ran ( x e. Y |-> { y e. Y | -. y S x } ) ( `' F " z ) e. (ordTop ` R ) <-> A. x e. Y ( `' F " { y e. Y | -. y S x } ) e. (ordTop ` R ) ) )
7360, 72mpbird 247 . . . 4 |- ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> A. z e. ran ( x e. Y |-> { y e. Y | -. y S x } ) ( `' F " z ) e. (ordTop ` R ) )
74 cnvimass 5485 . . . . . . . . . 10 |- ( `' F " { y e. Y | -. x S y } ) C_ dom F
7574, 21syl5sseq 3653 . . . . . . . . 9 |- ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) -> ( `' F " { y e. Y | -. x S y } ) C_ X )
76 sseqin2 3817 . . . . . . . . 9 |- ( ( `' F " { y e. Y | -. x S y } ) C_ X <-> ( X i^i ( `' F " { y e. Y | -. x S y } ) ) = ( `' F " { y e. Y | -. x S y } ) )
7775, 76sylib 208 . . . . . . . 8 |- ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) -> ( X i^i ( `' F " { y e. Y | -. x S y } ) ) = ( `' F " { y e. Y | -. x S y } ) )
78 elpreima 6337 . . . . . . . . . . 11 |- ( F Fn X -> ( z e. ( `' F " { y e. Y | -. x S y } ) <-> ( z e. X /\ ( F ` z ) e. { y e. Y | -. x S y } ) ) )
7927, 78syl 17 . . . . . . . . . 10 |- ( ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) /\ z e. X ) -> ( z e. ( `' F " { y e. Y | -. x S y } ) <-> ( z e. X /\ ( F ` z ) e. { y e. Y | -. x S y } ) ) )
8030biantrurd 529 . . . . . . . . . 10 |- ( ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) /\ z e. X ) -> ( ( F ` z ) e. { y e. Y | -. x S y } <-> ( z e. X /\ ( F ` z ) e. { y e. Y | -. x S y } ) ) )
81 breq2 4657 . . . . . . . . . . . . . 14 |- ( y = ( F ` z ) -> ( x S y <-> x S ( F ` z ) ) )
8281notbid 308 . . . . . . . . . . . . 13 |- ( y = ( F ` z ) -> ( -. x S y <-> -. x S ( F ` z ) ) )
8382elrab3 3364 . . . . . . . . . . . 12 |- ( ( F ` z ) e. Y -> ( ( F ` z ) e. { y e. Y | -. x S y } <-> -. x S ( F ` z ) ) )
8433, 83syl 17 . . . . . . . . . . 11 |- ( ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) /\ z e. X ) -> ( ( F ` z ) e. { y e. Y | -. x S y } <-> -. x S ( F ` z ) ) )
85 isorel 6576 . . . . . . . . . . . . . 14 |- ( ( F Isom R , S ( X , Y ) /\ ( ( `' F ` x ) e. X /\ z e. X ) ) -> ( ( `' F ` x ) R z <-> ( F ` ( `' F ` x ) ) S ( F ` z ) ) )
8638, 43, 30, 85syl12anc 1324 . . . . . . . . . . . . 13 |- ( ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) /\ z e. X ) -> ( ( `' F ` x ) R z <-> ( F ` ( `' F ` x ) ) S ( F ` z ) ) )
8748breq1d 4663 . . . . . . . . . . . . 13 |- ( ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) /\ z e. X ) -> ( ( F ` ( `' F ` x ) ) S ( F ` z ) <-> x S ( F ` z ) ) )
8886, 87bitrd 268 . . . . . . . . . . . 12 |- ( ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) /\ z e. X ) -> ( ( `' F ` x ) R z <-> x S ( F ` z ) ) )
8988notbid 308 . . . . . . . . . . 11 |- ( ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) /\ z e. X ) -> ( -. ( `' F ` x ) R z <-> -. x S ( F ` z ) ) )
9084, 89bitr4d 271 . . . . . . . . . 10 |- ( ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) /\ z e. X ) -> ( ( F ` z ) e. { y e. Y | -. x S y } <-> -. ( `' F ` x ) R z ) )
9179, 80, 903bitr2d 296 . . . . . . . . 9 |- ( ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) /\ z e. X ) -> ( z e. ( `' F " { y e. Y | -. x S y } ) <-> -. ( `' F ` x ) R z ) )
9291rabbi2dva 3821 . . . . . . . 8 |- ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) -> ( X i^i ( `' F " { y e. Y | -. x S y } ) ) = { z e. X | -. ( `' F ` x ) R z } )
9377, 92eqtr3d 2658 . . . . . . 7 |- ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) -> ( `' F " { y e. Y | -. x S y } ) = { z e. X | -. ( `' F ` x ) R z } )
947ordtopn2 20999 . . . . . . . 8 |- ( ( R e. V /\ ( `' F ` x ) e. X ) -> { z e. X | -. ( `' F ` x ) R z } e. (ordTop ` R ) )
9556, 42, 94syl2anc 693 . . . . . . 7 |- ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) -> { z e. X | -. ( `' F ` x ) R z } e. (ordTop ` R ) )
9693, 95eqeltrd 2701 . . . . . 6 |- ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) -> ( `' F " { y e. Y | -. x S y } ) e. (ordTop ` R ) )
9796ralrimiva 2966 . . . . 5 |- ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> A. x e. Y ( `' F " { y e. Y | -. x S y } ) e. (ordTop ` R ) )
98 rabexg 4812 . . . . . . . 8 |- ( Y e. _V -> { y e. Y | -. x S y } e. _V )
9964, 98syl 17 . . . . . . 7 |- ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> { y e. Y | -. x S y } e. _V )
10099ralrimivw 2967 . . . . . 6 |- ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> A. x e. Y { y e. Y | -. x S y } e. _V )
101 eqid 2622 . . . . . . 7 |- ( x e. Y |-> { y e. Y | -. x S y } ) = ( x e. Y |-> { y e. Y | -. x S y } )
102 imaeq2 5462 . . . . . . . 8 |- ( z = { y e. Y | -. x S y } -> ( `' F " z ) = ( `' F " { y e. Y | -. x S y } ) )
103102eleq1d 2686 . . . . . . 7 |- ( z = { y e. Y | -. x S y } -> ( ( `' F " z ) e. (ordTop ` R ) <-> ( `' F " { y e. Y | -. x S y } ) e. (ordTop ` R ) ) )
104101, 103ralrnmpt 6368 . . . . . 6 |- ( A. x e. Y { y e. Y | -. x S y } e. _V -> ( A. z e. ran ( x e. Y |-> { y e. Y | -. x S y } ) ( `' F " z ) e. (ordTop ` R ) <-> A. x e. Y ( `' F " { y e. Y | -. x S y } ) e. (ordTop ` R ) ) )
105100, 104syl 17 . . . . 5 |- ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> ( A. z e. ran ( x e. Y |-> { y e. Y | -. x S y } ) ( `' F " z ) e. (ordTop ` R ) <-> A. x e. Y ( `' F " { y e. Y | -. x S y } ) e. (ordTop ` R ) ) )
10697, 105mpbird 247 . . . 4 |- ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> A. z e. ran ( x e. Y |-> { y e. Y | -. x S y } ) ( `' F " z ) e. (ordTop ` R ) )
107 ralunb 3794 . . . 4 |- ( A. z e. ( ran ( x e. Y |-> { y e. Y | -. y S x } ) u. ran ( x e. Y |-> { y e. Y | -. x S y } ) ) ( `' F " z ) e. (ordTop ` R ) <-> ( A. z e. ran ( x e. Y |-> { y e. Y | -. y S x } ) ( `' F " z ) e. (ordTop ` R ) /\ A. z e. ran ( x e. Y |-> { y e. Y | -. x S y } ) ( `' F " z ) e. (ordTop ` R ) ) )
10873, 106, 107sylanbrc 698 . . 3 |- ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> A. z e. ( ran ( x e. Y |-> { y e. Y | -. y S x } ) u. ran ( x e. Y |-> { y e. Y | -. x S y } ) ) ( `' F " z ) e. (ordTop ` R ) )
109 ralunb 3794 . . 3 |- ( A. z e. ( { Y } u. ( ran ( x e. Y |-> { y e. Y | -. y S x } ) u. ran ( x e. Y |-> { y e. Y | -. x S y } ) ) ) ( `' F " z ) e. (ordTop ` R ) <-> ( A. z e. { Y } ( `' F " z ) e. (ordTop ` R ) /\ A. z e. ( ran ( x e. Y |-> { y e. Y | -. y S x } ) u. ran ( x e. Y |-> { y e. Y | -. x S y } ) ) ( `' F " z ) e. (ordTop ` R ) ) )
11017, 108, 109sylanbrc 698 . 2 |- ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> A. z e. ( { Y } u. ( ran ( x e. Y |-> { y e. Y | -. y S x } ) u. ran ( x e. Y |-> { y e. Y | -. x S y } ) ) ) ( `' F " z ) e. (ordTop ` R ) )
111 eqid 2622 . . . . . . 7 |- ran ( x e. Y |-> { y e. Y | -. y S x } ) = ran ( x e. Y |-> { y e. Y | -. y S x } )
112 eqid 2622 . . . . . . 7 |- ran ( x e. Y |-> { y e. Y | -. x S y } ) = ran ( x e. Y |-> { y e. Y | -. x S y } )
11361, 111, 112ordtuni 20994 . . . . . 6 |- ( S e. W -> Y = U. ( { Y } u. ( ran ( x e. Y |-> { y e. Y | -. y S x } ) u. ran ( x e. Y |-> { y e. Y | -. x S y } ) ) ) )
114113, 63eqeltrrd 2702 . . . . 5 |- ( S e. W -> U. ( { Y } u. ( ran ( x e. Y |-> { y e. Y | -. y S x } ) u. ran ( x e. Y |-> { y e. Y | -. x S y } ) ) ) e. _V )
115 uniexb 6973 . . . . 5 |- ( ( { Y } u. ( ran ( x e. Y |-> { y e. Y | -. y S x } ) u. ran ( x e. Y |-> { y e. Y | -. x S y } ) ) ) e. _V <-> U. ( { Y } u. ( ran ( x e. Y |-> { y e. Y | -. y S x } ) u. ran ( x e. Y |-> { y e. Y | -. x S y } ) ) ) e. _V )
116114, 115sylibr 224 . . . 4 |- ( S e. W -> ( { Y } u. ( ran ( x e. Y |-> { y e. Y | -. y S x } ) u. ran ( x e. Y |-> { y e. Y | -. x S y } ) ) ) e. _V )
1171163ad2ant2 1083 . . 3 |- ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> ( { Y } u. ( ran ( x e. Y |-> { y e. Y | -. y S x } ) u. ran ( x e. Y |-> { y e. Y | -. x S y } ) ) ) e. _V )
11861, 111, 112ordtval 20993 . . . 4 |- ( S e. W -> (ordTop ` S ) = ( topGen ` ( fi ` ( { Y } u. ( ran ( x e. Y |-> { y e. Y | -. y S x } ) u. ran ( x e. Y |-> { y e. Y | -. x S y } ) ) ) ) ) )
1191183ad2ant2 1083 . . 3 |- ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> (ordTop ` S ) = ( topGen ` ( fi ` ( { Y } u. ( ran ( x e. Y |-> { y e. Y | -. y S x } ) u. ran ( x e. Y |-> { y e. Y | -. x S y } ) ) ) ) ) )
12061ordttopon 20997 . . . 4 |- ( S e. W -> (ordTop ` S ) e. (TopOn ` Y ) )
1211203ad2ant2 1083 . . 3 |- ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> (ordTop ` S ) e. (TopOn ` Y ) )
1229, 117, 119, 121subbascn 21058 . 2 |- ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> ( F e. ( (ordTop ` R ) Cn (ordTop ` S ) ) <-> ( F : X --> Y /\ A. z e. ( { Y } u. ( ran ( x e. Y |-> { y e. Y | -. y S x } ) u. ran ( x e. Y |-> { y e. Y | -. x S y } ) ) ) ( `' F " z ) e. (ordTop ` R ) ) ) )
1234, 110, 122mpbir2and 957 1 |- ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> F e. ( (ordTop ` R ) Cn (ordTop ` S ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   A.wral 2912   {crab 2916   _Vcvv 3200   u. cun 3572   i^i cin 3573   C_ wss 3574   {csn 4177   U.cuni 4436   class class class wbr 4653   |-> cmpt 4729   `'ccnv 5113   dom cdm 5114   ran crn 5115   "cima 5117   Fn wfn 5883   -->wf 5884   -1-1-onto->wf1o 5887   ` cfv 5888   Isom wiso 5889  (class class class)co 6650   ficfi 8316   topGenctg 16098  ordTopcordt 16159  TopOnctopon 20715   Cn ccn 21028
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-fin 7959  df-fi 8317  df-topgen 16104  df-ordt 16161  df-top 20699  df-topon 20716  df-bases 20750  df-cn 21031
This theorem is referenced by:  ordthmeo  21605  xrmulc1cn  29976
  Copyright terms: Public domain W3C validator