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 ⊢ A ∈ T ∧ S ⊆ ℂ ∧ T ⊆ ℂ → x ∈ S ⟼ A : S ⟶cn T

Proof

Step Hyp Ref Expression
1 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
2 1 cnfldtopon ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ
3 simp2 ⊢ A ∈ T ∧ S ⊆ ℂ ∧ T ⊆ ℂ → S ⊆ ℂ
4 resttopon ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ ∧ S ⊆ ℂ → TopOpen ⁡ ℂ fld ↾ 𝑡 S ∈ TopOn ⁡ S
5 2 3 4 sylancr ⊢ A ∈ T ∧ S ⊆ ℂ ∧ T ⊆ ℂ → TopOpen ⁡ ℂ fld ↾ 𝑡 S ∈ TopOn ⁡ S
6 simp3 ⊢ A ∈ T ∧ S ⊆ ℂ ∧ T ⊆ ℂ → T ⊆ ℂ
7 resttopon ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ ∧ T ⊆ ℂ → TopOpen ⁡ ℂ fld ↾ 𝑡 T ∈ TopOn ⁡ T
8 2 6 7 sylancr ⊢ A ∈ T ∧ S ⊆ ℂ ∧ T ⊆ ℂ → TopOpen ⁡ ℂ fld ↾ 𝑡 T ∈ TopOn ⁡ T
9 simp1 ⊢ A ∈ T ∧ S ⊆ ℂ ∧ T ⊆ ℂ → A ∈ T
10 5 8 9 cnmptc ⊢ A ∈ T ∧ S ⊆ ℂ ∧ T ⊆ ℂ → x ∈ S ⟼ A ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 S Cn TopOpen ⁡ ℂ fld ↾ 𝑡 T
11 eqid ⊢ TopOpen ⁡ ℂ fld ↾ 𝑡 S = TopOpen ⁡ ℂ fld ↾ 𝑡 S
12 eqid ⊢ TopOpen ⁡ ℂ fld ↾ 𝑡 T = TopOpen ⁡ ℂ fld ↾ 𝑡 T
13 1 11 12 cncfcn ⊢ S ⊆ ℂ ∧ T ⊆ ℂ → S ⟶cn T = TopOpen ⁡ ℂ fld ↾ 𝑡 S Cn TopOpen ⁡ ℂ fld ↾ 𝑡 T
14 13 3adant1 ⊢ A ∈ T ∧ S ⊆ ℂ ∧ T ⊆ ℂ → S ⟶cn T = TopOpen ⁡ ℂ fld ↾ 𝑡 S Cn TopOpen ⁡ ℂ fld ↾ 𝑡 T
15 10 14 eleqtrrd ⊢ A ∈ T ∧ S ⊆ ℂ ∧ T ⊆ ℂ → x ∈ S ⟼ A : S ⟶cn T