This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cncfmptc

Description: A constant function is a continuous function on CC . (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 7-Sep-2015)

Ref Expression
Assertion cncfmptc ( ( 𝐴 ∈ 𝑇 ∧ 𝑆 ⊆ ℂ ∧ 𝑇 ⊆ ℂ ) → ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ∈ ( 𝑆 –cn→ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
2 1 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
3 simp2 ⊢ ( ( 𝐴 ∈ 𝑇 ∧ 𝑆 ⊆ ℂ ∧ 𝑇 ⊆ ℂ ) → 𝑆 ⊆ ℂ )
4 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ 𝑆 ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
5 2 3 4 sylancr ⊢ ( ( 𝐴 ∈ 𝑇 ∧ 𝑆 ⊆ ℂ ∧ 𝑇 ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
6 simp3 ⊢ ( ( 𝐴 ∈ 𝑇 ∧ 𝑆 ⊆ ℂ ∧ 𝑇 ⊆ ℂ ) → 𝑇 ⊆ ℂ )
7 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ 𝑇 ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝑇 ) ∈ ( TopOn ‘ 𝑇 ) )
8 2 6 7 sylancr ⊢ ( ( 𝐴 ∈ 𝑇 ∧ 𝑆 ⊆ ℂ ∧ 𝑇 ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝑇 ) ∈ ( TopOn ‘ 𝑇 ) )
9 simp1 ⊢ ( ( 𝐴 ∈ 𝑇 ∧ 𝑆 ⊆ ℂ ∧ 𝑇 ⊆ ℂ ) → 𝐴 ∈ 𝑇 )
10 5 8 9 cnmptc ⊢ ( ( 𝐴 ∈ 𝑇 ∧ 𝑆 ⊆ ℂ ∧ 𝑇 ⊆ ℂ ) → ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) Cn ( ( TopOpen ‘ ℂfld ) ↾t 𝑇 ) ) )
11 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 )
12 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝑇 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝑇 )
13 1 11 12 cncfcn ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝑇 ⊆ ℂ ) → ( 𝑆 –cn→ 𝑇 ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) Cn ( ( TopOpen ‘ ℂfld ) ↾t 𝑇 ) ) )
14 13 3adant1 ⊢ ( ( 𝐴 ∈ 𝑇 ∧ 𝑆 ⊆ ℂ ∧ 𝑇 ⊆ ℂ ) → ( 𝑆 –cn→ 𝑇 ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) Cn ( ( TopOpen ‘ ℂfld ) ↾t 𝑇 ) ) )
15 10 14 eleqtrrd ⊢ ( ( 𝐴 ∈ 𝑇 ∧ 𝑆 ⊆ ℂ ∧ 𝑇 ⊆ ℂ ) → ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ∈ ( 𝑆 –cn→ 𝑇 ) )