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

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 1 ist0 
 |-  ( J e. Kol2 <-> ( J e. Top /\ A. x e. U. J A. y e. U. J ( A. o e. J ( x e. o <-> y e. o ) -> x = y ) ) )
3 2 simplbi 
 |-  ( J e. Kol2 -> J e. Top )