Theorem cnfldtopon

Description: The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015)

	Ref	Expression
Hypothesis	cnfldtopn.1	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
Assertion	cnfldtopon	⊢ 𝐽 ∈ ( TopOn ‘ ℂ )

Proof

Step	Hyp	Ref	Expression
1		cnfldtopn.1	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2		cnfldtps	⊢ ℂfld ∈ TopSp
3		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
4	3 1	istps	⊢ ( ℂfld ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ ℂ ) )
5	2 4	mpbi	⊢ 𝐽 ∈ ( TopOn ‘ ℂ )