Metamath Proof Explorer

Theorem ishaus3

Description: A topological space is Hausdorff iff it is both T_0 and R_1 (where R_1 means that any two topologically distinct points are separated by neighborhoods). (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion ishaus3 ⊢ J ∈ Haus ↔ J ∈ Kol2 ∧ KQ ⁡ J ∈ Haus

Proof

Step Hyp Ref Expression
1 haust1 ⊢ J ∈ Haus → J ∈ Fre
2 t1t0 ⊢ J ∈ Fre → J ∈ Kol2
3 1 2 syl ⊢ J ∈ Haus → J ∈ Kol2
4 haushmph ⊢ J ≃ KQ ⁡ J → J ∈ Haus → KQ ⁡ J ∈ Haus
5 haushmph ⊢ KQ ⁡ J ≃ J → KQ ⁡ J ∈ Haus → J ∈ Haus
6 3 4 5 ist1-5lem ⊢ J ∈ Haus ↔ J ∈ Kol2 ∧ KQ ⁡ J ∈ Haus