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