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