This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sst0

Description: A topology finer than a T_0 topology is T_0. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypothesis t1sep.1 ⊢ 𝑋 = ∪ 𝐽
Assertion sst0 ( ( 𝐽 ∈ Kol2 ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → 𝐾 ∈ Kol2 )

Proof

Step Hyp Ref Expression
1 t1sep.1 ⊢ 𝑋 = ∪ 𝐽
2 t0top ⊢ ( 𝐽 ∈ Kol2 → 𝐽 ∈ Top )
3 cnt0 ⊢ ( ( 𝐽 ∈ Kol2 ∧ ( I ↾ 𝑋 ) : 𝑋 –1-1→ 𝑋 ∧ ( I ↾ 𝑋 ) ∈ ( 𝐾 Cn 𝐽 ) ) → 𝐾 ∈ Kol2 )
4 1 2 3 sshauslem ⊢ ( ( 𝐽 ∈ Kol2 ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → 𝐾 ∈ Kol2 )