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	⊢ ( 𝐽 ∈ Nrm → ( 𝐽 ∈ Haus ↔ 𝐽 ∈ Fre ) )

Proof

Step	Hyp	Ref	Expression
1		haust1	⊢ ( 𝐽 ∈ Haus → 𝐽 ∈ Fre )
2		nrmreg	⊢ ( ( 𝐽 ∈ Nrm ∧ 𝐽 ∈ Fre ) → 𝐽 ∈ Reg )
3	2	ex	⊢ ( 𝐽 ∈ Nrm → ( 𝐽 ∈ Fre → 𝐽 ∈ Reg ) )
4		t1t0	⊢ ( 𝐽 ∈ Fre → 𝐽 ∈ Kol2 )
5		reghaus	⊢ ( 𝐽 ∈ Reg → ( 𝐽 ∈ Haus ↔ 𝐽 ∈ Kol2 ) )
6	4 5	syl5ibrcom	⊢ ( 𝐽 ∈ Fre → ( 𝐽 ∈ Reg → 𝐽 ∈ Haus ) )
7	3 6	sylcom	⊢ ( 𝐽 ∈ Nrm → ( 𝐽 ∈ Fre → 𝐽 ∈ Haus ) )
8	1 7	impbid2	⊢ ( 𝐽 ∈ Nrm → ( 𝐽 ∈ Haus ↔ 𝐽 ∈ Fre ) )