Metamath Proof Explorer

Theorem xkococn

Description: Continuity of the composition operation as a function on continuous function spaces. (Contributed by Mario Carneiro, 20-Mar-2015) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypothesis xkococn.1 
|- F = ( f e. ( S Cn T ) , g e. ( R Cn S ) |-> ( f o. g ) )
Assertion xkococn 
|- ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> F e. ( ( ( T ^ko S ) tX ( S ^ko R ) ) Cn ( T ^ko R ) ) )

Proof

Step Hyp Ref Expression
1 xkococn.1 
 |-  F = ( f e. ( S Cn T ) , g e. ( R Cn S ) |-> ( f o. g ) )
2 simprr 
 |-  ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( f e. ( S Cn T ) /\ g e. ( R Cn S ) ) ) -> g e. ( R Cn S ) )
3 simprl 
 |-  ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( f e. ( S Cn T ) /\ g e. ( R Cn S ) ) ) -> f e. ( S Cn T ) )
4 cnco 
 |-  ( ( g e. ( R Cn S ) /\ f e. ( S Cn T ) ) -> ( f o. g ) e. ( R Cn T ) )
5 2 3 4 syl2anc 
 |-  ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( f e. ( S Cn T ) /\ g e. ( R Cn S ) ) ) -> ( f o. g ) e. ( R Cn T ) )
6 5 ralrimivva 
 |-  ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> A. f e. ( S Cn T ) A. g e. ( R Cn S ) ( f o. g ) e. ( R Cn T ) )
7 1 fmpo 
 |-  ( A. f e. ( S Cn T ) A. g e. ( R Cn S ) ( f o. g ) e. ( R Cn T ) <-> F : ( ( S Cn T ) X. ( R Cn S ) ) --> ( R Cn T ) )
8 6 7 sylib 
 |-  ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> F : ( ( S Cn T ) X. ( R Cn S ) ) --> ( R Cn T ) )
9 eqid 
 |-  ( k e. { y e. ~P U. R | ( R |`t y ) e. Comp } , v e. T |-> { h e. ( R Cn T ) | ( h " k ) C_ v } ) = ( k e. { y e. ~P U. R | ( R |`t y ) e. Comp } , v e. T |-> { h e. ( R Cn T ) | ( h " k ) C_ v } )
10 9 rnmpo 
 |-  ran ( k e. { y e. ~P U. R | ( R |`t y ) e. Comp } , v e. T |-> { h e. ( R Cn T ) | ( h " k ) C_ v } ) = { x | E. k e. { y e. ~P U. R | ( R |`t y ) e. Comp } E. v e. T x = { h e. ( R Cn T ) | ( h " k ) C_ v } }
11 10 eleq2i 
 |-  ( x e. ran ( k e. { y e. ~P U. R | ( R |`t y ) e. Comp } , v e. T |-> { h e. ( R Cn T ) | ( h " k ) C_ v } ) <-> x e. { x | E. k e. { y e. ~P U. R | ( R |`t y ) e. Comp } E. v e. T x = { h e. ( R Cn T ) | ( h " k ) C_ v } } )
12 abid 
 |-  ( x e. { x | E. k e. { y e. ~P U. R | ( R |`t y ) e. Comp } E. v e. T x = { h e. ( R Cn T ) | ( h " k ) C_ v } } <-> E. k e. { y e. ~P U. R | ( R |`t y ) e. Comp } E. v e. T x = { h e. ( R Cn T ) | ( h " k ) C_ v } )
13 oveq2 
 |-  ( y = k -> ( R |`t y ) = ( R |`t k ) )
14 13 eleq1d 
 |-  ( y = k -> ( ( R |`t y ) e. Comp <-> ( R |`t k ) e. Comp ) )
15 14 rexrab 
 |-  ( E. k e. { y e. ~P U. R | ( R |`t y ) e. Comp } E. v e. T x = { h e. ( R Cn T ) | ( h " k ) C_ v } <-> E. k e. ~P U. R ( ( R |`t k ) e. Comp /\ E. v e. T x = { h e. ( R Cn T ) | ( h " k ) C_ v } ) )
16 11 12 15 3bitri 
 |-  ( x e. ran ( k e. { y e. ~P U. R | ( R |`t y ) e. Comp } , v e. T |-> { h e. ( R Cn T ) | ( h " k ) C_ v } ) <-> E. k e. ~P U. R ( ( R |`t k ) e. Comp /\ E. v e. T x = { h e. ( R Cn T ) | ( h " k ) C_ v } ) )
17 8 ad2antrr 
 |-  ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) -> F : ( ( S Cn T ) X. ( R Cn S ) ) --> ( R Cn T ) )
18 ffn 
 |-  ( F : ( ( S Cn T ) X. ( R Cn S ) ) --> ( R Cn T ) -> F Fn ( ( S Cn T ) X. ( R Cn S ) ) )
19 elpreima 
 |-  ( F Fn ( ( S Cn T ) X. ( R Cn S ) ) -> ( y e. ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) <-> ( y e. ( ( S Cn T ) X. ( R Cn S ) ) /\ ( F ` y ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) )
20 17 18 19 3syl 
 |-  ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) -> ( y e. ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) <-> ( y e. ( ( S Cn T ) X. ( R Cn S ) ) /\ ( F ` y ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) )
21 coeq1 
 |-  ( f = a -> ( f o. g ) = ( a o. g ) )
22 coeq2 
 |-  ( g = b -> ( a o. g ) = ( a o. b ) )
23 vex 
 |-  a e. _V
24 vex 
 |-  b e. _V
25 23 24 coex 
 |-  ( a o. b ) e. _V
26 21 22 1 25 ovmpo 
 |-  ( ( a e. ( S Cn T ) /\ b e. ( R Cn S ) ) -> ( a F b ) = ( a o. b ) )
27 26 adantl 
 |-  ( ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) /\ ( a e. ( S Cn T ) /\ b e. ( R Cn S ) ) ) -> ( a F b ) = ( a o. b ) )
28 27 eleq1d 
 |-  ( ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) /\ ( a e. ( S Cn T ) /\ b e. ( R Cn S ) ) ) -> ( ( a F b ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } <-> ( a o. b ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } ) )
29 imaeq1 
 |-  ( h = ( a o. b ) -> ( h " k ) = ( ( a o. b ) " k ) )
30 29 sseq1d 
 |-  ( h = ( a o. b ) -> ( ( h " k ) C_ v <-> ( ( a o. b ) " k ) C_ v ) )
31 30 elrab 
 |-  ( ( a o. b ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } <-> ( ( a o. b ) e. ( R Cn T ) /\ ( ( a o. b ) " k ) C_ v ) )
32 31 simprbi 
 |-  ( ( a o. b ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } -> ( ( a o. b ) " k ) C_ v )
33 simp2 
 |-  ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> S e. N-Locally Comp )
34 33 ad3antrrr 
 |-  ( ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) /\ ( ( a e. ( S Cn T ) /\ b e. ( R Cn S ) ) /\ ( ( a o. b ) " k ) C_ v ) ) -> S e. N-Locally Comp )
35 elpwi 
 |-  ( k e. ~P U. R -> k C_ U. R )
36 35 ad2antrl 
 |-  ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) -> k C_ U. R )
37 36 ad2antrr 
 |-  ( ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) /\ ( ( a e. ( S Cn T ) /\ b e. ( R Cn S ) ) /\ ( ( a o. b ) " k ) C_ v ) ) -> k C_ U. R )
38 simprr 
 |-  ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) -> ( R |`t k ) e. Comp )
39 38 ad2antrr 
 |-  ( ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) /\ ( ( a e. ( S Cn T ) /\ b e. ( R Cn S ) ) /\ ( ( a o. b ) " k ) C_ v ) ) -> ( R |`t k ) e. Comp )
40 simplr 
 |-  ( ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) /\ ( ( a e. ( S Cn T ) /\ b e. ( R Cn S ) ) /\ ( ( a o. b ) " k ) C_ v ) ) -> v e. T )
41 simprll 
 |-  ( ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) /\ ( ( a e. ( S Cn T ) /\ b e. ( R Cn S ) ) /\ ( ( a o. b ) " k ) C_ v ) ) -> a e. ( S Cn T ) )
42 simprlr 
 |-  ( ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) /\ ( ( a e. ( S Cn T ) /\ b e. ( R Cn S ) ) /\ ( ( a o. b ) " k ) C_ v ) ) -> b e. ( R Cn S ) )
43 simprr 
 |-  ( ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) /\ ( ( a e. ( S Cn T ) /\ b e. ( R Cn S ) ) /\ ( ( a o. b ) " k ) C_ v ) ) -> ( ( a o. b ) " k ) C_ v )
44 1 34 37 39 40 41 42 43 xkococnlem 
 |-  ( ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) /\ ( ( a e. ( S Cn T ) /\ b e. ( R Cn S ) ) /\ ( ( a o. b ) " k ) C_ v ) ) -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. a , b >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) )
45 44 expr 
 |-  ( ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) /\ ( a e. ( S Cn T ) /\ b e. ( R Cn S ) ) ) -> ( ( ( a o. b ) " k ) C_ v -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. a , b >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) )
46 32 45 syl5 
 |-  ( ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) /\ ( a e. ( S Cn T ) /\ b e. ( R Cn S ) ) ) -> ( ( a o. b ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. a , b >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) )
47 28 46 sylbid 
 |-  ( ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) /\ ( a e. ( S Cn T ) /\ b e. ( R Cn S ) ) ) -> ( ( a F b ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. a , b >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) )
48 47 ralrimivva 
 |-  ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) -> A. a e. ( S Cn T ) A. b e. ( R Cn S ) ( ( a F b ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. a , b >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) )
49 fveq2 
 |-  ( y = <. a , b >. -> ( F ` y ) = ( F ` <. a , b >. ) )
50 df-ov 
 |-  ( a F b ) = ( F ` <. a , b >. )
51 49 50 eqtr4di 
 |-  ( y = <. a , b >. -> ( F ` y ) = ( a F b ) )
52 51 eleq1d 
 |-  ( y = <. a , b >. -> ( ( F ` y ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } <-> ( a F b ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } ) )
53 eleq1 
 |-  ( y = <. a , b >. -> ( y e. z <-> <. a , b >. e. z ) )
54 53 anbi1d 
 |-  ( y = <. a , b >. -> ( ( y e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) <-> ( <. a , b >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) )
55 54 rexbidv 
 |-  ( y = <. a , b >. -> ( E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( y e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) <-> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. a , b >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) )
56 52 55 imbi12d 
 |-  ( y = <. a , b >. -> ( ( ( F ` y ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( y e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) <-> ( ( a F b ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. a , b >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) ) )
57 56 ralxp 
 |-  ( A. y e. ( ( S Cn T ) X. ( R Cn S ) ) ( ( F ` y ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( y e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) <-> A. a e. ( S Cn T ) A. b e. ( R Cn S ) ( ( a F b ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. a , b >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) )
58 48 57 sylibr 
 |-  ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) -> A. y e. ( ( S Cn T ) X. ( R Cn S ) ) ( ( F ` y ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( y e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) )
59 58 r19.21bi 
 |-  ( ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) /\ y e. ( ( S Cn T ) X. ( R Cn S ) ) ) -> ( ( F ` y ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( y e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) )
60 59 expimpd 
 |-  ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) -> ( ( y e. ( ( S Cn T ) X. ( R Cn S ) ) /\ ( F ` y ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } ) -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( y e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) )
61 20 60 sylbid 
 |-  ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) -> ( y e. ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( y e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) )
62 61 ralrimiv 
 |-  ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) -> A. y e. ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( y e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) )
63 nllytop 
 |-  ( S e. N-Locally Comp -> S e. Top )
64 63 3ad2ant2 
 |-  ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> S e. Top )
65 simp3 
 |-  ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> T e. Top )
66 xkotop 
 |-  ( ( S e. Top /\ T e. Top ) -> ( T ^ko S ) e. Top )
67 64 65 66 syl2anc 
 |-  ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> ( T ^ko S ) e. Top )
68 simp1 
 |-  ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> R e. Top )
69 xkotop 
 |-  ( ( R e. Top /\ S e. Top ) -> ( S ^ko R ) e. Top )
70 68 64 69 syl2anc 
 |-  ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> ( S ^ko R ) e. Top )
71 txtop 
 |-  ( ( ( T ^ko S ) e. Top /\ ( S ^ko R ) e. Top ) -> ( ( T ^ko S ) tX ( S ^ko R ) ) e. Top )
72 67 70 71 syl2anc 
 |-  ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> ( ( T ^ko S ) tX ( S ^ko R ) ) e. Top )
73 72 ad2antrr 
 |-  ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) -> ( ( T ^ko S ) tX ( S ^ko R ) ) e. Top )
74 eltop2 
 |-  ( ( ( T ^ko S ) tX ( S ^ko R ) ) e. Top -> ( ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) e. ( ( T ^ko S ) tX ( S ^ko R ) ) <-> A. y e. ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( y e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) )
75 73 74 syl 
 |-  ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) -> ( ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) e. ( ( T ^ko S ) tX ( S ^ko R ) ) <-> A. y e. ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( y e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) )
76 62 75 mpbird 
 |-  ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) -> ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) e. ( ( T ^ko S ) tX ( S ^ko R ) ) )
77 imaeq2 
 |-  ( x = { h e. ( R Cn T ) | ( h " k ) C_ v } -> ( `' F " x ) = ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) )
78 77 eleq1d 
 |-  ( x = { h e. ( R Cn T ) | ( h " k ) C_ v } -> ( ( `' F " x ) e. ( ( T ^ko S ) tX ( S ^ko R ) ) <-> ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) e. ( ( T ^ko S ) tX ( S ^ko R ) ) ) )
79 76 78 syl5ibrcom 
 |-  ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) -> ( x = { h e. ( R Cn T ) | ( h " k ) C_ v } -> ( `' F " x ) e. ( ( T ^ko S ) tX ( S ^ko R ) ) ) )
80 79 rexlimdva 
 |-  ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) -> ( E. v e. T x = { h e. ( R Cn T ) | ( h " k ) C_ v } -> ( `' F " x ) e. ( ( T ^ko S ) tX ( S ^ko R ) ) ) )
81 80 anassrs 
 |-  ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ k e. ~P U. R ) /\ ( R |`t k ) e. Comp ) -> ( E. v e. T x = { h e. ( R Cn T ) | ( h " k ) C_ v } -> ( `' F " x ) e. ( ( T ^ko S ) tX ( S ^ko R ) ) ) )
82 81 expimpd 
 |-  ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ k e. ~P U. R ) -> ( ( ( R |`t k ) e. Comp /\ E. v e. T x = { h e. ( R Cn T ) | ( h " k ) C_ v } ) -> ( `' F " x ) e. ( ( T ^ko S ) tX ( S ^ko R ) ) ) )
83 82 rexlimdva 
 |-  ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> ( E. k e. ~P U. R ( ( R |`t k ) e. Comp /\ E. v e. T x = { h e. ( R Cn T ) | ( h " k ) C_ v } ) -> ( `' F " x ) e. ( ( T ^ko S ) tX ( S ^ko R ) ) ) )
84 16 83 syl5bi 
 |-  ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> ( x e. ran ( k e. { y e. ~P U. R | ( R |`t y ) e. Comp } , v e. T |-> { h e. ( R Cn T ) | ( h " k ) C_ v } ) -> ( `' F " x ) e. ( ( T ^ko S ) tX ( S ^ko R ) ) ) )
85 84 ralrimiv 
 |-  ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> A. x e. ran ( k e. { y e. ~P U. R | ( R |`t y ) e. Comp } , v e. T |-> { h e. ( R Cn T ) | ( h " k ) C_ v } ) ( `' F " x ) e. ( ( T ^ko S ) tX ( S ^ko R ) ) )
86 eqid 
 |-  ( T ^ko S ) = ( T ^ko S )
87 86 xkotopon 
 |-  ( ( S e. Top /\ T e. Top ) -> ( T ^ko S ) e. ( TopOn ` ( S Cn T ) ) )
88 64 65 87 syl2anc 
 |-  ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> ( T ^ko S ) e. ( TopOn ` ( S Cn T ) ) )
89 eqid 
 |-  ( S ^ko R ) = ( S ^ko R )
90 89 xkotopon 
 |-  ( ( R e. Top /\ S e. Top ) -> ( S ^ko R ) e. ( TopOn ` ( R Cn S ) ) )
91 68 64 90 syl2anc 
 |-  ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> ( S ^ko R ) e. ( TopOn ` ( R Cn S ) ) )
92 txtopon 
 |-  ( ( ( T ^ko S ) e. ( TopOn ` ( S Cn T ) ) /\ ( S ^ko R ) e. ( TopOn ` ( R Cn S ) ) ) -> ( ( T ^ko S ) tX ( S ^ko R ) ) e. ( TopOn ` ( ( S Cn T ) X. ( R Cn S ) ) ) )
93 88 91 92 syl2anc 
 |-  ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> ( ( T ^ko S ) tX ( S ^ko R ) ) e. ( TopOn ` ( ( S Cn T ) X. ( R Cn S ) ) ) )
94 ovex 
 |-  ( R Cn T ) e. _V
95 94 pwex 
 |-  ~P ( R Cn T ) e. _V
96 eqid 
 |-  U. R = U. R
97 eqid 
 |-  { y e. ~P U. R | ( R |`t y ) e. Comp } = { y e. ~P U. R | ( R |`t y ) e. Comp }
98 96 97 9 xkotf 
 |-  ( k e. { y e. ~P U. R | ( R |`t y ) e. Comp } , v e. T |-> { h e. ( R Cn T ) | ( h " k ) C_ v } ) : ( { y e. ~P U. R | ( R |`t y ) e. Comp } X. T ) --> ~P ( R Cn T )
99 frn 
 |-  ( ( k e. { y e. ~P U. R | ( R |`t y ) e. Comp } , v e. T |-> { h e. ( R Cn T ) | ( h " k ) C_ v } ) : ( { y e. ~P U. R | ( R |`t y ) e. Comp } X. T ) --> ~P ( R Cn T ) -> ran ( k e. { y e. ~P U. R | ( R |`t y ) e. Comp } , v e. T |-> { h e. ( R Cn T ) | ( h " k ) C_ v } ) C_ ~P ( R Cn T ) )
100 98 99 ax-mp 
 |-  ran ( k e. { y e. ~P U. R | ( R |`t y ) e. Comp } , v e. T |-> { h e. ( R Cn T ) | ( h " k ) C_ v } ) C_ ~P ( R Cn T )
101 95 100 ssexi 
 |-  ran ( k e. { y e. ~P U. R | ( R |`t y ) e. Comp } , v e. T |-> { h e. ( R Cn T ) | ( h " k ) C_ v } ) e. _V
102 101 a1i 
 |-  ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> ran ( k e. { y e. ~P U. R | ( R |`t y ) e. Comp } , v e. T |-> { h e. ( R Cn T ) | ( h " k ) C_ v } ) e. _V )
103 96 97 9 xkoval 
 |-  ( ( R e. Top /\ T e. Top ) -> ( T ^ko R ) = ( topGen ` ( fi ` ran ( k e. { y e. ~P U. R | ( R |`t y ) e. Comp } , v e. T |-> { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) )
104 103 3adant2 
 |-  ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> ( T ^ko R ) = ( topGen ` ( fi ` ran ( k e. { y e. ~P U. R | ( R |`t y ) e. Comp } , v e. T |-> { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) )
105 eqid 
 |-  ( T ^ko R ) = ( T ^ko R )
106 105 xkotopon 
 |-  ( ( R e. Top /\ T e. Top ) -> ( T ^ko R ) e. ( TopOn ` ( R Cn T ) ) )
107 106 3adant2 
 |-  ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> ( T ^ko R ) e. ( TopOn ` ( R Cn T ) ) )
108 93 102 104 107 subbascn 
 |-  ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> ( F e. ( ( ( T ^ko S ) tX ( S ^ko R ) ) Cn ( T ^ko R ) ) <-> ( F : ( ( S Cn T ) X. ( R Cn S ) ) --> ( R Cn T ) /\ A. x e. ran ( k e. { y e. ~P U. R | ( R |`t y ) e. Comp } , v e. T |-> { h e. ( R Cn T ) | ( h " k ) C_ v } ) ( `' F " x ) e. ( ( T ^ko S ) tX ( S ^ko R ) ) ) ) )
109 8 85 108 mpbir2and 
 |-  ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> F e. ( ( ( T ^ko S ) tX ( S ^ko R ) ) Cn ( T ^ko R ) ) )