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	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
Assertion	cncfcn1	⊢ ( ℂ –cn→ ℂ ) = ( 𝐽 Cn 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		cncfcn1.1	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2		ssid	⊢ ℂ ⊆ ℂ
3	1	cnfldtopon	⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
4	3	toponrestid	⊢ 𝐽 = ( 𝐽 ↾t ℂ )
5	1 4 4	cncfcn	⊢ ( ( ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ℂ –cn→ ℂ ) = ( 𝐽 Cn 𝐽 ) )
6	2 2 5	mp2an	⊢ ( ℂ –cn→ ℂ ) = ( 𝐽 Cn 𝐽 )