This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐽 ∈ Kol2 ↔ 𝐽 ≃ ( KQ ‘ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 t0top ⊢ ( 𝐽 ∈ Kol2 → 𝐽 ∈ Top )
2 toptopon2 ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
3 1 2 sylib ⊢ ( 𝐽 ∈ Kol2 → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
4 eqid ⊢ ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) = ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
5 4 t0kq ⊢ ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) → ( 𝐽 ∈ Kol2 ↔ ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) ∈ ( 𝐽 Homeo ( KQ ‘ 𝐽 ) ) ) )
6 3 5 syl ⊢ ( 𝐽 ∈ Kol2 → ( 𝐽 ∈ Kol2 ↔ ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) ∈ ( 𝐽 Homeo ( KQ ‘ 𝐽 ) ) ) )
7 6 ibi ⊢ ( 𝐽 ∈ Kol2 → ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) ∈ ( 𝐽 Homeo ( KQ ‘ 𝐽 ) ) )
8 hmphi ⊢ ( ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) ∈ ( 𝐽 Homeo ( KQ ‘ 𝐽 ) ) → 𝐽 ≃ ( KQ ‘ 𝐽 ) )
9 7 8 syl ⊢ ( 𝐽 ∈ Kol2 → 𝐽 ≃ ( KQ ‘ 𝐽 ) )
10 hmphsym ⊢ ( 𝐽 ≃ ( KQ ‘ 𝐽 ) → ( KQ ‘ 𝐽 ) ≃ 𝐽 )
11 hmphtop1 ⊢ ( 𝐽 ≃ ( KQ ‘ 𝐽 ) → 𝐽 ∈ Top )
12 kqt0 ⊢ ( 𝐽 ∈ Top ↔ ( KQ ‘ 𝐽 ) ∈ Kol2 )
13 11 12 sylib ⊢ ( 𝐽 ≃ ( KQ ‘ 𝐽 ) → ( KQ ‘ 𝐽 ) ∈ Kol2 )
14 t0hmph ⊢ ( ( KQ ‘ 𝐽 ) ≃ 𝐽 → ( ( KQ ‘ 𝐽 ) ∈ Kol2 → 𝐽 ∈ Kol2 ) )
15 10 13 14 sylc ⊢ ( 𝐽 ≃ ( KQ ‘ 𝐽 ) → 𝐽 ∈ Kol2 )
16 9 15 impbii ⊢ ( 𝐽 ∈ Kol2 ↔ 𝐽 ≃ ( KQ ‘ 𝐽 ) )