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 ) ) )