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 
|- ( J e. Fre -> J e. Top )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 1 ist1 
 |-  ( J e. Fre <-> ( J e. Top /\ A. x e. U. J { x } e. ( Clsd ` J ) ) )
3 2 simplbi 
 |-  ( J e. Fre -> J e. Top )