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∈JHomeoKQ⁡J
6 3 5 syl ⊢J∈Kol2→J∈Kol2↔x∈⋃J⟼y∈J|x∈y∈JHomeoKQ⁡J
7 6 ibi ⊢J∈Kol2→x∈⋃J⟼y∈J|x∈y∈JHomeoKQ⁡J
8 hmphi ⊢x∈⋃J⟼y∈J|x∈y∈JHomeoKQ⁡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