Metamath Proof Explorer

Theorem xkopjcn

Description: Continuity of a projection map from the space of continuous functions. (This theorem can be strengthened, to joint continuity in both f and A as a function on ( S ^ko R ) tX R , but not without stronger assumptions on R ; see xkofvcn .) (Contributed by Mario Carneiro, 3-Feb-2015) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypothesis xkopjcn.1 
|- X = U. R
Assertion xkopjcn 
|- ( ( R e. Top /\ S e. Top /\ A e. X ) -> ( f e. ( R Cn S ) |-> ( f ` A ) ) e. ( ( S ^ko R ) Cn S ) )

Proof

Step Hyp Ref Expression
1 xkopjcn.1 
 |-  X = U. R
2 eqid 
 |-  ( S ^ko R ) = ( S ^ko R )
3 2 xkotopon 
 |-  ( ( R e. Top /\ S e. Top ) -> ( S ^ko R ) e. ( TopOn ` ( R Cn S ) ) )
4 3 3adant3 
 |-  ( ( R e. Top /\ S e. Top /\ A e. X ) -> ( S ^ko R ) e. ( TopOn ` ( R Cn S ) ) )
5 1 topopn 
 |-  ( R e. Top -> X e. R )
6 5 3ad2ant1 
 |-  ( ( R e. Top /\ S e. Top /\ A e. X ) -> X e. R )
7 fconst6g 
 |-  ( S e. Top -> ( X X. { S } ) : X --> Top )
8 7 3ad2ant2 
 |-  ( ( R e. Top /\ S e. Top /\ A e. X ) -> ( X X. { S } ) : X --> Top )
9 pttop 
 |-  ( ( X e. R /\ ( X X. { S } ) : X --> Top ) -> ( Xt_ ` ( X X. { S } ) ) e. Top )
10 6 8 9 syl2anc 
 |-  ( ( R e. Top /\ S e. Top /\ A e. X ) -> ( Xt_ ` ( X X. { S } ) ) e. Top )
11 eqid 
 |-  U. S = U. S
12 1 11 cnf 
 |-  ( f e. ( R Cn S ) -> f : X --> U. S )
13 uniexg 
 |-  ( S e. Top -> U. S e. _V )
14 13 3ad2ant2 
 |-  ( ( R e. Top /\ S e. Top /\ A e. X ) -> U. S e. _V )
15 14 6 elmapd 
 |-  ( ( R e. Top /\ S e. Top /\ A e. X ) -> ( f e. ( U. S ^m X ) <-> f : X --> U. S ) )
16 12 15 syl5ibr 
 |-  ( ( R e. Top /\ S e. Top /\ A e. X ) -> ( f e. ( R Cn S ) -> f e. ( U. S ^m X ) ) )
17 16 ssrdv 
 |-  ( ( R e. Top /\ S e. Top /\ A e. X ) -> ( R Cn S ) C_ ( U. S ^m X ) )
18 simp2 
 |-  ( ( R e. Top /\ S e. Top /\ A e. X ) -> S e. Top )
19 eqid 
 |-  ( Xt_ ` ( X X. { S } ) ) = ( Xt_ ` ( X X. { S } ) )
20 19 11 ptuniconst 
 |-  ( ( X e. R /\ S e. Top ) -> ( U. S ^m X ) = U. ( Xt_ ` ( X X. { S } ) ) )
21 6 18 20 syl2anc 
 |-  ( ( R e. Top /\ S e. Top /\ A e. X ) -> ( U. S ^m X ) = U. ( Xt_ ` ( X X. { S } ) ) )
22 17 21 sseqtrd 
 |-  ( ( R e. Top /\ S e. Top /\ A e. X ) -> ( R Cn S ) C_ U. ( Xt_ ` ( X X. { S } ) ) )
23 eqid 
 |-  U. ( Xt_ ` ( X X. { S } ) ) = U. ( Xt_ ` ( X X. { S } ) )
24 23 restuni 
 |-  ( ( ( Xt_ ` ( X X. { S } ) ) e. Top /\ ( R Cn S ) C_ U. ( Xt_ ` ( X X. { S } ) ) ) -> ( R Cn S ) = U. ( ( Xt_ ` ( X X. { S } ) ) |`t ( R Cn S ) ) )
25 10 22 24 syl2anc 
 |-  ( ( R e. Top /\ S e. Top /\ A e. X ) -> ( R Cn S ) = U. ( ( Xt_ ` ( X X. { S } ) ) |`t ( R Cn S ) ) )
26 25 fveq2d 
 |-  ( ( R e. Top /\ S e. Top /\ A e. X ) -> ( TopOn ` ( R Cn S ) ) = ( TopOn ` U. ( ( Xt_ ` ( X X. { S } ) ) |`t ( R Cn S ) ) ) )
27 4 26 eleqtrd 
 |-  ( ( R e. Top /\ S e. Top /\ A e. X ) -> ( S ^ko R ) e. ( TopOn ` U. ( ( Xt_ ` ( X X. { S } ) ) |`t ( R Cn S ) ) ) )
28 1 19 xkoptsub 
 |-  ( ( R e. Top /\ S e. Top ) -> ( ( Xt_ ` ( X X. { S } ) ) |`t ( R Cn S ) ) C_ ( S ^ko R ) )
29 28 3adant3 
 |-  ( ( R e. Top /\ S e. Top /\ A e. X ) -> ( ( Xt_ ` ( X X. { S } ) ) |`t ( R Cn S ) ) C_ ( S ^ko R ) )
30 eqid 
 |-  U. ( ( Xt_ ` ( X X. { S } ) ) |`t ( R Cn S ) ) = U. ( ( Xt_ ` ( X X. { S } ) ) |`t ( R Cn S ) )
31 30 cnss1 
 |-  ( ( ( S ^ko R ) e. ( TopOn ` U. ( ( Xt_ ` ( X X. { S } ) ) |`t ( R Cn S ) ) ) /\ ( ( Xt_ ` ( X X. { S } ) ) |`t ( R Cn S ) ) C_ ( S ^ko R ) ) -> ( ( ( Xt_ ` ( X X. { S } ) ) |`t ( R Cn S ) ) Cn S ) C_ ( ( S ^ko R ) Cn S ) )
32 27 29 31 syl2anc 
 |-  ( ( R e. Top /\ S e. Top /\ A e. X ) -> ( ( ( Xt_ ` ( X X. { S } ) ) |`t ( R Cn S ) ) Cn S ) C_ ( ( S ^ko R ) Cn S ) )
33 22 resmptd 
 |-  ( ( R e. Top /\ S e. Top /\ A e. X ) -> ( ( f e. U. ( Xt_ ` ( X X. { S } ) ) |-> ( f ` A ) ) |` ( R Cn S ) ) = ( f e. ( R Cn S ) |-> ( f ` A ) ) )
34 simp3 
 |-  ( ( R e. Top /\ S e. Top /\ A e. X ) -> A e. X )
35 23 19 ptpjcn 
 |-  ( ( X e. R /\ ( X X. { S } ) : X --> Top /\ A e. X ) -> ( f e. U. ( Xt_ ` ( X X. { S } ) ) |-> ( f ` A ) ) e. ( ( Xt_ ` ( X X. { S } ) ) Cn ( ( X X. { S } ) ` A ) ) )
36 6 8 34 35 syl3anc 
 |-  ( ( R e. Top /\ S e. Top /\ A e. X ) -> ( f e. U. ( Xt_ ` ( X X. { S } ) ) |-> ( f ` A ) ) e. ( ( Xt_ ` ( X X. { S } ) ) Cn ( ( X X. { S } ) ` A ) ) )
37 fvconst2g 
 |-  ( ( S e. Top /\ A e. X ) -> ( ( X X. { S } ) ` A ) = S )
38 37 3adant1 
 |-  ( ( R e. Top /\ S e. Top /\ A e. X ) -> ( ( X X. { S } ) ` A ) = S )
39 38 oveq2d 
 |-  ( ( R e. Top /\ S e. Top /\ A e. X ) -> ( ( Xt_ ` ( X X. { S } ) ) Cn ( ( X X. { S } ) ` A ) ) = ( ( Xt_ ` ( X X. { S } ) ) Cn S ) )
40 36 39 eleqtrd 
 |-  ( ( R e. Top /\ S e. Top /\ A e. X ) -> ( f e. U. ( Xt_ ` ( X X. { S } ) ) |-> ( f ` A ) ) e. ( ( Xt_ ` ( X X. { S } ) ) Cn S ) )
41 23 cnrest 
 |-  ( ( ( f e. U. ( Xt_ ` ( X X. { S } ) ) |-> ( f ` A ) ) e. ( ( Xt_ ` ( X X. { S } ) ) Cn S ) /\ ( R Cn S ) C_ U. ( Xt_ ` ( X X. { S } ) ) ) -> ( ( f e. U. ( Xt_ ` ( X X. { S } ) ) |-> ( f ` A ) ) |` ( R Cn S ) ) e. ( ( ( Xt_ ` ( X X. { S } ) ) |`t ( R Cn S ) ) Cn S ) )
42 40 22 41 syl2anc 
 |-  ( ( R e. Top /\ S e. Top /\ A e. X ) -> ( ( f e. U. ( Xt_ ` ( X X. { S } ) ) |-> ( f ` A ) ) |` ( R Cn S ) ) e. ( ( ( Xt_ ` ( X X. { S } ) ) |`t ( R Cn S ) ) Cn S ) )
43 33 42 eqeltrrd 
 |-  ( ( R e. Top /\ S e. Top /\ A e. X ) -> ( f e. ( R Cn S ) |-> ( f ` A ) ) e. ( ( ( Xt_ ` ( X X. { S } ) ) |`t ( R Cn S ) ) Cn S ) )
44 32 43 sseldd 
 |-  ( ( R e. Top /\ S e. Top /\ A e. X ) -> ( f e. ( R Cn S ) |-> ( f ` A ) ) e. ( ( S ^ko R ) Cn S ) )