Metamath Proof Explorer

Theorem ordtrest2NEW

Description: An interval-closed set A in a total order has the same subspace topology as the restricted order topology. (An interval-closed set is the same thing as an open or half-open or closed interval in RR , but in other sets like QQ there are interval-closed sets like ( _pi , +oo ) i^i QQ that are not intervals.) (Contributed by Mario Carneiro, 9-Sep-2015) (Revised by Thierry Arnoux, 11-Sep-2018)

Ref Expression
Hypotheses ordtNEW.b 
|- B = ( Base ` K )
ordtNEW.l 
|- .<_ = ( ( le ` K ) i^i ( B X. B ) )
ordtrest2NEW.2 
|- ( ph -> K e. Toset )
ordtrest2NEW.3 
|- ( ph -> A C_ B )
ordtrest2NEW.4 
|- ( ( ph /\ ( x e. A /\ y e. A ) ) -> { z e. B | ( x .<_ z /\ z .<_ y ) } C_ A )
Assertion ordtrest2NEW 
|- ( ph -> ( ordTop ` ( .<_ i^i ( A X. A ) ) ) = ( ( ordTop ` .<_ ) |`t A ) )

Proof

Step Hyp Ref Expression
1 ordtNEW.b 
 |-  B = ( Base ` K )
2 ordtNEW.l 
 |-  .<_ = ( ( le ` K ) i^i ( B X. B ) )
3 ordtrest2NEW.2 
 |-  ( ph -> K e. Toset )
4 ordtrest2NEW.3 
 |-  ( ph -> A C_ B )
5 ordtrest2NEW.4 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> { z e. B | ( x .<_ z /\ z .<_ y ) } C_ A )
6 tospos 
 |-  ( K e. Toset -> K e. Poset )
7 posprs 
 |-  ( K e. Poset -> K e. Proset )
8 3 6 7 3syl 
 |-  ( ph -> K e. Proset )
9 1 2 ordtrestNEW 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( ordTop ` ( .<_ i^i ( A X. A ) ) ) C_ ( ( ordTop ` .<_ ) |`t A ) )
10 8 4 9 syl2anc 
 |-  ( ph -> ( ordTop ` ( .<_ i^i ( A X. A ) ) ) C_ ( ( ordTop ` .<_ ) |`t A ) )
11 eqid 
 |-  ran ( z e. B |-> { w e. B | -. w .<_ z } ) = ran ( z e. B |-> { w e. B | -. w .<_ z } )
12 eqid 
 |-  ran ( z e. B |-> { w e. B | -. z .<_ w } ) = ran ( z e. B |-> { w e. B | -. z .<_ w } )
13 1 2 11 12 ordtprsval 
 |-  ( K e. Proset -> ( ordTop ` .<_ ) = ( topGen ` ( fi ` ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ) ) )
14 8 13 syl 
 |-  ( ph -> ( ordTop ` .<_ ) = ( topGen ` ( fi ` ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ) ) )
15 14 oveq1d 
 |-  ( ph -> ( ( ordTop ` .<_ ) |`t A ) = ( ( topGen ` ( fi ` ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ) ) |`t A ) )
16 fibas 
 |-  ( fi ` ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ) e. TopBases
17 1 fvexi 
 |-  B e. _V
18 17 a1i 
 |-  ( ph -> B e. _V )
19 18 4 ssexd 
 |-  ( ph -> A e. _V )
20 tgrest 
 |-  ( ( ( fi ` ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ) e. TopBases /\ A e. _V ) -> ( topGen ` ( ( fi ` ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ) |`t A ) ) = ( ( topGen ` ( fi ` ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ) ) |`t A ) )
21 16 19 20 sylancr 
 |-  ( ph -> ( topGen ` ( ( fi ` ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ) |`t A ) ) = ( ( topGen ` ( fi ` ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ) ) |`t A ) )
22 15 21 eqtr4d 
 |-  ( ph -> ( ( ordTop ` .<_ ) |`t A ) = ( topGen ` ( ( fi ` ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ) |`t A ) ) )
23 firest 
 |-  ( fi ` ( ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) |`t A ) ) = ( ( fi ` ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ) |`t A )
24 23 fveq2i 
 |-  ( topGen ` ( fi ` ( ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) |`t A ) ) ) = ( topGen ` ( ( fi ` ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ) |`t A ) )
25 22 24 eqtr4di 
 |-  ( ph -> ( ( ordTop ` .<_ ) |`t A ) = ( topGen ` ( fi ` ( ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) |`t A ) ) ) )
26 fvex 
 |-  ( le ` K ) e. _V
27 26 inex1 
 |-  ( ( le ` K ) i^i ( B X. B ) ) e. _V
28 2 27 eqeltri 
 |-  .<_ e. _V
29 28 inex1 
 |-  ( .<_ i^i ( A X. A ) ) e. _V
30 ordttop 
 |-  ( ( .<_ i^i ( A X. A ) ) e. _V -> ( ordTop ` ( .<_ i^i ( A X. A ) ) ) e. Top )
31 29 30 mp1i 
 |-  ( ph -> ( ordTop ` ( .<_ i^i ( A X. A ) ) ) e. Top )
32 1 2 11 12 ordtprsuni 
 |-  ( K e. Proset -> B = U. ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) )
33 8 32 syl 
 |-  ( ph -> B = U. ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) )
34 33 18 eqeltrrd 
 |-  ( ph -> U. ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) e. _V )
35 uniexb 
 |-  ( ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) e. _V <-> U. ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) e. _V )
36 34 35 sylibr 
 |-  ( ph -> ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) e. _V )
37 restval 
 |-  ( ( ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) e. _V /\ A e. _V ) -> ( ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) |`t A ) = ran ( v e. ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) |-> ( v i^i A ) ) )
38 36 19 37 syl2anc 
 |-  ( ph -> ( ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) |`t A ) = ran ( v e. ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) |-> ( v i^i A ) ) )
39 sseqin2 
 |-  ( A C_ B <-> ( B i^i A ) = A )
40 4 39 sylib 
 |-  ( ph -> ( B i^i A ) = A )
41 eqid 
 |-  dom ( .<_ i^i ( A X. A ) ) = dom ( .<_ i^i ( A X. A ) )
42 41 ordttopon 
 |-  ( ( .<_ i^i ( A X. A ) ) e. _V -> ( ordTop ` ( .<_ i^i ( A X. A ) ) ) e. ( TopOn ` dom ( .<_ i^i ( A X. A ) ) ) )
43 29 42 mp1i 
 |-  ( ph -> ( ordTop ` ( .<_ i^i ( A X. A ) ) ) e. ( TopOn ` dom ( .<_ i^i ( A X. A ) ) ) )
44 1 2 prsssdm 
 |-  ( ( K e. Proset /\ A C_ B ) -> dom ( .<_ i^i ( A X. A ) ) = A )
45 8 4 44 syl2anc 
 |-  ( ph -> dom ( .<_ i^i ( A X. A ) ) = A )
46 45 fveq2d 
 |-  ( ph -> ( TopOn ` dom ( .<_ i^i ( A X. A ) ) ) = ( TopOn ` A ) )
47 43 46 eleqtrd 
 |-  ( ph -> ( ordTop ` ( .<_ i^i ( A X. A ) ) ) e. ( TopOn ` A ) )
48 toponmax 
 |-  ( ( ordTop ` ( .<_ i^i ( A X. A ) ) ) e. ( TopOn ` A ) -> A e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) )
49 47 48 syl 
 |-  ( ph -> A e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) )
50 40 49 eqeltrd 
 |-  ( ph -> ( B i^i A ) e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) )
51 elsni 
 |-  ( v e. { B } -> v = B )
52 51 ineq1d 
 |-  ( v e. { B } -> ( v i^i A ) = ( B i^i A ) )
53 52 eleq1d 
 |-  ( v e. { B } -> ( ( v i^i A ) e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) <-> ( B i^i A ) e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) ) )
54 50 53 syl5ibrcom 
 |-  ( ph -> ( v e. { B } -> ( v i^i A ) e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) ) )
55 54 ralrimiv 
 |-  ( ph -> A. v e. { B } ( v i^i A ) e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) )
56 1 2 3 4 5 ordtrest2NEWlem 
 |-  ( ph -> A. v e. ran ( z e. B |-> { w e. B | -. w .<_ z } ) ( v i^i A ) e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) )
57 eqid 
 |-  ( ODual ` K ) = ( ODual ` K )
58 57 1 odubas 
 |-  B = ( Base ` ( ODual ` K ) )
59 2 cnveqi 
 |-  `' .<_ = `' ( ( le ` K ) i^i ( B X. B ) )
60 cnvin 
 |-  `' ( ( le ` K ) i^i ( B X. B ) ) = ( `' ( le ` K ) i^i `' ( B X. B ) )
61 cnvxp 
 |-  `' ( B X. B ) = ( B X. B )
62 61 ineq2i 
 |-  ( `' ( le ` K ) i^i `' ( B X. B ) ) = ( `' ( le ` K ) i^i ( B X. B ) )
63 eqid 
 |-  ( le ` K ) = ( le ` K )
64 57 63 oduleval 
 |-  `' ( le ` K ) = ( le ` ( ODual ` K ) )
65 64 ineq1i 
 |-  ( `' ( le ` K ) i^i ( B X. B ) ) = ( ( le ` ( ODual ` K ) ) i^i ( B X. B ) )
66 60 62 65 3eqtri 
 |-  `' ( ( le ` K ) i^i ( B X. B ) ) = ( ( le ` ( ODual ` K ) ) i^i ( B X. B ) )
67 59 66 eqtri 
 |-  `' .<_ = ( ( le ` ( ODual ` K ) ) i^i ( B X. B ) )
68 57 odutos 
 |-  ( K e. Toset -> ( ODual ` K ) e. Toset )
69 3 68 syl 
 |-  ( ph -> ( ODual ` K ) e. Toset )
70 vex 
 |-  y e. _V
71 vex 
 |-  z e. _V
72 70 71 brcnv 
 |-  ( y `' .<_ z <-> z .<_ y )
73 vex 
 |-  x e. _V
74 71 73 brcnv 
 |-  ( z `' .<_ x <-> x .<_ z )
75 72 74 anbi12ci 
 |-  ( ( y `' .<_ z /\ z `' .<_ x ) <-> ( x .<_ z /\ z .<_ y ) )
76 75 rabbii 
 |-  { z e. B | ( y `' .<_ z /\ z `' .<_ x ) } = { z e. B | ( x .<_ z /\ z .<_ y ) }
77 76 5 eqsstrid 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> { z e. B | ( y `' .<_ z /\ z `' .<_ x ) } C_ A )
78 77 ancom2s 
 |-  ( ( ph /\ ( y e. A /\ x e. A ) ) -> { z e. B | ( y `' .<_ z /\ z `' .<_ x ) } C_ A )
79 58 67 69 4 78 ordtrest2NEWlem 
 |-  ( ph -> A. v e. ran ( z e. B |-> { w e. B | -. w `' .<_ z } ) ( v i^i A ) e. ( ordTop ` ( `' .<_ i^i ( A X. A ) ) ) )
80 vex 
 |-  w e. _V
81 80 71 brcnv 
 |-  ( w `' .<_ z <-> z .<_ w )
82 81 bicomi 
 |-  ( z .<_ w <-> w `' .<_ z )
83 82 a1i 
 |-  ( ph -> ( z .<_ w <-> w `' .<_ z ) )
84 83 notbid 
 |-  ( ph -> ( -. z .<_ w <-> -. w `' .<_ z ) )
85 84 rabbidv 
 |-  ( ph -> { w e. B | -. z .<_ w } = { w e. B | -. w `' .<_ z } )
86 85 mpteq2dv 
 |-  ( ph -> ( z e. B |-> { w e. B | -. z .<_ w } ) = ( z e. B |-> { w e. B | -. w `' .<_ z } ) )
87 86 rneqd 
 |-  ( ph -> ran ( z e. B |-> { w e. B | -. z .<_ w } ) = ran ( z e. B |-> { w e. B | -. w `' .<_ z } ) )
88 1 ressprs 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( K |`s A ) e. Proset )
89 8 4 88 syl2anc 
 |-  ( ph -> ( K |`s A ) e. Proset )
90 eqid 
 |-  ( Base ` ( K |`s A ) ) = ( Base ` ( K |`s A ) )
91 eqid 
 |-  ( ( le ` ( K |`s A ) ) i^i ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) = ( ( le ` ( K |`s A ) ) i^i ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) )
92 90 91 ordtcnvNEW 
 |-  ( ( K |`s A ) e. Proset -> ( ordTop ` `' ( ( le ` ( K |`s A ) ) i^i ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) ) = ( ordTop ` ( ( le ` ( K |`s A ) ) i^i ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) ) )
93 89 92 syl 
 |-  ( ph -> ( ordTop ` `' ( ( le ` ( K |`s A ) ) i^i ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) ) = ( ordTop ` ( ( le ` ( K |`s A ) ) i^i ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) ) )
94 1 2 prsss 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( .<_ i^i ( A X. A ) ) = ( ( le ` K ) i^i ( A X. A ) ) )
95 8 4 94 syl2anc 
 |-  ( ph -> ( .<_ i^i ( A X. A ) ) = ( ( le ` K ) i^i ( A X. A ) ) )
96 eqid 
 |-  ( K |`s A ) = ( K |`s A )
97 96 63 ressle 
 |-  ( A e. _V -> ( le ` K ) = ( le ` ( K |`s A ) ) )
98 19 97 syl 
 |-  ( ph -> ( le ` K ) = ( le ` ( K |`s A ) ) )
99 96 1 ressbas2 
 |-  ( A C_ B -> A = ( Base ` ( K |`s A ) ) )
100 4 99 syl 
 |-  ( ph -> A = ( Base ` ( K |`s A ) ) )
101 100 sqxpeqd 
 |-  ( ph -> ( A X. A ) = ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) )
102 98 101 ineq12d 
 |-  ( ph -> ( ( le ` K ) i^i ( A X. A ) ) = ( ( le ` ( K |`s A ) ) i^i ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) )
103 95 102 eqtrd 
 |-  ( ph -> ( .<_ i^i ( A X. A ) ) = ( ( le ` ( K |`s A ) ) i^i ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) )
104 103 cnveqd 
 |-  ( ph -> `' ( .<_ i^i ( A X. A ) ) = `' ( ( le ` ( K |`s A ) ) i^i ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) )
105 104 fveq2d 
 |-  ( ph -> ( ordTop ` `' ( .<_ i^i ( A X. A ) ) ) = ( ordTop ` `' ( ( le ` ( K |`s A ) ) i^i ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) ) )
106 103 fveq2d 
 |-  ( ph -> ( ordTop ` ( .<_ i^i ( A X. A ) ) ) = ( ordTop ` ( ( le ` ( K |`s A ) ) i^i ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) ) )
107 93 105 106 3eqtr4d 
 |-  ( ph -> ( ordTop ` `' ( .<_ i^i ( A X. A ) ) ) = ( ordTop ` ( .<_ i^i ( A X. A ) ) ) )
108 cnvin 
 |-  `' ( .<_ i^i ( A X. A ) ) = ( `' .<_ i^i `' ( A X. A ) )
109 cnvxp 
 |-  `' ( A X. A ) = ( A X. A )
110 109 ineq2i 
 |-  ( `' .<_ i^i `' ( A X. A ) ) = ( `' .<_ i^i ( A X. A ) )
111 108 110 eqtri 
 |-  `' ( .<_ i^i ( A X. A ) ) = ( `' .<_ i^i ( A X. A ) )
112 111 fveq2i 
 |-  ( ordTop ` `' ( .<_ i^i ( A X. A ) ) ) = ( ordTop ` ( `' .<_ i^i ( A X. A ) ) )
113 107 112 eqtr3di 
 |-  ( ph -> ( ordTop ` ( .<_ i^i ( A X. A ) ) ) = ( ordTop ` ( `' .<_ i^i ( A X. A ) ) ) )
114 113 eleq2d 
 |-  ( ph -> ( ( v i^i A ) e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) <-> ( v i^i A ) e. ( ordTop ` ( `' .<_ i^i ( A X. A ) ) ) ) )
115 87 114 raleqbidv 
 |-  ( ph -> ( A. v e. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ( v i^i A ) e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) <-> A. v e. ran ( z e. B |-> { w e. B | -. w `' .<_ z } ) ( v i^i A ) e. ( ordTop ` ( `' .<_ i^i ( A X. A ) ) ) ) )
116 79 115 mpbird 
 |-  ( ph -> A. v e. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ( v i^i A ) e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) )
117 ralunb 
 |-  ( A. v e. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ( v i^i A ) e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) <-> ( A. v e. ran ( z e. B |-> { w e. B | -. w .<_ z } ) ( v i^i A ) e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) /\ A. v e. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ( v i^i A ) e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) ) )
118 56 116 117 sylanbrc 
 |-  ( ph -> A. v e. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ( v i^i A ) e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) )
119 ralunb 
 |-  ( A. v e. ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ( v i^i A ) e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) <-> ( A. v e. { B } ( v i^i A ) e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) /\ A. v e. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ( v i^i A ) e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) ) )
120 55 118 119 sylanbrc 
 |-  ( ph -> A. v e. ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ( v i^i A ) e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) )
121 eqid 
 |-  ( v e. ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) |-> ( v i^i A ) ) = ( v e. ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) |-> ( v i^i A ) )
122 121 fmpt 
 |-  ( A. v e. ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ( v i^i A ) e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) <-> ( v e. ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) |-> ( v i^i A ) ) : ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) --> ( ordTop ` ( .<_ i^i ( A X. A ) ) ) )
123 120 122 sylib 
 |-  ( ph -> ( v e. ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) |-> ( v i^i A ) ) : ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) --> ( ordTop ` ( .<_ i^i ( A X. A ) ) ) )
124 123 frnd 
 |-  ( ph -> ran ( v e. ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) |-> ( v i^i A ) ) C_ ( ordTop ` ( .<_ i^i ( A X. A ) ) ) )
125 38 124 eqsstrd 
 |-  ( ph -> ( ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) |`t A ) C_ ( ordTop ` ( .<_ i^i ( A X. A ) ) ) )
126 tgfiss 
 |-  ( ( ( ordTop ` ( .<_ i^i ( A X. A ) ) ) e. Top /\ ( ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) |`t A ) C_ ( ordTop ` ( .<_ i^i ( A X. A ) ) ) ) -> ( topGen ` ( fi ` ( ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) |`t A ) ) ) C_ ( ordTop ` ( .<_ i^i ( A X. A ) ) ) )
127 31 125 126 syl2anc 
 |-  ( ph -> ( topGen ` ( fi ` ( ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) |`t A ) ) ) C_ ( ordTop ` ( .<_ i^i ( A X. A ) ) ) )
128 25 127 eqsstrd 
 |-  ( ph -> ( ( ordTop ` .<_ ) |`t A ) C_ ( ordTop ` ( .<_ i^i ( A X. A ) ) ) )
129 10 128 eqssd 
 |-  ( ph -> ( ordTop ` ( .<_ i^i ( A X. A ) ) ) = ( ( ordTop ` .<_ ) |`t A ) )