Metamath Proof Explorer


Theorem t1top

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

Ref Expression
Assertion t1top ( 𝐽 ∈ Fre → 𝐽 ∈ Top )

Proof

Step Hyp Ref Expression
1 eqid 𝐽 = 𝐽
2 1 ist1 ( 𝐽 ∈ Fre ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 𝐽 { 𝑥 } ∈ ( Clsd ‘ 𝐽 ) ) )
3 2 simplbi ( 𝐽 ∈ Fre → 𝐽 ∈ Top )