Metamath Proof Explorer

Theorem ordtrestNEW

Description: The subspace topology of an order topology is in general finer than the topology generated by the restricted order, but we do have inclusion in one direction. (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 ) )
Assertion ordtrestNEW 
|- ( ( K e. Proset /\ A C_ B ) -> ( ordTop ` ( .<_ i^i ( A X. A ) ) ) C_ ( ( 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 fvex 
 |-  ( le ` K ) e. _V
4 3 inex1 
 |-  ( ( le ` K ) i^i ( B X. B ) ) e. _V
5 2 4 eqeltri 
 |-  .<_ e. _V
6 5 inex1 
 |-  ( .<_ i^i ( A X. A ) ) e. _V
7 eqid 
 |-  dom ( .<_ i^i ( A X. A ) ) = dom ( .<_ i^i ( A X. A ) )
8 eqid 
 |-  ran ( x e. dom ( .<_ i^i ( A X. A ) ) |-> { y e. dom ( .<_ i^i ( A X. A ) ) | -. y ( .<_ i^i ( A X. A ) ) x } ) = ran ( x e. dom ( .<_ i^i ( A X. A ) ) |-> { y e. dom ( .<_ i^i ( A X. A ) ) | -. y ( .<_ i^i ( A X. A ) ) x } )
9 eqid 
 |-  ran ( x e. dom ( .<_ i^i ( A X. A ) ) |-> { y e. dom ( .<_ i^i ( A X. A ) ) | -. x ( .<_ i^i ( A X. A ) ) y } ) = ran ( x e. dom ( .<_ i^i ( A X. A ) ) |-> { y e. dom ( .<_ i^i ( A X. A ) ) | -. x ( .<_ i^i ( A X. A ) ) y } )
10 7 8 9 ordtval 
 |-  ( ( .<_ i^i ( A X. A ) ) e. _V -> ( ordTop ` ( .<_ i^i ( A X. A ) ) ) = ( topGen ` ( fi ` ( { dom ( .<_ i^i ( A X. A ) ) } u. ( ran ( x e. dom ( .<_ i^i ( A X. A ) ) |-> { y e. dom ( .<_ i^i ( A X. A ) ) | -. y ( .<_ i^i ( A X. A ) ) x } ) u. ran ( x e. dom ( .<_ i^i ( A X. A ) ) |-> { y e. dom ( .<_ i^i ( A X. A ) ) | -. x ( .<_ i^i ( A X. A ) ) y } ) ) ) ) ) )
11 6 10 mp1i 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( ordTop ` ( .<_ i^i ( A X. A ) ) ) = ( topGen ` ( fi ` ( { dom ( .<_ i^i ( A X. A ) ) } u. ( ran ( x e. dom ( .<_ i^i ( A X. A ) ) |-> { y e. dom ( .<_ i^i ( A X. A ) ) | -. y ( .<_ i^i ( A X. A ) ) x } ) u. ran ( x e. dom ( .<_ i^i ( A X. A ) ) |-> { y e. dom ( .<_ i^i ( A X. A ) ) | -. x ( .<_ i^i ( A X. A ) ) y } ) ) ) ) ) )
12 ordttop 
 |-  ( .<_ e. _V -> ( ordTop ` .<_ ) e. Top )
13 5 12 ax-mp 
 |-  ( ordTop ` .<_ ) e. Top
14 fvex 
 |-  ( Base ` K ) e. _V
15 1 14 eqeltri 
 |-  B e. _V
16 15 ssex 
 |-  ( A C_ B -> A e. _V )
17 resttop 
 |-  ( ( ( ordTop ` .<_ ) e. Top /\ A e. _V ) -> ( ( ordTop ` .<_ ) |`t A ) e. Top )
18 13 16 17 sylancr 
 |-  ( A C_ B -> ( ( ordTop ` .<_ ) |`t A ) e. Top )
19 18 adantl 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( ( ordTop ` .<_ ) |`t A ) e. Top )
20 1 ressprs 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( K |`s A ) e. Proset )
21 eqid 
 |-  ( Base ` ( K |`s A ) ) = ( Base ` ( K |`s A ) )
22 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 ) ) ) )
23 21 22 prsdm 
 |-  ( ( K |`s A ) e. Proset -> dom ( ( le ` ( K |`s A ) ) i^i ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) = ( Base ` ( K |`s A ) ) )
24 20 23 syl 
 |-  ( ( K e. Proset /\ A C_ B ) -> dom ( ( le ` ( K |`s A ) ) i^i ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) = ( Base ` ( K |`s A ) ) )
25 eqid 
 |-  ( K |`s A ) = ( K |`s A )
26 25 1 ressbas2 
 |-  ( A C_ B -> A = ( Base ` ( K |`s A ) ) )
27 fvex 
 |-  ( Base ` ( K |`s A ) ) e. _V
28 26 27 eqeltrdi 
 |-  ( A C_ B -> A e. _V )
29 eqid 
 |-  ( le ` K ) = ( le ` K )
30 25 29 ressle 
 |-  ( A e. _V -> ( le ` K ) = ( le ` ( K |`s A ) ) )
31 28 30 syl 
 |-  ( A C_ B -> ( le ` K ) = ( le ` ( K |`s A ) ) )
32 31 adantl 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( le ` K ) = ( le ` ( K |`s A ) ) )
33 26 adantl 
 |-  ( ( K e. Proset /\ A C_ B ) -> A = ( Base ` ( K |`s A ) ) )
34 33 sqxpeqd 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( A X. A ) = ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) )
35 32 34 ineq12d 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( ( le ` K ) i^i ( A X. A ) ) = ( ( le ` ( K |`s A ) ) i^i ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) )
36 35 dmeqd 
 |-  ( ( K e. Proset /\ A C_ B ) -> dom ( ( le ` K ) i^i ( A X. A ) ) = dom ( ( le ` ( K |`s A ) ) i^i ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) )
37 24 36 33 3eqtr4d 
 |-  ( ( K e. Proset /\ A C_ B ) -> dom ( ( le ` K ) i^i ( A X. A ) ) = A )
38 1 2 prsss 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( .<_ i^i ( A X. A ) ) = ( ( le ` K ) i^i ( A X. A ) ) )
39 38 dmeqd 
 |-  ( ( K e. Proset /\ A C_ B ) -> dom ( .<_ i^i ( A X. A ) ) = dom ( ( le ` K ) i^i ( A X. A ) ) )
40 1 2 prsdm 
 |-  ( K e. Proset -> dom .<_ = B )
41 40 sseq2d 
 |-  ( K e. Proset -> ( A C_ dom .<_ <-> A C_ B ) )
42 41 biimpar 
 |-  ( ( K e. Proset /\ A C_ B ) -> A C_ dom .<_ )
43 sseqin2 
 |-  ( A C_ dom .<_ <-> ( dom .<_ i^i A ) = A )
44 42 43 sylib 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( dom .<_ i^i A ) = A )
45 37 39 44 3eqtr4d 
 |-  ( ( K e. Proset /\ A C_ B ) -> dom ( .<_ i^i ( A X. A ) ) = ( dom .<_ i^i A ) )
46 5 12 mp1i 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( ordTop ` .<_ ) e. Top )
47 16 adantl 
 |-  ( ( K e. Proset /\ A C_ B ) -> A e. _V )
48 eqid 
 |-  dom .<_ = dom .<_
49 48 ordttopon 
 |-  ( .<_ e. _V -> ( ordTop ` .<_ ) e. ( TopOn ` dom .<_ ) )
50 5 49 mp1i 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( ordTop ` .<_ ) e. ( TopOn ` dom .<_ ) )
51 toponmax 
 |-  ( ( ordTop ` .<_ ) e. ( TopOn ` dom .<_ ) -> dom .<_ e. ( ordTop ` .<_ ) )
52 50 51 syl 
 |-  ( ( K e. Proset /\ A C_ B ) -> dom .<_ e. ( ordTop ` .<_ ) )
53 elrestr 
 |-  ( ( ( ordTop ` .<_ ) e. Top /\ A e. _V /\ dom .<_ e. ( ordTop ` .<_ ) ) -> ( dom .<_ i^i A ) e. ( ( ordTop ` .<_ ) |`t A ) )
54 46 47 52 53 syl3anc 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( dom .<_ i^i A ) e. ( ( ordTop ` .<_ ) |`t A ) )
55 45 54 eqeltrd 
 |-  ( ( K e. Proset /\ A C_ B ) -> dom ( .<_ i^i ( A X. A ) ) e. ( ( ordTop ` .<_ ) |`t A ) )
56 55 snssd 
 |-  ( ( K e. Proset /\ A C_ B ) -> { dom ( .<_ i^i ( A X. A ) ) } C_ ( ( ordTop ` .<_ ) |`t A ) )
57 rabeq 
 |-  ( dom ( .<_ i^i ( A X. A ) ) = ( dom .<_ i^i A ) -> { y e. dom ( .<_ i^i ( A X. A ) ) | -. y ( .<_ i^i ( A X. A ) ) x } = { y e. ( dom .<_ i^i A ) | -. y ( .<_ i^i ( A X. A ) ) x } )
58 45 57 syl 
 |-  ( ( K e. Proset /\ A C_ B ) -> { y e. dom ( .<_ i^i ( A X. A ) ) | -. y ( .<_ i^i ( A X. A ) ) x } = { y e. ( dom .<_ i^i A ) | -. y ( .<_ i^i ( A X. A ) ) x } )
59 45 58 mpteq12dv 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( x e. dom ( .<_ i^i ( A X. A ) ) |-> { y e. dom ( .<_ i^i ( A X. A ) ) | -. y ( .<_ i^i ( A X. A ) ) x } ) = ( x e. ( dom .<_ i^i A ) |-> { y e. ( dom .<_ i^i A ) | -. y ( .<_ i^i ( A X. A ) ) x } ) )
60 59 rneqd 
 |-  ( ( K e. Proset /\ A C_ B ) -> ran ( x e. dom ( .<_ i^i ( A X. A ) ) |-> { y e. dom ( .<_ i^i ( A X. A ) ) | -. y ( .<_ i^i ( A X. A ) ) x } ) = ran ( x e. ( dom .<_ i^i A ) |-> { y e. ( dom .<_ i^i A ) | -. y ( .<_ i^i ( A X. A ) ) x } ) )
61 inrab2 
 |-  ( { y e. dom .<_ | -. y .<_ x } i^i A ) = { y e. ( dom .<_ i^i A ) | -. y .<_ x }
62 inss2 
 |-  ( dom .<_ i^i A ) C_ A
63 simpr 
 |-  ( ( ( ( K e. Proset /\ A C_ B ) /\ x e. ( dom .<_ i^i A ) ) /\ y e. ( dom .<_ i^i A ) ) -> y e. ( dom .<_ i^i A ) )
64 62 63 sselid 
 |-  ( ( ( ( K e. Proset /\ A C_ B ) /\ x e. ( dom .<_ i^i A ) ) /\ y e. ( dom .<_ i^i A ) ) -> y e. A )
65 simpr 
 |-  ( ( ( K e. Proset /\ A C_ B ) /\ x e. ( dom .<_ i^i A ) ) -> x e. ( dom .<_ i^i A ) )
66 62 65 sselid 
 |-  ( ( ( K e. Proset /\ A C_ B ) /\ x e. ( dom .<_ i^i A ) ) -> x e. A )
67 66 adantr 
 |-  ( ( ( ( K e. Proset /\ A C_ B ) /\ x e. ( dom .<_ i^i A ) ) /\ y e. ( dom .<_ i^i A ) ) -> x e. A )
68 brinxp 
 |-  ( ( y e. A /\ x e. A ) -> ( y .<_ x <-> y ( .<_ i^i ( A X. A ) ) x ) )
69 64 67 68 syl2anc 
 |-  ( ( ( ( K e. Proset /\ A C_ B ) /\ x e. ( dom .<_ i^i A ) ) /\ y e. ( dom .<_ i^i A ) ) -> ( y .<_ x <-> y ( .<_ i^i ( A X. A ) ) x ) )
70 69 notbid 
 |-  ( ( ( ( K e. Proset /\ A C_ B ) /\ x e. ( dom .<_ i^i A ) ) /\ y e. ( dom .<_ i^i A ) ) -> ( -. y .<_ x <-> -. y ( .<_ i^i ( A X. A ) ) x ) )
71 70 rabbidva 
 |-  ( ( ( K e. Proset /\ A C_ B ) /\ x e. ( dom .<_ i^i A ) ) -> { y e. ( dom .<_ i^i A ) | -. y .<_ x } = { y e. ( dom .<_ i^i A ) | -. y ( .<_ i^i ( A X. A ) ) x } )
72 61 71 syl5eq 
 |-  ( ( ( K e. Proset /\ A C_ B ) /\ x e. ( dom .<_ i^i A ) ) -> ( { y e. dom .<_ | -. y .<_ x } i^i A ) = { y e. ( dom .<_ i^i A ) | -. y ( .<_ i^i ( A X. A ) ) x } )
73 5 12 mp1i 
 |-  ( ( ( K e. Proset /\ A C_ B ) /\ x e. ( dom .<_ i^i A ) ) -> ( ordTop ` .<_ ) e. Top )
74 47 adantr 
 |-  ( ( ( K e. Proset /\ A C_ B ) /\ x e. ( dom .<_ i^i A ) ) -> A e. _V )
75 simpl 
 |-  ( ( K e. Proset /\ A C_ B ) -> K e. Proset )
76 inss1 
 |-  ( dom .<_ i^i A ) C_ dom .<_
77 76 sseli 
 |-  ( x e. ( dom .<_ i^i A ) -> x e. dom .<_ )
78 48 ordtopn1 
 |-  ( ( .<_ e. _V /\ x e. dom .<_ ) -> { y e. dom .<_ | -. y .<_ x } e. ( ordTop ` .<_ ) )
79 5 78 mpan 
 |-  ( x e. dom .<_ -> { y e. dom .<_ | -. y .<_ x } e. ( ordTop ` .<_ ) )
80 79 adantl 
 |-  ( ( K e. Proset /\ x e. dom .<_ ) -> { y e. dom .<_ | -. y .<_ x } e. ( ordTop ` .<_ ) )
81 75 77 80 syl2an 
 |-  ( ( ( K e. Proset /\ A C_ B ) /\ x e. ( dom .<_ i^i A ) ) -> { y e. dom .<_ | -. y .<_ x } e. ( ordTop ` .<_ ) )
82 elrestr 
 |-  ( ( ( ordTop ` .<_ ) e. Top /\ A e. _V /\ { y e. dom .<_ | -. y .<_ x } e. ( ordTop ` .<_ ) ) -> ( { y e. dom .<_ | -. y .<_ x } i^i A ) e. ( ( ordTop ` .<_ ) |`t A ) )
83 73 74 81 82 syl3anc 
 |-  ( ( ( K e. Proset /\ A C_ B ) /\ x e. ( dom .<_ i^i A ) ) -> ( { y e. dom .<_ | -. y .<_ x } i^i A ) e. ( ( ordTop ` .<_ ) |`t A ) )
84 72 83 eqeltrrd 
 |-  ( ( ( K e. Proset /\ A C_ B ) /\ x e. ( dom .<_ i^i A ) ) -> { y e. ( dom .<_ i^i A ) | -. y ( .<_ i^i ( A X. A ) ) x } e. ( ( ordTop ` .<_ ) |`t A ) )
85 84 fmpttd 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( x e. ( dom .<_ i^i A ) |-> { y e. ( dom .<_ i^i A ) | -. y ( .<_ i^i ( A X. A ) ) x } ) : ( dom .<_ i^i A ) --> ( ( ordTop ` .<_ ) |`t A ) )
86 85 frnd 
 |-  ( ( K e. Proset /\ A C_ B ) -> ran ( x e. ( dom .<_ i^i A ) |-> { y e. ( dom .<_ i^i A ) | -. y ( .<_ i^i ( A X. A ) ) x } ) C_ ( ( ordTop ` .<_ ) |`t A ) )
87 60 86 eqsstrd 
 |-  ( ( K e. Proset /\ A C_ B ) -> ran ( x e. dom ( .<_ i^i ( A X. A ) ) |-> { y e. dom ( .<_ i^i ( A X. A ) ) | -. y ( .<_ i^i ( A X. A ) ) x } ) C_ ( ( ordTop ` .<_ ) |`t A ) )
88 rabeq 
 |-  ( dom ( .<_ i^i ( A X. A ) ) = ( dom .<_ i^i A ) -> { y e. dom ( .<_ i^i ( A X. A ) ) | -. x ( .<_ i^i ( A X. A ) ) y } = { y e. ( dom .<_ i^i A ) | -. x ( .<_ i^i ( A X. A ) ) y } )
89 45 88 syl 
 |-  ( ( K e. Proset /\ A C_ B ) -> { y e. dom ( .<_ i^i ( A X. A ) ) | -. x ( .<_ i^i ( A X. A ) ) y } = { y e. ( dom .<_ i^i A ) | -. x ( .<_ i^i ( A X. A ) ) y } )
90 45 89 mpteq12dv 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( x e. dom ( .<_ i^i ( A X. A ) ) |-> { y e. dom ( .<_ i^i ( A X. A ) ) | -. x ( .<_ i^i ( A X. A ) ) y } ) = ( x e. ( dom .<_ i^i A ) |-> { y e. ( dom .<_ i^i A ) | -. x ( .<_ i^i ( A X. A ) ) y } ) )
91 90 rneqd 
 |-  ( ( K e. Proset /\ A C_ B ) -> ran ( x e. dom ( .<_ i^i ( A X. A ) ) |-> { y e. dom ( .<_ i^i ( A X. A ) ) | -. x ( .<_ i^i ( A X. A ) ) y } ) = ran ( x e. ( dom .<_ i^i A ) |-> { y e. ( dom .<_ i^i A ) | -. x ( .<_ i^i ( A X. A ) ) y } ) )
92 inrab2 
 |-  ( { y e. dom .<_ | -. x .<_ y } i^i A ) = { y e. ( dom .<_ i^i A ) | -. x .<_ y }
93 brinxp 
 |-  ( ( x e. A /\ y e. A ) -> ( x .<_ y <-> x ( .<_ i^i ( A X. A ) ) y ) )
94 67 64 93 syl2anc 
 |-  ( ( ( ( K e. Proset /\ A C_ B ) /\ x e. ( dom .<_ i^i A ) ) /\ y e. ( dom .<_ i^i A ) ) -> ( x .<_ y <-> x ( .<_ i^i ( A X. A ) ) y ) )
95 94 notbid 
 |-  ( ( ( ( K e. Proset /\ A C_ B ) /\ x e. ( dom .<_ i^i A ) ) /\ y e. ( dom .<_ i^i A ) ) -> ( -. x .<_ y <-> -. x ( .<_ i^i ( A X. A ) ) y ) )
96 95 rabbidva 
 |-  ( ( ( K e. Proset /\ A C_ B ) /\ x e. ( dom .<_ i^i A ) ) -> { y e. ( dom .<_ i^i A ) | -. x .<_ y } = { y e. ( dom .<_ i^i A ) | -. x ( .<_ i^i ( A X. A ) ) y } )
97 92 96 syl5eq 
 |-  ( ( ( K e. Proset /\ A C_ B ) /\ x e. ( dom .<_ i^i A ) ) -> ( { y e. dom .<_ | -. x .<_ y } i^i A ) = { y e. ( dom .<_ i^i A ) | -. x ( .<_ i^i ( A X. A ) ) y } )
98 48 ordtopn2 
 |-  ( ( .<_ e. _V /\ x e. dom .<_ ) -> { y e. dom .<_ | -. x .<_ y } e. ( ordTop ` .<_ ) )
99 5 98 mpan 
 |-  ( x e. dom .<_ -> { y e. dom .<_ | -. x .<_ y } e. ( ordTop ` .<_ ) )
100 99 adantl 
 |-  ( ( K e. Proset /\ x e. dom .<_ ) -> { y e. dom .<_ | -. x .<_ y } e. ( ordTop ` .<_ ) )
101 75 77 100 syl2an 
 |-  ( ( ( K e. Proset /\ A C_ B ) /\ x e. ( dom .<_ i^i A ) ) -> { y e. dom .<_ | -. x .<_ y } e. ( ordTop ` .<_ ) )
102 elrestr 
 |-  ( ( ( ordTop ` .<_ ) e. Top /\ A e. _V /\ { y e. dom .<_ | -. x .<_ y } e. ( ordTop ` .<_ ) ) -> ( { y e. dom .<_ | -. x .<_ y } i^i A ) e. ( ( ordTop ` .<_ ) |`t A ) )
103 73 74 101 102 syl3anc 
 |-  ( ( ( K e. Proset /\ A C_ B ) /\ x e. ( dom .<_ i^i A ) ) -> ( { y e. dom .<_ | -. x .<_ y } i^i A ) e. ( ( ordTop ` .<_ ) |`t A ) )
104 97 103 eqeltrrd 
 |-  ( ( ( K e. Proset /\ A C_ B ) /\ x e. ( dom .<_ i^i A ) ) -> { y e. ( dom .<_ i^i A ) | -. x ( .<_ i^i ( A X. A ) ) y } e. ( ( ordTop ` .<_ ) |`t A ) )
105 104 fmpttd 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( x e. ( dom .<_ i^i A ) |-> { y e. ( dom .<_ i^i A ) | -. x ( .<_ i^i ( A X. A ) ) y } ) : ( dom .<_ i^i A ) --> ( ( ordTop ` .<_ ) |`t A ) )
106 105 frnd 
 |-  ( ( K e. Proset /\ A C_ B ) -> ran ( x e. ( dom .<_ i^i A ) |-> { y e. ( dom .<_ i^i A ) | -. x ( .<_ i^i ( A X. A ) ) y } ) C_ ( ( ordTop ` .<_ ) |`t A ) )
107 91 106 eqsstrd 
 |-  ( ( K e. Proset /\ A C_ B ) -> ran ( x e. dom ( .<_ i^i ( A X. A ) ) |-> { y e. dom ( .<_ i^i ( A X. A ) ) | -. x ( .<_ i^i ( A X. A ) ) y } ) C_ ( ( ordTop ` .<_ ) |`t A ) )
108 87 107 unssd 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( ran ( x e. dom ( .<_ i^i ( A X. A ) ) |-> { y e. dom ( .<_ i^i ( A X. A ) ) | -. y ( .<_ i^i ( A X. A ) ) x } ) u. ran ( x e. dom ( .<_ i^i ( A X. A ) ) |-> { y e. dom ( .<_ i^i ( A X. A ) ) | -. x ( .<_ i^i ( A X. A ) ) y } ) ) C_ ( ( ordTop ` .<_ ) |`t A ) )
109 56 108 unssd 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( { dom ( .<_ i^i ( A X. A ) ) } u. ( ran ( x e. dom ( .<_ i^i ( A X. A ) ) |-> { y e. dom ( .<_ i^i ( A X. A ) ) | -. y ( .<_ i^i ( A X. A ) ) x } ) u. ran ( x e. dom ( .<_ i^i ( A X. A ) ) |-> { y e. dom ( .<_ i^i ( A X. A ) ) | -. x ( .<_ i^i ( A X. A ) ) y } ) ) ) C_ ( ( ordTop ` .<_ ) |`t A ) )
110 tgfiss 
 |-  ( ( ( ( ordTop ` .<_ ) |`t A ) e. Top /\ ( { dom ( .<_ i^i ( A X. A ) ) } u. ( ran ( x e. dom ( .<_ i^i ( A X. A ) ) |-> { y e. dom ( .<_ i^i ( A X. A ) ) | -. y ( .<_ i^i ( A X. A ) ) x } ) u. ran ( x e. dom ( .<_ i^i ( A X. A ) ) |-> { y e. dom ( .<_ i^i ( A X. A ) ) | -. x ( .<_ i^i ( A X. A ) ) y } ) ) ) C_ ( ( ordTop ` .<_ ) |`t A ) ) -> ( topGen ` ( fi ` ( { dom ( .<_ i^i ( A X. A ) ) } u. ( ran ( x e. dom ( .<_ i^i ( A X. A ) ) |-> { y e. dom ( .<_ i^i ( A X. A ) ) | -. y ( .<_ i^i ( A X. A ) ) x } ) u. ran ( x e. dom ( .<_ i^i ( A X. A ) ) |-> { y e. dom ( .<_ i^i ( A X. A ) ) | -. x ( .<_ i^i ( A X. A ) ) y } ) ) ) ) ) C_ ( ( ordTop ` .<_ ) |`t A ) )
111 19 109 110 syl2anc 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( topGen ` ( fi ` ( { dom ( .<_ i^i ( A X. A ) ) } u. ( ran ( x e. dom ( .<_ i^i ( A X. A ) ) |-> { y e. dom ( .<_ i^i ( A X. A ) ) | -. y ( .<_ i^i ( A X. A ) ) x } ) u. ran ( x e. dom ( .<_ i^i ( A X. A ) ) |-> { y e. dom ( .<_ i^i ( A X. A ) ) | -. x ( .<_ i^i ( A X. A ) ) y } ) ) ) ) ) C_ ( ( ordTop ` .<_ ) |`t A ) )
112 11 111 eqsstrd 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( ordTop ` ( .<_ i^i ( A X. A ) ) ) C_ ( ( ordTop ` .<_ ) |`t A ) )