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