Metamath Proof Explorer

Theorem xkoco2cn

Description: If F is a continuous function, then g |-> F o. g is a continuous function on function spaces. (Contributed by Mario Carneiro, 23-Mar-2015)

Ref Expression
Hypotheses xkoco2cn.r 
|- ( ph -> R e. Top )
xkoco2cn.f 
|- ( ph -> F e. ( S Cn T ) )
Assertion xkoco2cn 
|- ( ph -> ( g e. ( R Cn S ) |-> ( F o. g ) ) e. ( ( S ^ko R ) Cn ( T ^ko R ) ) )

Proof

Step Hyp Ref Expression
1 xkoco2cn.r 
 |-  ( ph -> R e. Top )
2 xkoco2cn.f 
 |-  ( ph -> F e. ( S Cn T ) )
3 simpr 
 |-  ( ( ph /\ g e. ( R Cn S ) ) -> g e. ( R Cn S ) )
4 2 adantr 
 |-  ( ( ph /\ g e. ( R Cn S ) ) -> F e. ( S Cn T ) )
5 cnco 
 |-  ( ( g e. ( R Cn S ) /\ F e. ( S Cn T ) ) -> ( F o. g ) e. ( R Cn T ) )
6 3 4 5 syl2anc 
 |-  ( ( ph /\ g e. ( R Cn S ) ) -> ( F o. g ) e. ( R Cn T ) )
7 6 fmpttd 
 |-  ( ph -> ( g e. ( R Cn S ) |-> ( F o. g ) ) : ( R Cn S ) --> ( R Cn T ) )
8 eqid 
 |-  U. R = U. R
9 eqid 
 |-  { y e. ~P U. R | ( R |`t y ) e. Comp } = { y e. ~P U. R | ( R |`t y ) e. Comp }
10 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 } )
11 8 9 10 xkobval 
 |-  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. ~P U. R E. v e. T ( ( R |`t k ) e. Comp /\ x = { h e. ( R Cn T ) | ( h " k ) C_ v } ) }
12 11 abeq2i 
 |-  ( 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 E. v e. T ( ( R |`t k ) e. Comp /\ x = { h e. ( R Cn T ) | ( h " k ) C_ v } ) )
13 simpr 
 |-  ( ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) /\ g e. ( R Cn S ) ) -> g e. ( R Cn S ) )
14 2 ad3antrrr 
 |-  ( ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) /\ g e. ( R Cn S ) ) -> F e. ( S Cn T ) )
15 13 14 5 syl2anc 
 |-  ( ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) /\ g e. ( R Cn S ) ) -> ( F o. g ) e. ( R Cn T ) )
16 imaeq1 
 |-  ( h = ( F o. g ) -> ( h " k ) = ( ( F o. g ) " k ) )
17 imaco 
 |-  ( ( F o. g ) " k ) = ( F " ( g " k ) )
18 16 17 eqtrdi 
 |-  ( h = ( F o. g ) -> ( h " k ) = ( F " ( g " k ) ) )
19 18 sseq1d 
 |-  ( h = ( F o. g ) -> ( ( h " k ) C_ v <-> ( F " ( g " k ) ) C_ v ) )
20 19 elrab3 
 |-  ( ( F o. g ) e. ( R Cn T ) -> ( ( F o. g ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } <-> ( F " ( g " k ) ) C_ v ) )
21 15 20 syl 
 |-  ( ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) /\ g e. ( R Cn S ) ) -> ( ( F o. g ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } <-> ( F " ( g " k ) ) C_ v ) )
22 eqid 
 |-  U. S = U. S
23 eqid 
 |-  U. T = U. T
24 22 23 cnf 
 |-  ( F e. ( S Cn T ) -> F : U. S --> U. T )
25 2 24 syl 
 |-  ( ph -> F : U. S --> U. T )
26 25 ad3antrrr 
 |-  ( ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) /\ g e. ( R Cn S ) ) -> F : U. S --> U. T )
27 26 ffund 
 |-  ( ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) /\ g e. ( R Cn S ) ) -> Fun F )
28 imassrn 
 |-  ( g " k ) C_ ran g
29 8 22 cnf 
 |-  ( g e. ( R Cn S ) -> g : U. R --> U. S )
30 13 29 syl 
 |-  ( ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) /\ g e. ( R Cn S ) ) -> g : U. R --> U. S )
31 30 frnd 
 |-  ( ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) /\ g e. ( R Cn S ) ) -> ran g C_ U. S )
32 28 31 sstrid 
 |-  ( ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) /\ g e. ( R Cn S ) ) -> ( g " k ) C_ U. S )
33 26 fdmd 
 |-  ( ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) /\ g e. ( R Cn S ) ) -> dom F = U. S )
34 32 33 sseqtrrd 
 |-  ( ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) /\ g e. ( R Cn S ) ) -> ( g " k ) C_ dom F )
35 funimass3 
 |-  ( ( Fun F /\ ( g " k ) C_ dom F ) -> ( ( F " ( g " k ) ) C_ v <-> ( g " k ) C_ ( `' F " v ) ) )
36 27 34 35 syl2anc 
 |-  ( ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) /\ g e. ( R Cn S ) ) -> ( ( F " ( g " k ) ) C_ v <-> ( g " k ) C_ ( `' F " v ) ) )
37 21 36 bitrd 
 |-  ( ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) /\ g e. ( R Cn S ) ) -> ( ( F o. g ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } <-> ( g " k ) C_ ( `' F " v ) ) )
38 37 rabbidva 
 |-  ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) -> { g e. ( R Cn S ) | ( F o. g ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } } = { g e. ( R Cn S ) | ( g " k ) C_ ( `' F " v ) } )
39 1 ad2antrr 
 |-  ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) -> R e. Top )
40 cntop1 
 |-  ( F e. ( S Cn T ) -> S e. Top )
41 2 40 syl 
 |-  ( ph -> S e. Top )
42 41 ad2antrr 
 |-  ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) -> S e. Top )
43 simplrl 
 |-  ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) -> k e. ~P U. R )
44 43 elpwid 
 |-  ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) -> k C_ U. R )
45 simpr 
 |-  ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) -> ( R |`t k ) e. Comp )
46 2 ad2antrr 
 |-  ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) -> F e. ( S Cn T ) )
47 simplrr 
 |-  ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) -> v e. T )
48 cnima 
 |-  ( ( F e. ( S Cn T ) /\ v e. T ) -> ( `' F " v ) e. S )
49 46 47 48 syl2anc 
 |-  ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) -> ( `' F " v ) e. S )
50 8 39 42 44 45 49 xkoopn 
 |-  ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) -> { g e. ( R Cn S ) | ( g " k ) C_ ( `' F " v ) } e. ( S ^ko R ) )
51 38 50 eqeltrd 
 |-  ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) -> { g e. ( R Cn S ) | ( F o. g ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } } e. ( S ^ko R ) )
52 imaeq2 
 |-  ( x = { h e. ( R Cn T ) | ( h " k ) C_ v } -> ( `' ( g e. ( R Cn S ) |-> ( F o. g ) ) " x ) = ( `' ( g e. ( R Cn S ) |-> ( F o. g ) ) " { h e. ( R Cn T ) | ( h " k ) C_ v } ) )
53 eqid 
 |-  ( g e. ( R Cn S ) |-> ( F o. g ) ) = ( g e. ( R Cn S ) |-> ( F o. g ) )
54 53 mptpreima 
 |-  ( `' ( g e. ( R Cn S ) |-> ( F o. g ) ) " { h e. ( R Cn T ) | ( h " k ) C_ v } ) = { g e. ( R Cn S ) | ( F o. g ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } }
55 52 54 eqtrdi 
 |-  ( x = { h e. ( R Cn T ) | ( h " k ) C_ v } -> ( `' ( g e. ( R Cn S ) |-> ( F o. g ) ) " x ) = { g e. ( R Cn S ) | ( F o. g ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } } )
56 55 eleq1d 
 |-  ( x = { h e. ( R Cn T ) | ( h " k ) C_ v } -> ( ( `' ( g e. ( R Cn S ) |-> ( F o. g ) ) " x ) e. ( S ^ko R ) <-> { g e. ( R Cn S ) | ( F o. g ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } } e. ( S ^ko R ) ) )
57 51 56 syl5ibrcom 
 |-  ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) -> ( x = { h e. ( R Cn T ) | ( h " k ) C_ v } -> ( `' ( g e. ( R Cn S ) |-> ( F o. g ) ) " x ) e. ( S ^ko R ) ) )
58 57 expimpd 
 |-  ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) -> ( ( ( R |`t k ) e. Comp /\ x = { h e. ( R Cn T ) | ( h " k ) C_ v } ) -> ( `' ( g e. ( R Cn S ) |-> ( F o. g ) ) " x ) e. ( S ^ko R ) ) )
59 58 rexlimdvva 
 |-  ( ph -> ( E. k e. ~P U. R E. v e. T ( ( R |`t k ) e. Comp /\ x = { h e. ( R Cn T ) | ( h " k ) C_ v } ) -> ( `' ( g e. ( R Cn S ) |-> ( F o. g ) ) " x ) e. ( S ^ko R ) ) )
60 12 59 syl5bi 
 |-  ( ph -> ( 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 } ) -> ( `' ( g e. ( R Cn S ) |-> ( F o. g ) ) " x ) e. ( S ^ko R ) ) )
61 60 ralrimiv 
 |-  ( ph -> 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 } ) ( `' ( g e. ( R Cn S ) |-> ( F o. g ) ) " x ) e. ( S ^ko R ) )
62 eqid 
 |-  ( S ^ko R ) = ( S ^ko R )
63 62 xkotopon 
 |-  ( ( R e. Top /\ S e. Top ) -> ( S ^ko R ) e. ( TopOn ` ( R Cn S ) ) )
64 1 41 63 syl2anc 
 |-  ( ph -> ( S ^ko R ) e. ( TopOn ` ( R Cn S ) ) )
65 ovex 
 |-  ( R Cn T ) e. _V
66 65 pwex 
 |-  ~P ( R Cn T ) e. _V
67 8 9 10 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 )
68 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 ) )
69 67 68 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 )
70 66 69 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
71 70 a1i 
 |-  ( ph -> 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 )
72 cntop2 
 |-  ( F e. ( S Cn T ) -> T e. Top )
73 2 72 syl 
 |-  ( ph -> T e. Top )
74 8 9 10 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 } ) ) ) )
75 1 73 74 syl2anc 
 |-  ( ph -> ( 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 } ) ) ) )
76 eqid 
 |-  ( T ^ko R ) = ( T ^ko R )
77 76 xkotopon 
 |-  ( ( R e. Top /\ T e. Top ) -> ( T ^ko R ) e. ( TopOn ` ( R Cn T ) ) )
78 1 73 77 syl2anc 
 |-  ( ph -> ( T ^ko R ) e. ( TopOn ` ( R Cn T ) ) )
79 64 71 75 78 subbascn 
 |-  ( ph -> ( ( g e. ( R Cn S ) |-> ( F o. g ) ) e. ( ( S ^ko R ) Cn ( T ^ko R ) ) <-> ( ( g e. ( R Cn S ) |-> ( F o. g ) ) : ( 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 } ) ( `' ( g e. ( R Cn S ) |-> ( F o. g ) ) " x ) e. ( S ^ko R ) ) ) )
80 7 61 79 mpbir2and 
 |-  ( ph -> ( g e. ( R Cn S ) |-> ( F o. g ) ) e. ( ( S ^ko R ) Cn ( T ^ko R ) ) )