Metamath Proof Explorer

Theorem ordthmeolem

Description: Lemma for ordthmeo . (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Hypotheses ordthmeo.1 
|- X = dom R
ordthmeo.2 
|- Y = dom S
Assertion ordthmeolem 
|- ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> F e. ( ( ordTop ` R ) Cn ( ordTop ` S ) ) )

Proof

Step Hyp Ref Expression
1 ordthmeo.1 
 |-  X = dom R
2 ordthmeo.2 
 |-  Y = dom S
3 isof1o 
 |-  ( F Isom R , S ( X , Y ) -> F : X -1-1-onto-> Y )
4 3 3ad2ant3 
 |-  ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> F : X -1-1-onto-> Y )
5 f1of 
 |-  ( F : X -1-1-onto-> Y -> F : X --> Y )
6 4 5 syl 
 |-  ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> F : X --> Y )
7 fimacnv 
 |-  ( F : X --> Y -> ( `' F " Y ) = X )
8 6 7 syl 
 |-  ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> ( `' F " Y ) = X )
9 1 ordttopon 
 |-  ( R e. V -> ( ordTop ` R ) e. ( TopOn ` X ) )
10 9 3ad2ant1 
 |-  ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> ( ordTop ` R ) e. ( TopOn ` X ) )
11 toponmax 
 |-  ( ( ordTop ` R ) e. ( TopOn ` X ) -> X e. ( ordTop ` R ) )
12 10 11 syl 
 |-  ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> X e. ( ordTop ` R ) )
13 8 12 eqeltrd 
 |-  ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> ( `' F " Y ) e. ( ordTop ` R ) )
14 elsni 
 |-  ( z e. { Y } -> z = Y )
15 14 imaeq2d 
 |-  ( z e. { Y } -> ( `' F " z ) = ( `' F " Y ) )
16 15 eleq1d 
 |-  ( z e. { Y } -> ( ( `' F " z ) e. ( ordTop ` R ) <-> ( `' F " Y ) e. ( ordTop ` R ) ) )
17 13 16 syl5ibrcom 
 |-  ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> ( z e. { Y } -> ( `' F " z ) e. ( ordTop ` R ) ) )
18 17 ralrimiv 
 |-  ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> A. z e. { Y } ( `' F " z ) e. ( ordTop ` R ) )
19 cnvimass 
 |-  ( `' F " { y e. Y | -. y S x } ) C_ dom F
20 f1odm 
 |-  ( F : X -1-1-onto-> Y -> dom F = X )
21 4 20 syl 
 |-  ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> dom F = X )
22 21 adantr 
 |-  ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) -> dom F = X )
23 19 22 sseqtrid 
 |-  ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) -> ( `' F " { y e. Y | -. y S x } ) C_ X )
24 sseqin2 
 |-  ( ( `' 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 } ) )
25 23 24 sylib 
 |-  ( ( ( 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 } ) )
26 4 ad2antrr 
 |-  ( ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) /\ z e. X ) -> F : X -1-1-onto-> Y )
27 f1ofn 
 |-  ( F : X -1-1-onto-> Y -> F Fn X )
28 26 27 syl 
 |-  ( ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) /\ z e. X ) -> F Fn X )
29 elpreima 
 |-  ( F Fn X -> ( z e. ( `' F " { y e. Y | -. y S x } ) <-> ( z e. X /\ ( F ` z ) e. { y e. Y | -. y S x } ) ) )
30 28 29 syl 
 |-  ( ( ( ( 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 } ) ) )
31 simpr 
 |-  ( ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) /\ z e. X ) -> z e. X )
32 31 biantrurd 
 |-  ( ( ( ( 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 } ) ) )
33 6 adantr 
 |-  ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) -> F : X --> Y )
34 33 ffvelrnda 
 |-  ( ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) /\ z e. X ) -> ( F ` z ) e. Y )
35 breq1 
 |-  ( y = ( F ` z ) -> ( y S x <-> ( F ` z ) S x ) )
36 35 notbid 
 |-  ( y = ( F ` z ) -> ( -. y S x <-> -. ( F ` z ) S x ) )
37 36 elrab3 
 |-  ( ( F ` z ) e. Y -> ( ( F ` z ) e. { y e. Y | -. y S x } <-> -. ( F ` z ) S x ) )
38 34 37 syl 
 |-  ( ( ( ( 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 ) )
39 simpll3 
 |-  ( ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) /\ z e. X ) -> F Isom R , S ( X , Y ) )
40 f1ocnv 
 |-  ( F : X -1-1-onto-> Y -> `' F : Y -1-1-onto-> X )
41 f1of 
 |-  ( `' F : Y -1-1-onto-> X -> `' F : Y --> X )
42 4 40 41 3syl 
 |-  ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> `' F : Y --> X )
43 42 ffvelrnda 
 |-  ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) -> ( `' F ` x ) e. X )
44 43 adantr 
 |-  ( ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) /\ z e. X ) -> ( `' F ` x ) e. X )
45 isorel 
 |-  ( ( F Isom R , S ( X , Y ) /\ ( z e. X /\ ( `' F ` x ) e. X ) ) -> ( z R ( `' F ` x ) <-> ( F ` z ) S ( F ` ( `' F ` x ) ) ) )
46 39 31 44 45 syl12anc 
 |-  ( ( ( ( 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 ) ) ) )
47 f1ocnvfv2 
 |-  ( ( F : X -1-1-onto-> Y /\ x e. Y ) -> ( F ` ( `' F ` x ) ) = x )
48 4 47 sylan 
 |-  ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) -> ( F ` ( `' F ` x ) ) = x )
49 48 adantr 
 |-  ( ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) /\ z e. X ) -> ( F ` ( `' F ` x ) ) = x )
50 49 breq2d 
 |-  ( ( ( ( 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 ) )
51 46 50 bitrd 
 |-  ( ( ( ( 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 ) )
52 51 notbid 
 |-  ( ( ( ( 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 ) )
53 38 52 bitr4d 
 |-  ( ( ( ( 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 ) ) )
54 30 32 53 3bitr2d 
 |-  ( ( ( ( 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 ) ) )
55 54 rabbi2dva 
 |-  ( ( ( 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 ) } )
56 25 55 eqtr3d 
 |-  ( ( ( 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 ) } )
57 simpl1 
 |-  ( ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) /\ x e. Y ) -> R e. V )
58 1 ordtopn1 
 |-  ( ( R e. V /\ ( `' F ` x ) e. X ) -> { z e. X | -. z R ( `' F ` x ) } e. ( ordTop ` R ) )
59 57 43 58 syl2anc 
 |-  ( ( ( 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 ) )
60 56 59 eqeltrd 
 |-  ( ( ( 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 ) )
61 60 ralrimiva 
 |-  ( ( 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 ) )
62 dmexg 
 |-  ( S e. W -> dom S e. _V )
63 2 62 eqeltrid 
 |-  ( S e. W -> Y e. _V )
64 63 3ad2ant2 
 |-  ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> Y e. _V )
65 rabexg 
 |-  ( Y e. _V -> { y e. Y | -. y S x } e. _V )
66 64 65 syl 
 |-  ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> { y e. Y | -. y S x } e. _V )
67 66 ralrimivw 
 |-  ( ( 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 
 |-  ( x e. Y |-> { y e. Y | -. y S x } ) = ( x e. Y |-> { y e. Y | -. y S x } )
69 imaeq2 
 |-  ( z = { y e. Y | -. y S x } -> ( `' F " z ) = ( `' F " { y e. Y | -. y S x } ) )
70 69 eleq1d 
 |-  ( z = { y e. Y | -. y S x } -> ( ( `' F " z ) e. ( ordTop ` R ) <-> ( `' F " { y e. Y | -. y S x } ) e. ( ordTop ` R ) ) )
71 68 70 ralrnmptw 
 |-  ( 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 ) ) )
72 67 71 syl 
 |-  ( ( 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 ) ) )
73 61 72 mpbird 
 |-  ( ( 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 
 |-  ( `' F " { y e. Y | -. x S y } ) C_ dom F
75 74 22 sseqtrid 
 |-  ( ( ( 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 
 |-  ( ( `' 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 } ) )
77 75 76 sylib 
 |-  ( ( ( 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 
 |-  ( F Fn X -> ( z e. ( `' F " { y e. Y | -. x S y } ) <-> ( z e. X /\ ( F ` z ) e. { y e. Y | -. x S y } ) ) )
79 28 78 syl 
 |-  ( ( ( ( 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 } ) ) )
80 31 biantrurd 
 |-  ( ( ( ( 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 
 |-  ( y = ( F ` z ) -> ( x S y <-> x S ( F ` z ) ) )
82 81 notbid 
 |-  ( y = ( F ` z ) -> ( -. x S y <-> -. x S ( F ` z ) ) )
83 82 elrab3 
 |-  ( ( F ` z ) e. Y -> ( ( F ` z ) e. { y e. Y | -. x S y } <-> -. x S ( F ` z ) ) )
84 34 83 syl 
 |-  ( ( ( ( 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 
 |-  ( ( F Isom R , S ( X , Y ) /\ ( ( `' F ` x ) e. X /\ z e. X ) ) -> ( ( `' F ` x ) R z <-> ( F ` ( `' F ` x ) ) S ( F ` z ) ) )
86 39 44 31 85 syl12anc 
 |-  ( ( ( ( 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 ) ) )
87 49 breq1d 
 |-  ( ( ( ( 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 ) ) )
88 86 87 bitrd 
 |-  ( ( ( ( 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 ) ) )
89 88 notbid 
 |-  ( ( ( ( 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 ) ) )
90 84 89 bitr4d 
 |-  ( ( ( ( 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 ) )
91 79 80 90 3bitr2d 
 |-  ( ( ( ( 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 ) )
92 91 rabbi2dva 
 |-  ( ( ( 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 } )
93 77 92 eqtr3d 
 |-  ( ( ( 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 } )
94 1 ordtopn2 
 |-  ( ( R e. V /\ ( `' F ` x ) e. X ) -> { z e. X | -. ( `' F ` x ) R z } e. ( ordTop ` R ) )
95 57 43 94 syl2anc 
 |-  ( ( ( 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 ) )
96 93 95 eqeltrd 
 |-  ( ( ( 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 ) )
97 96 ralrimiva 
 |-  ( ( 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 
 |-  ( Y e. _V -> { y e. Y | -. x S y } e. _V )
99 64 98 syl 
 |-  ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> { y e. Y | -. x S y } e. _V )
100 99 ralrimivw 
 |-  ( ( 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 
 |-  ( x e. Y |-> { y e. Y | -. x S y } ) = ( x e. Y |-> { y e. Y | -. x S y } )
102 imaeq2 
 |-  ( z = { y e. Y | -. x S y } -> ( `' F " z ) = ( `' F " { y e. Y | -. x S y } ) )
103 102 eleq1d 
 |-  ( z = { y e. Y | -. x S y } -> ( ( `' F " z ) e. ( ordTop ` R ) <-> ( `' F " { y e. Y | -. x S y } ) e. ( ordTop ` R ) ) )
104 101 103 ralrnmptw 
 |-  ( 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 ) ) )
105 100 104 syl 
 |-  ( ( 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 ) ) )
106 97 105 mpbird 
 |-  ( ( 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 
 |-  ( 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 ) ) )
108 73 106 107 sylanbrc 
 |-  ( ( 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 
 |-  ( 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 ) ) )
110 18 108 109 sylanbrc 
 |-  ( ( 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 
 |-  ran ( x e. Y |-> { y e. Y | -. y S x } ) = ran ( x e. Y |-> { y e. Y | -. y S x } )
112 eqid 
 |-  ran ( x e. Y |-> { y e. Y | -. x S y } ) = ran ( x e. Y |-> { y e. Y | -. x S y } )
113 2 111 112 ordtuni 
 |-  ( 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 } ) ) ) )
114 113 63 eqeltrrd 
 |-  ( 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 
 |-  ( ( { 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 )
116 114 115 sylibr 
 |-  ( 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 )
117 116 3ad2ant2 
 |-  ( ( 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 )
118 2 111 112 ordtval 
 |-  ( 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 } ) ) ) ) ) )
119 118 3ad2ant2 
 |-  ( ( 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 } ) ) ) ) ) )
120 2 ordttopon 
 |-  ( S e. W -> ( ordTop ` S ) e. ( TopOn ` Y ) )
121 120 3ad2ant2 
 |-  ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> ( ordTop ` S ) e. ( TopOn ` Y ) )
122 10 117 119 121 subbascn 
 |-  ( ( 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 ) ) ) )
123 6 110 122 mpbir2and 
 |-  ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> F e. ( ( ordTop ` R ) Cn ( ordTop ` S ) ) )