Metamath Proof Explorer

Theorem kqhmph

Description: A topological space is T_0 iff it is homeomorphic to its Kolmogorov quotient. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion kqhmph ⊢ J ∈ Kol2 ↔ J ≃ KQ ⁡ J

Proof

Step Hyp Ref Expression
1 t0top ⊢ J ∈ Kol2 → J ∈ Top
2 toptopon2 ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ ⋃ J
3 1 2 sylib ⊢ J ∈ Kol2 → J ∈ TopOn ⁡ ⋃ J
4 eqid ⊢ x ∈ ⋃ J ⟼ y ∈ J | x ∈ y = x ∈ ⋃ J ⟼ y ∈ J | x ∈ y
5 4 t0kq ⊢ J ∈ TopOn ⁡ ⋃ J → J ∈ Kol2 ↔ x ∈ ⋃ J ⟼ y ∈ J | x ∈ y ∈ J Homeo KQ ⁡ J
6 3 5 syl ⊢ J ∈ Kol2 → J ∈ Kol2 ↔ x ∈ ⋃ J ⟼ y ∈ J | x ∈ y ∈ J Homeo KQ ⁡ J
7 6 ibi ⊢ J ∈ Kol2 → x ∈ ⋃ J ⟼ y ∈ J | x ∈ y ∈ J Homeo KQ ⁡ J
8 hmphi ⊢ x ∈ ⋃ J ⟼ y ∈ J | x ∈ y ∈ J Homeo KQ ⁡ J → J ≃ KQ ⁡ J
9 7 8 syl ⊢ J ∈ Kol2 → J ≃ KQ ⁡ J
10 hmphsym ⊢ J ≃ KQ ⁡ J → KQ ⁡ J ≃ J
11 hmphtop1 ⊢ J ≃ KQ ⁡ J → J ∈ Top
12 kqt0 ⊢ J ∈ Top ↔ KQ ⁡ J ∈ Kol2
13 11 12 sylib ⊢ J ≃ KQ ⁡ J → KQ ⁡ J ∈ Kol2
14 t0hmph ⊢ KQ ⁡ J ≃ J → KQ ⁡ J ∈ Kol2 → J ∈ Kol2
15 10 13 14 sylc ⊢ J ≃ KQ ⁡ J → J ∈ Kol2
16 9 15 impbii ⊢ J ∈ Kol2 ↔ J ≃ KQ ⁡ J