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