Metamath Proof Explorer

Theorem ist1-5

Description: A topological space is T_1 iff it is both T_0 and R_0. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion ist1-5 ⊢ J ∈ Fre ↔ J ∈ Kol2 ∧ KQ ⁡ J ∈ Fre

Proof

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