Metamath Proof Explorer

Theorem cncfdmsn

Description: A complex function with a singleton domain is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion cncfdmsn ⊢ A ∈ ℂ ∧ B ∈ ℂ → x ∈ A ⟼ B : A ⟶cn B

Proof

Step Hyp Ref Expression
1 cnfdmsn ⊢ A ∈ ℂ ∧ B ∈ ℂ → x ∈ A ⟼ B ∈ 𝒫 A Cn 𝒫 B
2 snssi ⊢ A ∈ ℂ → A ⊆ ℂ
3 snssi ⊢ B ∈ ℂ → B ⊆ ℂ
4 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
5 eqid ⊢ TopOpen ⁡ ℂ fld ↾ 𝑡 A = TopOpen ⁡ ℂ fld ↾ 𝑡 A
6 eqid ⊢ TopOpen ⁡ ℂ fld ↾ 𝑡 B = TopOpen ⁡ ℂ fld ↾ 𝑡 B
7 4 5 6 cncfcn ⊢ A ⊆ ℂ ∧ B ⊆ ℂ → A ⟶cn B = TopOpen ⁡ ℂ fld ↾ 𝑡 A Cn TopOpen ⁡ ℂ fld ↾ 𝑡 B
8 2 3 7 syl2an ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⟶cn B = TopOpen ⁡ ℂ fld ↾ 𝑡 A Cn TopOpen ⁡ ℂ fld ↾ 𝑡 B
9 4 cnfldtopon ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ
10 simpl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ∈ ℂ
11 restsn2 ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ ∧ A ∈ ℂ → TopOpen ⁡ ℂ fld ↾ 𝑡 A = 𝒫 A
12 9 10 11 sylancr ⊢ A ∈ ℂ ∧ B ∈ ℂ → TopOpen ⁡ ℂ fld ↾ 𝑡 A = 𝒫 A
13 simpr ⊢ A ∈ ℂ ∧ B ∈ ℂ → B ∈ ℂ
14 restsn2 ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ ∧ B ∈ ℂ → TopOpen ⁡ ℂ fld ↾ 𝑡 B = 𝒫 B
15 9 13 14 sylancr ⊢ A ∈ ℂ ∧ B ∈ ℂ → TopOpen ⁡ ℂ fld ↾ 𝑡 B = 𝒫 B
16 12 15 oveq12d ⊢ A ∈ ℂ ∧ B ∈ ℂ → TopOpen ⁡ ℂ fld ↾ 𝑡 A Cn TopOpen ⁡ ℂ fld ↾ 𝑡 B = 𝒫 A Cn 𝒫 B
17 8 16 eqtr2d ⊢ A ∈ ℂ ∧ B ∈ ℂ → 𝒫 A Cn 𝒫 B = A ⟶cn B
18 1 17 eleqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ → x ∈ A ⟼ B : A ⟶cn B