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