Theorem kqt0

Description: The Kolmogorov quotient is T_0 even if the original topology is not. (Contributed by Mario Carneiro, 25-Aug-2015)

	Ref	Expression
Assertion	kqt0	⊢ ( 𝐽 ∈ Top ↔ ( KQ ‘ 𝐽 ) ∈ Kol2 )

Proof

Step	Hyp	Ref	Expression
1		toptopon2	⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
2		eqid	⊢ ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) = ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
3	2	kqt0lem	⊢ ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) → ( KQ ‘ 𝐽 ) ∈ Kol2 )
4	1 3	sylbi	⊢ ( 𝐽 ∈ Top → ( KQ ‘ 𝐽 ) ∈ Kol2 )
5		t0top	⊢ ( ( KQ ‘ 𝐽 ) ∈ Kol2 → ( KQ ‘ 𝐽 ) ∈ Top )
6		kqtop	⊢ ( 𝐽 ∈ Top ↔ ( KQ ‘ 𝐽 ) ∈ Top )
7	5 6	sylibr	⊢ ( ( KQ ‘ 𝐽 ) ∈ Kol2 → 𝐽 ∈ Top )
8	4 7	impbii	⊢ ( 𝐽 ∈ Top ↔ ( KQ ‘ 𝐽 ) ∈ Kol2 )