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 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
Assertion cnfldtopn 𝐽 = ( MetOpen ‘ ( abs ∘ − ) )

Proof

Step Hyp Ref Expression
1 cnfldtopn.1 ⊢ 𝐽 = ( 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 ⊢ 𝐽 = ( MetOpen ‘ ( abs ∘ − ) )