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 ⊢ 𝑋 = ∪ 𝑅
Assertion xkopjcn ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐴 ∈ 𝑋 ) → ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝑓 ‘ 𝐴 ) ) ∈ ( ( 𝑆 ↑ko 𝑅 ) Cn 𝑆 ) )

Proof

Step Hyp Ref Expression
1 xkopjcn.1 ⊢ 𝑋 = ∪ 𝑅
2 eqid ⊢ ( 𝑆 ↑ko 𝑅 ) = ( 𝑆 ↑ko 𝑅 )
3 2 xkotopon ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑆 ↑ko 𝑅 ) ∈ ( TopOn ‘ ( 𝑅 Cn 𝑆 ) ) )
4 3 3adant3 ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐴 ∈ 𝑋 ) → ( 𝑆 ↑ko 𝑅 ) ∈ ( TopOn ‘ ( 𝑅 Cn 𝑆 ) ) )
5 1 topopn ⊢ ( 𝑅 ∈ Top → 𝑋 ∈ 𝑅 )
6 5 3ad2ant1 ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐴 ∈ 𝑋 ) → 𝑋 ∈ 𝑅 )
7 fconst6g ⊢ ( 𝑆 ∈ Top → ( 𝑋 × { 𝑆 } ) : 𝑋 ⟶ Top )
8 7 3ad2ant2 ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐴 ∈ 𝑋 ) → ( 𝑋 × { 𝑆 } ) : 𝑋 ⟶ Top )
9 pttop ⊢ ( ( 𝑋 ∈ 𝑅 ∧ ( 𝑋 × { 𝑆 } ) : 𝑋 ⟶ Top ) → ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) ∈ Top )
10 6 8 9 syl2anc ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐴 ∈ 𝑋 ) → ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) ∈ Top )
11 eqid ⊢ ∪ 𝑆 = ∪ 𝑆
12 1 11 cnf ⊢ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) → 𝑓 : 𝑋 ⟶ ∪ 𝑆 )
13 uniexg ⊢ ( 𝑆 ∈ Top → ∪ 𝑆 ∈ V )
14 13 3ad2ant2 ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐴 ∈ 𝑋 ) → ∪ 𝑆 ∈ V )
15 14 6 elmapd ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐴 ∈ 𝑋 ) → ( 𝑓 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↔ 𝑓 : 𝑋 ⟶ ∪ 𝑆 ) )
16 12 15 imbitrrid ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐴 ∈ 𝑋 ) → ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) → 𝑓 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ) )
17 16 ssrdv ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐴 ∈ 𝑋 ) → ( 𝑅 Cn 𝑆 ) ⊆ ( ∪ 𝑆 ↑m 𝑋 ) )
18 simp2 ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐴 ∈ 𝑋 ) → 𝑆 ∈ Top )
19 eqid ⊢ ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) = ( ∏t ‘ ( 𝑋 × { 𝑆 } ) )
20 19 11 ptuniconst ⊢ ( ( 𝑋 ∈ 𝑅 ∧ 𝑆 ∈ Top ) → ( ∪ 𝑆 ↑m 𝑋 ) = ∪ ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) )
21 6 18 20 syl2anc ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐴 ∈ 𝑋 ) → ( ∪ 𝑆 ↑m 𝑋 ) = ∪ ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) )
22 17 21 sseqtrd ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐴 ∈ 𝑋 ) → ( 𝑅 Cn 𝑆 ) ⊆ ∪ ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) )
23 eqid ⊢ ∪ ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) = ∪ ( ∏t ‘ ( 𝑋 × { 𝑆 } ) )
24 23 restuni ⊢ ( ( ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) ∈ Top ∧ ( 𝑅 Cn 𝑆 ) ⊆ ∪ ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) ) → ( 𝑅 Cn 𝑆 ) = ∪ ( ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) ↾t ( 𝑅 Cn 𝑆 ) ) )
25 10 22 24 syl2anc ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐴 ∈ 𝑋 ) → ( 𝑅 Cn 𝑆 ) = ∪ ( ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) ↾t ( 𝑅 Cn 𝑆 ) ) )
26 25 fveq2d ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐴 ∈ 𝑋 ) → ( TopOn ‘ ( 𝑅 Cn 𝑆 ) ) = ( TopOn ‘ ∪ ( ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) ↾t ( 𝑅 Cn 𝑆 ) ) ) )
27 4 26 eleqtrd ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐴 ∈ 𝑋 ) → ( 𝑆 ↑ko 𝑅 ) ∈ ( TopOn ‘ ∪ ( ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) ↾t ( 𝑅 Cn 𝑆 ) ) ) )
28 1 19 xkoptsub ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) ↾t ( 𝑅 Cn 𝑆 ) ) ⊆ ( 𝑆 ↑ko 𝑅 ) )
29 28 3adant3 ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐴 ∈ 𝑋 ) → ( ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) ↾t ( 𝑅 Cn 𝑆 ) ) ⊆ ( 𝑆 ↑ko 𝑅 ) )
30 eqid ⊢ ∪ ( ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) ↾t ( 𝑅 Cn 𝑆 ) ) = ∪ ( ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) ↾t ( 𝑅 Cn 𝑆 ) )
31 30 cnss1 ⊢ ( ( ( 𝑆 ↑ko 𝑅 ) ∈ ( TopOn ‘ ∪ ( ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) ↾t ( 𝑅 Cn 𝑆 ) ) ) ∧ ( ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) ↾t ( 𝑅 Cn 𝑆 ) ) ⊆ ( 𝑆 ↑ko 𝑅 ) ) → ( ( ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) ↾t ( 𝑅 Cn 𝑆 ) ) Cn 𝑆 ) ⊆ ( ( 𝑆 ↑ko 𝑅 ) Cn 𝑆 ) )
32 27 29 31 syl2anc ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐴 ∈ 𝑋 ) → ( ( ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) ↾t ( 𝑅 Cn 𝑆 ) ) Cn 𝑆 ) ⊆ ( ( 𝑆 ↑ko 𝑅 ) Cn 𝑆 ) )
33 22 resmptd ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑓 ∈ ∪ ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) ↦ ( 𝑓 ‘ 𝐴 ) ) ↾ ( 𝑅 Cn 𝑆 ) ) = ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝑓 ‘ 𝐴 ) ) )
34 simp3 ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
35 23 19 ptpjcn ⊢ ( ( 𝑋 ∈ 𝑅 ∧ ( 𝑋 × { 𝑆 } ) : 𝑋 ⟶ Top ∧ 𝐴 ∈ 𝑋 ) → ( 𝑓 ∈ ∪ ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) ↦ ( 𝑓 ‘ 𝐴 ) ) ∈ ( ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) Cn ( ( 𝑋 × { 𝑆 } ) ‘ 𝐴 ) ) )
36 6 8 34 35 syl3anc ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐴 ∈ 𝑋 ) → ( 𝑓 ∈ ∪ ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) ↦ ( 𝑓 ‘ 𝐴 ) ) ∈ ( ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) Cn ( ( 𝑋 × { 𝑆 } ) ‘ 𝐴 ) ) )
37 fvconst2g ⊢ ( ( 𝑆 ∈ Top ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑋 × { 𝑆 } ) ‘ 𝐴 ) = 𝑆 )
38 37 3adant1 ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑋 × { 𝑆 } ) ‘ 𝐴 ) = 𝑆 )
39 38 oveq2d ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐴 ∈ 𝑋 ) → ( ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) Cn ( ( 𝑋 × { 𝑆 } ) ‘ 𝐴 ) ) = ( ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) Cn 𝑆 ) )
40 36 39 eleqtrd ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐴 ∈ 𝑋 ) → ( 𝑓 ∈ ∪ ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) ↦ ( 𝑓 ‘ 𝐴 ) ) ∈ ( ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) Cn 𝑆 ) )
41 23 cnrest ⊢ ( ( ( 𝑓 ∈ ∪ ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) ↦ ( 𝑓 ‘ 𝐴 ) ) ∈ ( ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) Cn 𝑆 ) ∧ ( 𝑅 Cn 𝑆 ) ⊆ ∪ ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) ) → ( ( 𝑓 ∈ ∪ ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) ↦ ( 𝑓 ‘ 𝐴 ) ) ↾ ( 𝑅 Cn 𝑆 ) ) ∈ ( ( ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) ↾t ( 𝑅 Cn 𝑆 ) ) Cn 𝑆 ) )
42 40 22 41 syl2anc ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑓 ∈ ∪ ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) ↦ ( 𝑓 ‘ 𝐴 ) ) ↾ ( 𝑅 Cn 𝑆 ) ) ∈ ( ( ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) ↾t ( 𝑅 Cn 𝑆 ) ) Cn 𝑆 ) )
43 33 42 eqeltrrd ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐴 ∈ 𝑋 ) → ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝑓 ‘ 𝐴 ) ) ∈ ( ( ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) ↾t ( 𝑅 Cn 𝑆 ) ) Cn 𝑆 ) )
44 32 43 sseldd ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐴 ∈ 𝑋 ) → ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝑓 ‘ 𝐴 ) ) ∈ ( ( 𝑆 ↑ko 𝑅 ) Cn 𝑆 ) )