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

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	$⊢ J = TopOpen (ℂ_{fld})$
	Assertion	cnfldhaus	$⊢ J \in Haus$

Step	Hyp	Ref	Expression
1		cnfldtopn.1	$⊢ J = TopOpen (ℂ_{fld})$
2		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
3	1	cnfldtopn	$⊢ J = MetOpen (abs \circ -)$
4	3	methaus	$⊢ abs \circ - \in ∞Met (ℂ) \to J \in Haus$
5	2 4	ax-mp	$⊢ J \in Haus$