Theorem cncfcn1

Description: Relate complex function continuity to topological continuity. (Contributed by Paul Chapman, 28-Nov-2007) (Revised by Mario Carneiro, 7-Sep-2015)

	Ref	Expression
Hypothesis	cncfcn1.1	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
Assertion	cncfcn1	$$⊢ℂ\underset{cn}{⟶}ℂ=J\mathrm{Cn}J$$

Proof

Step	Hyp	Ref	Expression
1		cncfcn1.1	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
2		ssid	$$⊢ℂ\subseteq ℂ$$
3	1	cnfldtopon	$$⊢J\in \mathrm{TopOn}\left(ℂ\right)$$
4	3	toponrestid	$$⊢J=J{\upharpoonright }_{𝑡}ℂ$$
5	1 4 4	cncfcn	$$⊢\left(ℂ\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to ℂ\underset{cn}{⟶}ℂ=J\mathrm{Cn}J$$
6	2 2 5	mp2an	$$⊢ℂ\underset{cn}{⟶}ℂ=J\mathrm{Cn}J$$