Metamath Proof Explorer

Theorem 1stctop

Description: A first-countable topology is a topology. (Contributed by Jeff Hankins, 22-Aug-2009)

Ref Expression
Assertion 1stctop 
|- ( J e. 1stc -> J e. Top )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 1 is1stc 
 |-  ( J e. 1stc <-> ( J e. Top /\ A. x e. U. J E. y e. ~P J ( y ~<_ _om /\ A. z e. J ( x e. z -> x e. U. ( y i^i ~P z ) ) ) ) )
3 2 simplbi 
 |-  ( J e. 1stc -> J e. Top )