Theorem cncfdmsn

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

	Ref	Expression
Assertion	cncfdmsn	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(x\in \left\{A\right\}⟼B\right):\left\{A\right\}\underset{cn}{⟶}\left\{B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		cnfdmsn	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(x\in \left\{A\right\}⟼B\right)\in \left(𝒫\left\{A\right\}\mathrm{Cn}𝒫\left\{B\right\}\right)$$
2		snssi	$$⊢A\in ℂ\to \left\{A\right\}\subseteq ℂ$$
3		snssi	$$⊢B\in ℂ\to \left\{B\right\}\subseteq ℂ$$
4		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
5		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left\{A\right\}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left\{A\right\}$$
6		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left\{B\right\}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left\{B\right\}$$
7	4 5 6	cncfcn	$$⊢\left(\left\{A\right\}\subseteq ℂ\wedge \left\{B\right\}\subseteq ℂ\right)\to \left\{A\right\}\underset{cn}{⟶}\left\{B\right\}=\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left\{A\right\}\right)\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left\{B\right\}\right)$$
8	2 3 7	syl2an	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left\{A\right\}\underset{cn}{⟶}\left\{B\right\}=\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left\{A\right\}\right)\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left\{B\right\}\right)$$
9	4	cnfldtopon	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$$
10		simpl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A\in ℂ$$
11		restsn2	$$⊢\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\wedge A\in ℂ\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left\{A\right\}=𝒫\left\{A\right\}$$
12	9 10 11	sylancr	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left\{A\right\}=𝒫\left\{A\right\}$$
13		simpr	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to B\in ℂ$$
14		restsn2	$$⊢\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\wedge B\in ℂ\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left\{B\right\}=𝒫\left\{B\right\}$$
15	9 13 14	sylancr	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left\{B\right\}=𝒫\left\{B\right\}$$
16	12 15	oveq12d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left\{A\right\}\right)\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left\{B\right\}\right)=𝒫\left\{A\right\}\mathrm{Cn}𝒫\left\{B\right\}$$
17	8 16	eqtr2d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 𝒫\left\{A\right\}\mathrm{Cn}𝒫\left\{B\right\}=\left\{A\right\}\underset{cn}{⟶}\left\{B\right\}$$
18	1 17	eleqtrd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(x\in \left\{A\right\}⟼B\right):\left\{A\right\}\underset{cn}{⟶}\left\{B\right\}$$