Metamath Proof Explorer

Theorem 2ndctop

Description: A second-countable topology is a topology. (Contributed by Jeff Hankins, 17-Jan-2010) (Revised by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion 2ndctop 
|- ( J e. 2ndc -> J e. Top )

Proof

Step Hyp Ref Expression
1 is2ndc 
 |-  ( J e. 2ndc <-> E. x e. TopBases ( x ~<_ _om /\ ( topGen ` x ) = J ) )
2 simprr 
 |-  ( ( x e. TopBases /\ ( x ~<_ _om /\ ( topGen ` x ) = J ) ) -> ( topGen ` x ) = J )
3 tgcl 
 |-  ( x e. TopBases -> ( topGen ` x ) e. Top )
4 3 adantr 
 |-  ( ( x e. TopBases /\ ( x ~<_ _om /\ ( topGen ` x ) = J ) ) -> ( topGen ` x ) e. Top )
5 2 4 eqeltrrd 
 |-  ( ( x e. TopBases /\ ( x ~<_ _om /\ ( topGen ` x ) = J ) ) -> J e. Top )
6 5 rexlimiva 
 |-  ( E. x e. TopBases ( x ~<_ _om /\ ( topGen ` x ) = J ) -> J e. Top )
7 1 6 sylbi 
 |-  ( J e. 2ndc -> J e. Top )