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 ∈ Nrm → J ∈ Haus ↔ J ∈ Fre

Proof

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