Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cncfmptc Structured version   Visualization version   GIF version

Theorem cncfmptc 22522
 Description: A constant function is a continuous function on ℂ. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 7-Sep-2015.)
Assertion
Ref Expression
cncfmptc ((𝐴𝑇𝑆 ⊆ ℂ ∧ 𝑇 ⊆ ℂ) → (𝑥𝑆𝐴) ∈ (𝑆cn𝑇))
Distinct variable groups:   𝑥,𝐴   𝑥,𝑆   𝑥,𝑇

Proof of Theorem cncfmptc
StepHypRef Expression
1 eqid 2610 . . . . 5 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
21cnfldtopon 22396 . . . 4 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
3 simp2 1055 . . . 4 ((𝐴𝑇𝑆 ⊆ ℂ ∧ 𝑇 ⊆ ℂ) → 𝑆 ⊆ ℂ)
4 resttopon 20775 . . . 4 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆))
52, 3, 4sylancr 694 . . 3 ((𝐴𝑇𝑆 ⊆ ℂ ∧ 𝑇 ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆))
6 simp3 1056 . . . 4 ((𝐴𝑇𝑆 ⊆ ℂ ∧ 𝑇 ⊆ ℂ) → 𝑇 ⊆ ℂ)
7 resttopon 20775 . . . 4 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ 𝑇 ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t 𝑇) ∈ (TopOn‘𝑇))
82, 6, 7sylancr 694 . . 3 ((𝐴𝑇𝑆 ⊆ ℂ ∧ 𝑇 ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t 𝑇) ∈ (TopOn‘𝑇))
9 simp1 1054 . . 3 ((𝐴𝑇𝑆 ⊆ ℂ ∧ 𝑇 ⊆ ℂ) → 𝐴𝑇)
105, 8, 9cnmptc 21275 . 2 ((𝐴𝑇𝑆 ⊆ ℂ ∧ 𝑇 ⊆ ℂ) → (𝑥𝑆𝐴) ∈ (((TopOpen‘ℂfld) ↾t 𝑆) Cn ((TopOpen‘ℂfld) ↾t 𝑇)))
11 eqid 2610 . . . 4 ((TopOpen‘ℂfld) ↾t 𝑆) = ((TopOpen‘ℂfld) ↾t 𝑆)
12 eqid 2610 . . . 4 ((TopOpen‘ℂfld) ↾t 𝑇) = ((TopOpen‘ℂfld) ↾t 𝑇)
131, 11, 12cncfcn 22520 . . 3 ((𝑆 ⊆ ℂ ∧ 𝑇 ⊆ ℂ) → (𝑆cn𝑇) = (((TopOpen‘ℂfld) ↾t 𝑆) Cn ((TopOpen‘ℂfld) ↾t 𝑇)))
14133adant1 1072 . 2 ((𝐴𝑇𝑆 ⊆ ℂ ∧ 𝑇 ⊆ ℂ) → (𝑆cn𝑇) = (((TopOpen‘ℂfld) ↾t 𝑆) Cn ((TopOpen‘ℂfld) ↾t 𝑇)))
1510, 14eleqtrrd 2691 1 ((𝐴𝑇𝑆 ⊆ ℂ ∧ 𝑇 ⊆ ℂ) → (𝑥𝑆𝐴) ∈ (𝑆cn𝑇))