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