Metamath Proof Explorer

Theorem xkopt

Description: The compact-open topology on a discrete set coincides with the product topology where all the factors are the same. (Contributed by Mario Carneiro, 19-Mar-2015) (Revised by Mario Carneiro, 12-Sep-2015)

Ref Expression
Assertion xkopt 
|- ( ( R e. Top /\ A e. V ) -> ( R ^ko ~P A ) = ( Xt_ ` ( A X. { R } ) ) )

Proof

Step Hyp Ref Expression
1 distop 
 |-  ( A e. V -> ~P A e. Top )
2 simpl 
 |-  ( ( R e. Top /\ A e. V ) -> R e. Top )
3 unipw 
 |-  U. ~P A = A
4 3 eqcomi 
 |-  A = U. ~P A
5 eqid 
 |-  { x e. ~P A | ( ~P A |`t x ) e. Comp } = { x e. ~P A | ( ~P A |`t x ) e. Comp }
6 eqid 
 |-  ( k e. { x e. ~P A | ( ~P A |`t x ) e. Comp } , v e. R |-> { f e. ( ~P A Cn R ) | ( f " k ) C_ v } ) = ( k e. { x e. ~P A | ( ~P A |`t x ) e. Comp } , v e. R |-> { f e. ( ~P A Cn R ) | ( f " k ) C_ v } )
7 4 5 6 xkoval 
 |-  ( ( ~P A e. Top /\ R e. Top ) -> ( R ^ko ~P A ) = ( topGen ` ( fi ` ran ( k e. { x e. ~P A | ( ~P A |`t x ) e. Comp } , v e. R |-> { f e. ( ~P A Cn R ) | ( f " k ) C_ v } ) ) ) )
8 1 2 7 syl2an2 
 |-  ( ( R e. Top /\ A e. V ) -> ( R ^ko ~P A ) = ( topGen ` ( fi ` ran ( k e. { x e. ~P A | ( ~P A |`t x ) e. Comp } , v e. R |-> { f e. ( ~P A Cn R ) | ( f " k ) C_ v } ) ) ) )
9 simpr 
 |-  ( ( R e. Top /\ A e. V ) -> A e. V )
10 fconst6g 
 |-  ( R e. Top -> ( A X. { R } ) : A --> Top )
11 10 adantr 
 |-  ( ( R e. Top /\ A e. V ) -> ( A X. { R } ) : A --> Top )
12 pttop 
 |-  ( ( A e. V /\ ( A X. { R } ) : A --> Top ) -> ( Xt_ ` ( A X. { R } ) ) e. Top )
13 9 11 12 syl2anc 
 |-  ( ( R e. Top /\ A e. V ) -> ( Xt_ ` ( A X. { R } ) ) e. Top )
14 elpwi 
 |-  ( x e. ~P A -> x C_ A )
15 restdis 
 |-  ( ( A e. V /\ x C_ A ) -> ( ~P A |`t x ) = ~P x )
16 14 15 sylan2 
 |-  ( ( A e. V /\ x e. ~P A ) -> ( ~P A |`t x ) = ~P x )
17 16 adantll 
 |-  ( ( ( R e. Top /\ A e. V ) /\ x e. ~P A ) -> ( ~P A |`t x ) = ~P x )
18 17 eleq1d 
 |-  ( ( ( R e. Top /\ A e. V ) /\ x e. ~P A ) -> ( ( ~P A |`t x ) e. Comp <-> ~P x e. Comp ) )
19 discmp 
 |-  ( x e. Fin <-> ~P x e. Comp )
20 18 19 bitr4di 
 |-  ( ( ( R e. Top /\ A e. V ) /\ x e. ~P A ) -> ( ( ~P A |`t x ) e. Comp <-> x e. Fin ) )
21 20 rabbidva 
 |-  ( ( R e. Top /\ A e. V ) -> { x e. ~P A | ( ~P A |`t x ) e. Comp } = { x e. ~P A | x e. Fin } )
22 dfin5 
 |-  ( ~P A i^i Fin ) = { x e. ~P A | x e. Fin }
23 21 22 eqtr4di 
 |-  ( ( R e. Top /\ A e. V ) -> { x e. ~P A | ( ~P A |`t x ) e. Comp } = ( ~P A i^i Fin ) )
24 eqidd 
 |-  ( ( R e. Top /\ A e. V ) -> R = R )
25 toptopon2 
 |-  ( R e. Top <-> R e. ( TopOn ` U. R ) )
26 cndis 
 |-  ( ( A e. V /\ R e. ( TopOn ` U. R ) ) -> ( ~P A Cn R ) = ( U. R ^m A ) )
27 26 ancoms 
 |-  ( ( R e. ( TopOn ` U. R ) /\ A e. V ) -> ( ~P A Cn R ) = ( U. R ^m A ) )
28 25 27 sylanb 
 |-  ( ( R e. Top /\ A e. V ) -> ( ~P A Cn R ) = ( U. R ^m A ) )
29 28 rabeqdv 
 |-  ( ( R e. Top /\ A e. V ) -> { f e. ( ~P A Cn R ) | ( f " k ) C_ v } = { f e. ( U. R ^m A ) | ( f " k ) C_ v } )
30 23 24 29 mpoeq123dv 
 |-  ( ( R e. Top /\ A e. V ) -> ( k e. { x e. ~P A | ( ~P A |`t x ) e. Comp } , v e. R |-> { f e. ( ~P A Cn R ) | ( f " k ) C_ v } ) = ( k e. ( ~P A i^i Fin ) , v e. R |-> { f e. ( U. R ^m A ) | ( f " k ) C_ v } ) )
31 30 rneqd 
 |-  ( ( R e. Top /\ A e. V ) -> ran ( k e. { x e. ~P A | ( ~P A |`t x ) e. Comp } , v e. R |-> { f e. ( ~P A Cn R ) | ( f " k ) C_ v } ) = ran ( k e. ( ~P A i^i Fin ) , v e. R |-> { f e. ( U. R ^m A ) | ( f " k ) C_ v } ) )
32 eqid 
 |-  ( k e. ( ~P A i^i Fin ) , v e. R |-> { f e. ( U. R ^m A ) | ( f " k ) C_ v } ) = ( k e. ( ~P A i^i Fin ) , v e. R |-> { f e. ( U. R ^m A ) | ( f " k ) C_ v } )
33 32 rnmpo 
 |-  ran ( k e. ( ~P A i^i Fin ) , v e. R |-> { f e. ( U. R ^m A ) | ( f " k ) C_ v } ) = { x | E. k e. ( ~P A i^i Fin ) E. v e. R x = { f e. ( U. R ^m A ) | ( f " k ) C_ v } }
34 31 33 eqtrdi 
 |-  ( ( R e. Top /\ A e. V ) -> ran ( k e. { x e. ~P A | ( ~P A |`t x ) e. Comp } , v e. R |-> { f e. ( ~P A Cn R ) | ( f " k ) C_ v } ) = { x | E. k e. ( ~P A i^i Fin ) E. v e. R x = { f e. ( U. R ^m A ) | ( f " k ) C_ v } } )
35 elmapi 
 |-  ( f e. ( U. R ^m A ) -> f : A --> U. R )
36 eleq2 
 |-  ( v = if ( x e. k , v , U. R ) -> ( ( f ` x ) e. v <-> ( f ` x ) e. if ( x e. k , v , U. R ) ) )
37 36 imbi2d 
 |-  ( v = if ( x e. k , v , U. R ) -> ( ( x e. A -> ( f ` x ) e. v ) <-> ( x e. A -> ( f ` x ) e. if ( x e. k , v , U. R ) ) ) )
38 37 bibi1d 
 |-  ( v = if ( x e. k , v , U. R ) -> ( ( ( x e. A -> ( f ` x ) e. v ) <-> ( x e. k -> ( f ` x ) e. v ) ) <-> ( ( x e. A -> ( f ` x ) e. if ( x e. k , v , U. R ) ) <-> ( x e. k -> ( f ` x ) e. v ) ) ) )
39 eleq2 
 |-  ( U. R = if ( x e. k , v , U. R ) -> ( ( f ` x ) e. U. R <-> ( f ` x ) e. if ( x e. k , v , U. R ) ) )
40 39 imbi2d 
 |-  ( U. R = if ( x e. k , v , U. R ) -> ( ( x e. A -> ( f ` x ) e. U. R ) <-> ( x e. A -> ( f ` x ) e. if ( x e. k , v , U. R ) ) ) )
41 40 bibi1d 
 |-  ( U. R = if ( x e. k , v , U. R ) -> ( ( ( x e. A -> ( f ` x ) e. U. R ) <-> ( x e. k -> ( f ` x ) e. v ) ) <-> ( ( x e. A -> ( f ` x ) e. if ( x e. k , v , U. R ) ) <-> ( x e. k -> ( f ` x ) e. v ) ) ) )
42 simprl 
 |-  ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) -> k e. ( ~P A i^i Fin ) )
43 42 elin1d 
 |-  ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) -> k e. ~P A )
44 43 elpwid 
 |-  ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) -> k C_ A )
45 44 adantr 
 |-  ( ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) /\ f : A --> U. R ) -> k C_ A )
46 45 sselda 
 |-  ( ( ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) /\ f : A --> U. R ) /\ x e. k ) -> x e. A )
47 simpr 
 |-  ( ( ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) /\ f : A --> U. R ) /\ x e. k ) -> x e. k )
48 46 47 2thd 
 |-  ( ( ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) /\ f : A --> U. R ) /\ x e. k ) -> ( x e. A <-> x e. k ) )
49 48 imbi1d 
 |-  ( ( ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) /\ f : A --> U. R ) /\ x e. k ) -> ( ( x e. A -> ( f ` x ) e. v ) <-> ( x e. k -> ( f ` x ) e. v ) ) )
50 ffvelrn 
 |-  ( ( f : A --> U. R /\ x e. A ) -> ( f ` x ) e. U. R )
51 50 ex 
 |-  ( f : A --> U. R -> ( x e. A -> ( f ` x ) e. U. R ) )
52 51 adantl 
 |-  ( ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) /\ f : A --> U. R ) -> ( x e. A -> ( f ` x ) e. U. R ) )
53 52 adantr 
 |-  ( ( ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) /\ f : A --> U. R ) /\ -. x e. k ) -> ( x e. A -> ( f ` x ) e. U. R ) )
54 pm2.21 
 |-  ( -. x e. k -> ( x e. k -> ( f ` x ) e. v ) )
55 54 adantl 
 |-  ( ( ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) /\ f : A --> U. R ) /\ -. x e. k ) -> ( x e. k -> ( f ` x ) e. v ) )
56 53 55 2thd 
 |-  ( ( ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) /\ f : A --> U. R ) /\ -. x e. k ) -> ( ( x e. A -> ( f ` x ) e. U. R ) <-> ( x e. k -> ( f ` x ) e. v ) ) )
57 38 41 49 56 ifbothda 
 |-  ( ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) /\ f : A --> U. R ) -> ( ( x e. A -> ( f ` x ) e. if ( x e. k , v , U. R ) ) <-> ( x e. k -> ( f ` x ) e. v ) ) )
58 57 ralbidv2 
 |-  ( ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) /\ f : A --> U. R ) -> ( A. x e. A ( f ` x ) e. if ( x e. k , v , U. R ) <-> A. x e. k ( f ` x ) e. v ) )
59 ffn 
 |-  ( f : A --> U. R -> f Fn A )
60 59 adantl 
 |-  ( ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) /\ f : A --> U. R ) -> f Fn A )
61 vex 
 |-  f e. _V
62 61 elixp 
 |-  ( f e. X_ x e. A if ( x e. k , v , U. R ) <-> ( f Fn A /\ A. x e. A ( f ` x ) e. if ( x e. k , v , U. R ) ) )
63 62 baib 
 |-  ( f Fn A -> ( f e. X_ x e. A if ( x e. k , v , U. R ) <-> A. x e. A ( f ` x ) e. if ( x e. k , v , U. R ) ) )
64 60 63 syl 
 |-  ( ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) /\ f : A --> U. R ) -> ( f e. X_ x e. A if ( x e. k , v , U. R ) <-> A. x e. A ( f ` x ) e. if ( x e. k , v , U. R ) ) )
65 ffun 
 |-  ( f : A --> U. R -> Fun f )
66 fdm 
 |-  ( f : A --> U. R -> dom f = A )
67 66 adantl 
 |-  ( ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) /\ f : A --> U. R ) -> dom f = A )
68 45 67 sseqtrrd 
 |-  ( ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) /\ f : A --> U. R ) -> k C_ dom f )
69 funimass4 
 |-  ( ( Fun f /\ k C_ dom f ) -> ( ( f " k ) C_ v <-> A. x e. k ( f ` x ) e. v ) )
70 65 68 69 syl2an2 
 |-  ( ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) /\ f : A --> U. R ) -> ( ( f " k ) C_ v <-> A. x e. k ( f ` x ) e. v ) )
71 58 64 70 3bitr4d 
 |-  ( ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) /\ f : A --> U. R ) -> ( f e. X_ x e. A if ( x e. k , v , U. R ) <-> ( f " k ) C_ v ) )
72 35 71 sylan2 
 |-  ( ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) /\ f e. ( U. R ^m A ) ) -> ( f e. X_ x e. A if ( x e. k , v , U. R ) <-> ( f " k ) C_ v ) )
73 72 rabbi2dva 
 |-  ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) -> ( ( U. R ^m A ) i^i X_ x e. A if ( x e. k , v , U. R ) ) = { f e. ( U. R ^m A ) | ( f " k ) C_ v } )
74 elssuni 
 |-  ( v e. R -> v C_ U. R )
75 74 ad2antll 
 |-  ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) -> v C_ U. R )
76 ssid 
 |-  U. R C_ U. R
77 sseq1 
 |-  ( v = if ( x e. k , v , U. R ) -> ( v C_ U. R <-> if ( x e. k , v , U. R ) C_ U. R ) )
78 sseq1 
 |-  ( U. R = if ( x e. k , v , U. R ) -> ( U. R C_ U. R <-> if ( x e. k , v , U. R ) C_ U. R ) )
79 77 78 ifboth 
 |-  ( ( v C_ U. R /\ U. R C_ U. R ) -> if ( x e. k , v , U. R ) C_ U. R )
80 75 76 79 sylancl 
 |-  ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) -> if ( x e. k , v , U. R ) C_ U. R )
81 80 ralrimivw 
 |-  ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) -> A. x e. A if ( x e. k , v , U. R ) C_ U. R )
82 ss2ixp 
 |-  ( A. x e. A if ( x e. k , v , U. R ) C_ U. R -> X_ x e. A if ( x e. k , v , U. R ) C_ X_ x e. A U. R )
83 81 82 syl 
 |-  ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) -> X_ x e. A if ( x e. k , v , U. R ) C_ X_ x e. A U. R )
84 simplr 
 |-  ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) -> A e. V )
85 uniexg 
 |-  ( R e. Top -> U. R e. _V )
86 85 ad2antrr 
 |-  ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) -> U. R e. _V )
87 ixpconstg 
 |-  ( ( A e. V /\ U. R e. _V ) -> X_ x e. A U. R = ( U. R ^m A ) )
88 84 86 87 syl2anc 
 |-  ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) -> X_ x e. A U. R = ( U. R ^m A ) )
89 83 88 sseqtrd 
 |-  ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) -> X_ x e. A if ( x e. k , v , U. R ) C_ ( U. R ^m A ) )
90 sseqin2 
 |-  ( X_ x e. A if ( x e. k , v , U. R ) C_ ( U. R ^m A ) <-> ( ( U. R ^m A ) i^i X_ x e. A if ( x e. k , v , U. R ) ) = X_ x e. A if ( x e. k , v , U. R ) )
91 89 90 sylib 
 |-  ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) -> ( ( U. R ^m A ) i^i X_ x e. A if ( x e. k , v , U. R ) ) = X_ x e. A if ( x e. k , v , U. R ) )
92 73 91 eqtr3d 
 |-  ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) -> { f e. ( U. R ^m A ) | ( f " k ) C_ v } = X_ x e. A if ( x e. k , v , U. R ) )
93 10 ad2antrr 
 |-  ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) -> ( A X. { R } ) : A --> Top )
94 42 elin2d 
 |-  ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) -> k e. Fin )
95 simplrr 
 |-  ( ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) /\ x e. A ) -> v e. R )
96 eqid 
 |-  U. R = U. R
97 96 topopn 
 |-  ( R e. Top -> U. R e. R )
98 97 ad3antrrr 
 |-  ( ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) /\ x e. A ) -> U. R e. R )
99 95 98 ifcld 
 |-  ( ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) /\ x e. A ) -> if ( x e. k , v , U. R ) e. R )
100 fvconst2g 
 |-  ( ( R e. Top /\ x e. A ) -> ( ( A X. { R } ) ` x ) = R )
101 100 ad4ant14 
 |-  ( ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) /\ x e. A ) -> ( ( A X. { R } ) ` x ) = R )
102 99 101 eleqtrrd 
 |-  ( ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) /\ x e. A ) -> if ( x e. k , v , U. R ) e. ( ( A X. { R } ) ` x ) )
103 eldifn 
 |-  ( x e. ( A \ k ) -> -. x e. k )
104 103 iffalsed 
 |-  ( x e. ( A \ k ) -> if ( x e. k , v , U. R ) = U. R )
105 104 adantl 
 |-  ( ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) /\ x e. ( A \ k ) ) -> if ( x e. k , v , U. R ) = U. R )
106 eldifi 
 |-  ( x e. ( A \ k ) -> x e. A )
107 106 101 sylan2 
 |-  ( ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) /\ x e. ( A \ k ) ) -> ( ( A X. { R } ) ` x ) = R )
108 107 unieqd 
 |-  ( ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) /\ x e. ( A \ k ) ) -> U. ( ( A X. { R } ) ` x ) = U. R )
109 105 108 eqtr4d 
 |-  ( ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) /\ x e. ( A \ k ) ) -> if ( x e. k , v , U. R ) = U. ( ( A X. { R } ) ` x ) )
110 84 93 94 102 109 ptopn 
 |-  ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) -> X_ x e. A if ( x e. k , v , U. R ) e. ( Xt_ ` ( A X. { R } ) ) )
111 92 110 eqeltrd 
 |-  ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) -> { f e. ( U. R ^m A ) | ( f " k ) C_ v } e. ( Xt_ ` ( A X. { R } ) ) )
112 eleq1 
 |-  ( x = { f e. ( U. R ^m A ) | ( f " k ) C_ v } -> ( x e. ( Xt_ ` ( A X. { R } ) ) <-> { f e. ( U. R ^m A ) | ( f " k ) C_ v } e. ( Xt_ ` ( A X. { R } ) ) ) )
113 111 112 syl5ibrcom 
 |-  ( ( ( R e. Top /\ A e. V ) /\ ( k e. ( ~P A i^i Fin ) /\ v e. R ) ) -> ( x = { f e. ( U. R ^m A ) | ( f " k ) C_ v } -> x e. ( Xt_ ` ( A X. { R } ) ) ) )
114 113 rexlimdvva 
 |-  ( ( R e. Top /\ A e. V ) -> ( E. k e. ( ~P A i^i Fin ) E. v e. R x = { f e. ( U. R ^m A ) | ( f " k ) C_ v } -> x e. ( Xt_ ` ( A X. { R } ) ) ) )
115 114 abssdv 
 |-  ( ( R e. Top /\ A e. V ) -> { x | E. k e. ( ~P A i^i Fin ) E. v e. R x = { f e. ( U. R ^m A ) | ( f " k ) C_ v } } C_ ( Xt_ ` ( A X. { R } ) ) )
116 34 115 eqsstrd 
 |-  ( ( R e. Top /\ A e. V ) -> ran ( k e. { x e. ~P A | ( ~P A |`t x ) e. Comp } , v e. R |-> { f e. ( ~P A Cn R ) | ( f " k ) C_ v } ) C_ ( Xt_ ` ( A X. { R } ) ) )
117 tgfiss 
 |-  ( ( ( Xt_ ` ( A X. { R } ) ) e. Top /\ ran ( k e. { x e. ~P A | ( ~P A |`t x ) e. Comp } , v e. R |-> { f e. ( ~P A Cn R ) | ( f " k ) C_ v } ) C_ ( Xt_ ` ( A X. { R } ) ) ) -> ( topGen ` ( fi ` ran ( k e. { x e. ~P A | ( ~P A |`t x ) e. Comp } , v e. R |-> { f e. ( ~P A Cn R ) | ( f " k ) C_ v } ) ) ) C_ ( Xt_ ` ( A X. { R } ) ) )
118 13 116 117 syl2anc 
 |-  ( ( R e. Top /\ A e. V ) -> ( topGen ` ( fi ` ran ( k e. { x e. ~P A | ( ~P A |`t x ) e. Comp } , v e. R |-> { f e. ( ~P A Cn R ) | ( f " k ) C_ v } ) ) ) C_ ( Xt_ ` ( A X. { R } ) ) )
119 8 118 eqsstrd 
 |-  ( ( R e. Top /\ A e. V ) -> ( R ^ko ~P A ) C_ ( Xt_ ` ( A X. { R } ) ) )
120 eqid 
 |-  ( Xt_ ` ( A X. { R } ) ) = ( Xt_ ` ( A X. { R } ) )
121 120 96 ptuniconst 
 |-  ( ( A e. V /\ R e. Top ) -> ( U. R ^m A ) = U. ( Xt_ ` ( A X. { R } ) ) )
122 121 ancoms 
 |-  ( ( R e. Top /\ A e. V ) -> ( U. R ^m A ) = U. ( Xt_ ` ( A X. { R } ) ) )
123 28 122 eqtrd 
 |-  ( ( R e. Top /\ A e. V ) -> ( ~P A Cn R ) = U. ( Xt_ ` ( A X. { R } ) ) )
124 123 oveq2d 
 |-  ( ( R e. Top /\ A e. V ) -> ( ( Xt_ ` ( A X. { R } ) ) |`t ( ~P A Cn R ) ) = ( ( Xt_ ` ( A X. { R } ) ) |`t U. ( Xt_ ` ( A X. { R } ) ) ) )
125 eqid 
 |-  U. ( Xt_ ` ( A X. { R } ) ) = U. ( Xt_ ` ( A X. { R } ) )
126 125 restid 
 |-  ( ( Xt_ ` ( A X. { R } ) ) e. Top -> ( ( Xt_ ` ( A X. { R } ) ) |`t U. ( Xt_ ` ( A X. { R } ) ) ) = ( Xt_ ` ( A X. { R } ) ) )
127 13 126 syl 
 |-  ( ( R e. Top /\ A e. V ) -> ( ( Xt_ ` ( A X. { R } ) ) |`t U. ( Xt_ ` ( A X. { R } ) ) ) = ( Xt_ ` ( A X. { R } ) ) )
128 124 127 eqtrd 
 |-  ( ( R e. Top /\ A e. V ) -> ( ( Xt_ ` ( A X. { R } ) ) |`t ( ~P A Cn R ) ) = ( Xt_ ` ( A X. { R } ) ) )
129 4 120 xkoptsub 
 |-  ( ( ~P A e. Top /\ R e. Top ) -> ( ( Xt_ ` ( A X. { R } ) ) |`t ( ~P A Cn R ) ) C_ ( R ^ko ~P A ) )
130 1 2 129 syl2an2 
 |-  ( ( R e. Top /\ A e. V ) -> ( ( Xt_ ` ( A X. { R } ) ) |`t ( ~P A Cn R ) ) C_ ( R ^ko ~P A ) )
131 128 130 eqsstrrd 
 |-  ( ( R e. Top /\ A e. V ) -> ( Xt_ ` ( A X. { R } ) ) C_ ( R ^ko ~P A ) )
132 119 131 eqssd 
 |-  ( ( R e. Top /\ A e. V ) -> ( R ^ko ~P A ) = ( Xt_ ` ( A X. { R } ) ) )