Metamath Proof Explorer


Theorem t0top

Description: A T_0 space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010)

Ref Expression
Assertion t0top ( 𝐽 ∈ Kol2 → 𝐽 ∈ Top )

Proof

Step Hyp Ref Expression
1 eqid 𝐽 = 𝐽
2 1 ist0 ( 𝐽 ∈ Kol2 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 𝐽𝑦 𝐽 ( ∀ 𝑜𝐽 ( 𝑥𝑜𝑦𝑜 ) → 𝑥 = 𝑦 ) ) )
3 2 simplbi ( 𝐽 ∈ Kol2 → 𝐽 ∈ Top )