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

Metamath Proof Explorer

Theorem cnfldtopn

Description: The topology of the complex numbers. (Contributed by Mario Carneiro, 28-Aug-2015)

Ref Expression
Hypothesis cnfldtopn.1 ⊢ J = TopOpen ⁡ ℂ fld
Assertion cnfldtopn ⊢ J = MetOpen ⁡ abs ∘ −

Proof

Step Hyp Ref Expression
1 cnfldtopn.1 ⊢ J = TopOpen ⁡ ℂ fld
2 cnxmet ⊢ abs ∘ − ∈ ∞Met ⁡ ℂ
3 eqid ⊢ MetOpen ⁡ abs ∘ − = MetOpen ⁡ abs ∘ −
4 3 mopntopon ⊢ abs ∘ − ∈ ∞Met ⁡ ℂ → MetOpen ⁡ abs ∘ − ∈ TopOn ⁡ ℂ
5 cnfldbas ⊢ ℂ = Base ℂ fld
6 cnfldtset ⊢ MetOpen ⁡ abs ∘ − = TopSet ⁡ ℂ fld
7 5 6 topontopn ⊢ MetOpen ⁡ abs ∘ − ∈ TopOn ⁡ ℂ → MetOpen ⁡ abs ∘ − = TopOpen ⁡ ℂ fld
8 2 4 7 mp2b ⊢ MetOpen ⁡ abs ∘ − = TopOpen ⁡ ℂ fld
9 1 8 eqtr4i ⊢ J = MetOpen ⁡ abs ∘ −