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

Metamath Proof Explorer

Theorem cnfldtop

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 cnfldtop 𝐽 ∈ Top

Proof

Step Hyp Ref Expression
1 cnfldtopn.1 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2 1 cnfldtopon ⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
3 2 topontopi ⊢ 𝐽 ∈ Top