Metamath Proof Explorer

Theorem xkoco1cn

Description: If F is a continuous function, then g |-> g o. F is a continuous function on function spaces. (The reason we prove this and xkoco2cn independently of the more general xkococn is because that requires some inconvenient extra assumptions on S .) (Contributed by Mario Carneiro, 20-Mar-2015)

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

Proof

Step Hyp Ref Expression
1 xkoco1cn.t 
 |-  ( ph -> T e. Top )
2 xkoco1cn.f 
 |-  ( ph -> F e. ( R Cn S ) )
3 cnco 
 |-  ( ( F e. ( R Cn S ) /\ g e. ( S Cn T ) ) -> ( g o. F ) e. ( R Cn T ) )
4 2 3 sylan 
 |-  ( ( ph /\ g e. ( S Cn T ) ) -> ( g o. F ) e. ( R Cn T ) )
5 4 fmpttd 
 |-  ( ph -> ( g e. ( S Cn T ) |-> ( g o. F ) ) : ( S Cn T ) --> ( R Cn T ) )
6 eqid 
 |-  U. R = U. R
7 eqid 
 |-  { y e. ~P U. R | ( R |`t y ) e. Comp } = { y e. ~P U. R | ( R |`t y ) e. Comp }
8 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 } )
9 6 7 8 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 } ) }
10 9 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 } ) )
11 2 ad2antrr 
 |-  ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) -> F e. ( R Cn S ) )
12 11 3 sylan 
 |-  ( ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) /\ g e. ( S Cn T ) ) -> ( g o. F ) e. ( R Cn T ) )
13 imaeq1 
 |-  ( h = ( g o. F ) -> ( h " k ) = ( ( g o. F ) " k ) )
14 imaco 
 |-  ( ( g o. F ) " k ) = ( g " ( F " k ) )
15 13 14 eqtrdi 
 |-  ( h = ( g o. F ) -> ( h " k ) = ( g " ( F " k ) ) )
16 15 sseq1d 
 |-  ( h = ( g o. F ) -> ( ( h " k ) C_ v <-> ( g " ( F " k ) ) C_ v ) )
17 16 elrab3 
 |-  ( ( g o. F ) e. ( R Cn T ) -> ( ( g o. F ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } <-> ( g " ( F " k ) ) C_ v ) )
18 12 17 syl 
 |-  ( ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) /\ g e. ( S Cn T ) ) -> ( ( g o. F ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } <-> ( g " ( F " k ) ) C_ v ) )
19 18 rabbidva 
 |-  ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) -> { g e. ( S Cn T ) | ( g o. F ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } } = { g e. ( S Cn T ) | ( g " ( F " k ) ) C_ v } )
20 eqid 
 |-  U. S = U. S
21 cntop2 
 |-  ( F e. ( R Cn S ) -> S e. Top )
22 2 21 syl 
 |-  ( ph -> S e. Top )
23 22 ad2antrr 
 |-  ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) -> S e. Top )
24 1 ad2antrr 
 |-  ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) -> T e. Top )
25 imassrn 
 |-  ( F " k ) C_ ran F
26 6 20 cnf 
 |-  ( F e. ( R Cn S ) -> F : U. R --> U. S )
27 frn 
 |-  ( F : U. R --> U. S -> ran F C_ U. S )
28 11 26 27 3syl 
 |-  ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) -> ran F C_ U. S )
29 25 28 sstrid 
 |-  ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) -> ( F " k ) C_ U. S )
30 imacmp 
 |-  ( ( F e. ( R Cn S ) /\ ( R |`t k ) e. Comp ) -> ( S |`t ( F " k ) ) e. Comp )
31 11 30 sylancom 
 |-  ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) -> ( S |`t ( F " k ) ) e. Comp )
32 simplrr 
 |-  ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) -> v e. T )
33 20 23 24 29 31 32 xkoopn 
 |-  ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) -> { g e. ( S Cn T ) | ( g " ( F " k ) ) C_ v } e. ( T ^ko S ) )
34 19 33 eqeltrd 
 |-  ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R |`t k ) e. Comp ) -> { g e. ( S Cn T ) | ( g o. F ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } } e. ( T ^ko S ) )
35 imaeq2 
 |-  ( x = { h e. ( R Cn T ) | ( h " k ) C_ v } -> ( `' ( g e. ( S Cn T ) |-> ( g o. F ) ) " x ) = ( `' ( g e. ( S Cn T ) |-> ( g o. F ) ) " { h e. ( R Cn T ) | ( h " k ) C_ v } ) )
36 eqid 
 |-  ( g e. ( S Cn T ) |-> ( g o. F ) ) = ( g e. ( S Cn T ) |-> ( g o. F ) )
37 36 mptpreima 
 |-  ( `' ( g e. ( S Cn T ) |-> ( g o. F ) ) " { h e. ( R Cn T ) | ( h " k ) C_ v } ) = { g e. ( S Cn T ) | ( g o. F ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } }
38 35 37 eqtrdi 
 |-  ( x = { h e. ( R Cn T ) | ( h " k ) C_ v } -> ( `' ( g e. ( S Cn T ) |-> ( g o. F ) ) " x ) = { g e. ( S Cn T ) | ( g o. F ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } } )
39 38 eleq1d 
 |-  ( x = { h e. ( R Cn T ) | ( h " k ) C_ v } -> ( ( `' ( g e. ( S Cn T ) |-> ( g o. F ) ) " x ) e. ( T ^ko S ) <-> { g e. ( S Cn T ) | ( g o. F ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } } e. ( T ^ko S ) ) )
40 34 39 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. ( S Cn T ) |-> ( g o. F ) ) " x ) e. ( T ^ko S ) ) )
41 40 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. ( S Cn T ) |-> ( g o. F ) ) " x ) e. ( T ^ko S ) ) )
42 41 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. ( S Cn T ) |-> ( g o. F ) ) " x ) e. ( T ^ko S ) ) )
43 10 42 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. ( S Cn T ) |-> ( g o. F ) ) " x ) e. ( T ^ko S ) ) )
44 43 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. ( S Cn T ) |-> ( g o. F ) ) " x ) e. ( T ^ko S ) )
45 eqid 
 |-  ( T ^ko S ) = ( T ^ko S )
46 45 xkotopon 
 |-  ( ( S e. Top /\ T e. Top ) -> ( T ^ko S ) e. ( TopOn ` ( S Cn T ) ) )
47 22 1 46 syl2anc 
 |-  ( ph -> ( T ^ko S ) e. ( TopOn ` ( S Cn T ) ) )
48 ovex 
 |-  ( R Cn T ) e. _V
49 48 pwex 
 |-  ~P ( R Cn T ) e. _V
50 6 7 8 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 )
51 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 ) )
52 50 51 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 )
53 49 52 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
54 53 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 )
55 cntop1 
 |-  ( F e. ( R Cn S ) -> R e. Top )
56 2 55 syl 
 |-  ( ph -> R e. Top )
57 6 7 8 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 } ) ) ) )
58 56 1 57 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 } ) ) ) )
59 eqid 
 |-  ( T ^ko R ) = ( T ^ko R )
60 59 xkotopon 
 |-  ( ( R e. Top /\ T e. Top ) -> ( T ^ko R ) e. ( TopOn ` ( R Cn T ) ) )
61 56 1 60 syl2anc 
 |-  ( ph -> ( T ^ko R ) e. ( TopOn ` ( R Cn T ) ) )
62 47 54 58 61 subbascn 
 |-  ( ph -> ( ( g e. ( S Cn T ) |-> ( g o. F ) ) e. ( ( T ^ko S ) Cn ( T ^ko R ) ) <-> ( ( g e. ( S Cn T ) |-> ( g o. F ) ) : ( S Cn T ) --> ( 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. ( S Cn T ) |-> ( g o. F ) ) " x ) e. ( T ^ko S ) ) ) )
63 5 44 62 mpbir2and 
 |-  ( ph -> ( g e. ( S Cn T ) |-> ( g o. F ) ) e. ( ( T ^ko S ) Cn ( T ^ko R ) ) )