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 ‘ 𝐽 ) ) ) )