Metamath Proof Explorer

Theorem kqt0

Description: The Kolmogorov quotient is T_0 even if the original topology is not. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion kqt0 ⊢ J ∈ Top ↔ KQ ⁡ J ∈ Kol2

Proof

Step Hyp Ref Expression
1 toptopon2 ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ ⋃ J
2 eqid ⊢ x ∈ ⋃ J ⟼ y ∈ J | x ∈ y = x ∈ ⋃ J ⟼ y ∈ J | x ∈ y
3 2 kqt0lem ⊢ J ∈ TopOn ⁡ ⋃ J → KQ ⁡ J ∈ Kol2
4 1 3 sylbi ⊢ J ∈ Top → KQ ⁡ J ∈ Kol2
5 t0top ⊢ KQ ⁡ J ∈ Kol2 → KQ ⁡ J ∈ Top
6 kqtop ⊢ J ∈ Top ↔ KQ ⁡ J ∈ Top
7 5 6 sylibr ⊢ KQ ⁡ J ∈ Kol2 → J ∈ Top
8 4 7 impbii ⊢ J ∈ Top ↔ KQ ⁡ J ∈ Kol2