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

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 ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
Assertion t0kq ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Kol2 ↔ 𝐹 ∈ ( 𝐽 Homeo ( KQ ‘ 𝐽 ) ) ) )

Proof

Step Hyp Ref Expression
1 t0kq.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
2 simpl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Kol2 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3 1 ist0-4 ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Kol2 ↔ 𝐹 : 𝑋 –1-1→ V ) )
4 3 biimpa ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Kol2 ) → 𝐹 : 𝑋 –1-1→ V )
5 2 4 qtopf1 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Kol2 ) → 𝐹 ∈ ( 𝐽 Homeo ( 𝐽 qTop 𝐹 ) ) )
6 1 kqval ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( KQ ‘ 𝐽 ) = ( 𝐽 qTop 𝐹 ) )
7 6 adantr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Kol2 ) → ( KQ ‘ 𝐽 ) = ( 𝐽 qTop 𝐹 ) )
8 7 oveq2d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Kol2 ) → ( 𝐽 Homeo ( KQ ‘ 𝐽 ) ) = ( 𝐽 Homeo ( 𝐽 qTop 𝐹 ) ) )
9 5 8 eleqtrrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Kol2 ) → 𝐹 ∈ ( 𝐽 Homeo ( KQ ‘ 𝐽 ) ) )
10 hmphi ⊢ ( 𝐹 ∈ ( 𝐽 Homeo ( KQ ‘ 𝐽 ) ) → 𝐽 ≃ ( KQ ‘ 𝐽 ) )
11 hmphsym ⊢ ( 𝐽 ≃ ( KQ ‘ 𝐽 ) → ( KQ ‘ 𝐽 ) ≃ 𝐽 )
12 10 11 syl ⊢ ( 𝐹 ∈ ( 𝐽 Homeo ( KQ ‘ 𝐽 ) ) → ( KQ ‘ 𝐽 ) ≃ 𝐽 )
13 1 kqt0lem ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( KQ ‘ 𝐽 ) ∈ Kol2 )
14 t0hmph ⊢ ( ( KQ ‘ 𝐽 ) ≃ 𝐽 → ( ( KQ ‘ 𝐽 ) ∈ Kol2 → 𝐽 ∈ Kol2 ) )
15 12 13 14 syl2im ⊢ ( 𝐹 ∈ ( 𝐽 Homeo ( KQ ‘ 𝐽 ) ) → ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Kol2 ) )
16 15 impcom ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( 𝐽 Homeo ( KQ ‘ 𝐽 ) ) ) → 𝐽 ∈ Kol2 )
17 9 16 impbida ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Kol2 ↔ 𝐹 ∈ ( 𝐽 Homeo ( KQ ‘ 𝐽 ) ) ) )