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 )`
` |-  ( ( 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 ) )`
` |-  ( ( 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 )`
` |-  ( ( ( 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 } ) )`
` |-  ( ( ( ( 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 } ) ) )`
` |-  ( ( ( 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 )`
` |-  ( ( ( ( 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 )`
` |-  ( ( ( ( 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 )`
` |-  ( ( 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 )`
` |-  ( ( 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 )`
` |-  ( 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 } ) ) ) ) ) )`
` |-  ( ( 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 } ) ) ) ) ) )`
` |-  ( S e. W -> ( ordTop ` S ) e. ( TopOn ` Y ) )`
` |-  ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> ( ordTop ` S ) e. ( TopOn ` Y ) )`
` |-  ( ( 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 ) ) ) )`
` |-  ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> F e. ( ( ordTop ` R ) Cn ( ordTop ` S ) ) )`