This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ ℂ )