Metamath Proof Explorer

Theorem t0kq

Description: A topological space is T_0 iff the quotient map is a homeomorphism onto the space's Kolmogorov quotient. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypothesis t0kq.1 ⊢ F = x ∈ X ⟼ y ∈ J | x ∈ y
Assertion t0kq ⊢ J ∈ TopOn ⁡ X → J ∈ Kol2 ↔ F ∈ J Homeo KQ ⁡ J

Proof

Step Hyp Ref Expression
1 t0kq.1 ⊢ F = x ∈ X ⟼ y ∈ J | x ∈ y
2 simpl ⊢ J ∈ TopOn ⁡ X ∧ J ∈ Kol2 → J ∈ TopOn ⁡ X
3 1 ist0-4 ⊢ J ∈ TopOn ⁡ X → J ∈ Kol2 ↔ F : X ⟶ 1-1 V
4 3 biimpa ⊢ J ∈ TopOn ⁡ X ∧ J ∈ Kol2 → F : X ⟶ 1-1 V
5 2 4 qtopf1 ⊢ J ∈ TopOn ⁡ X ∧ J ∈ Kol2 → F ∈ J Homeo J qTop F
6 1 kqval ⊢ J ∈ TopOn ⁡ X → KQ ⁡ J = J qTop F
7 6 adantr ⊢ J ∈ TopOn ⁡ X ∧ J ∈ Kol2 → KQ ⁡ J = J qTop F
8 7 oveq2d ⊢ J ∈ TopOn ⁡ X ∧ J ∈ Kol2 → J Homeo KQ ⁡ J = J Homeo J qTop F
9 5 8 eleqtrrd ⊢ J ∈ TopOn ⁡ X ∧ J ∈ Kol2 → F ∈ J Homeo KQ ⁡ J
10 hmphi ⊢ F ∈ J Homeo KQ ⁡ J → J ≃ KQ ⁡ J
11 hmphsym ⊢ J ≃ KQ ⁡ J → KQ ⁡ J ≃ J
12 10 11 syl ⊢ F ∈ J Homeo KQ ⁡ J → KQ ⁡ J ≃ J
13 1 kqt0lem ⊢ J ∈ TopOn ⁡ X → KQ ⁡ J ∈ Kol2
14 t0hmph ⊢ KQ ⁡ J ≃ J → KQ ⁡ J ∈ Kol2 → J ∈ Kol2
15 12 13 14 syl2im ⊢ F ∈ J Homeo KQ ⁡ J → J ∈ TopOn ⁡ X → J ∈ Kol2
16 15 impcom ⊢ J ∈ TopOn ⁡ X ∧ F ∈ J Homeo KQ ⁡ J → J ∈ Kol2
17 9 16 impbida ⊢ J ∈ TopOn ⁡ X → J ∈ Kol2 ↔ F ∈ J Homeo KQ ⁡ J