Metamath Proof Explorer

Theorem nrmhaus

Description: A T_1 normal space is Hausdorff. A Hausdorff or T_1 normal space is also known as a T_4 space. (Contributed by Mario Carneiro, 24-Aug-2015)

		Ref	Expression
	Assertion	nrmhaus	$⊢ J \in Nrm \to (J \in Haus \leftrightarrow J \in Fre)$

Proof

Step	Hyp	Ref	Expression
1		haust1	$⊢ J \in Haus \to J \in Fre$
2		nrmreg	$⊢ (J \in Nrm \land J \in Fre) \to J \in Reg$
3	2	ex	$⊢ J \in Nrm \to (J \in Fre \to J \in Reg)$
4		t1t0	$⊢ J \in Fre \to J \in Kol2$
5		reghaus	$⊢ J \in Reg \to (J \in Haus \leftrightarrow J \in Kol2)$
6	4 5	syl5ibrcom	$⊢ J \in Fre \to (J \in Reg \to J \in Haus)$
7	3 6	sylcom	$⊢ J \in Nrm \to (J \in Fre \to J \in Haus)$
8	1 7	impbid2	$⊢ J \in Nrm \to (J \in Haus \leftrightarrow J \in Fre)$