Metamath Proof Explorer


Theorem cnfldhaus

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

Ref Expression
Hypothesis cnfldtopn.1 𝐽 = ( TopOpen ‘ ℂfld )
Assertion cnfldhaus 𝐽 ∈ Haus

Proof

Step Hyp Ref Expression
1 cnfldtopn.1 𝐽 = ( TopOpen ‘ ℂfld )
2 cnxmet ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
3 1 cnfldtopn 𝐽 = ( MetOpen ‘ ( abs ∘ − ) )
4 3 methaus ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) → 𝐽 ∈ Haus )
5 2 4 ax-mp 𝐽 ∈ Haus