Metamath Proof Explorer


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 )