Metamath Proof Explorer

Theorem is2ndc

Description: The property of being second-countable. (Contributed by Jeff Hankins, 17-Jan-2010) (Revised by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion is2ndc 
|- ( J e. 2ndc <-> E. x e. TopBases ( x ~<_ _om /\ ( topGen ` x ) = J ) )

Proof

Step Hyp Ref Expression
1 df-2ndc 
 |-  2ndc = { j | E. x e. TopBases ( x ~<_ _om /\ ( topGen ` x ) = j ) }
2 1 eleq2i 
 |-  ( J e. 2ndc <-> J e. { j | E. x e. TopBases ( x ~<_ _om /\ ( topGen ` x ) = j ) } )
3 simpr 
 |-  ( ( x ~<_ _om /\ ( topGen ` x ) = J ) -> ( topGen ` x ) = J )
4 fvex 
 |-  ( topGen ` x ) e. _V
5 3 4 eqeltrrdi 
 |-  ( ( x ~<_ _om /\ ( topGen ` x ) = J ) -> J e. _V )
6 5 rexlimivw 
 |-  ( E. x e. TopBases ( x ~<_ _om /\ ( topGen ` x ) = J ) -> J e. _V )
7 eqeq2 
 |-  ( j = J -> ( ( topGen ` x ) = j <-> ( topGen ` x ) = J ) )
8 7 anbi2d 
 |-  ( j = J -> ( ( x ~<_ _om /\ ( topGen ` x ) = j ) <-> ( x ~<_ _om /\ ( topGen ` x ) = J ) ) )
9 8 rexbidv 
 |-  ( j = J -> ( E. x e. TopBases ( x ~<_ _om /\ ( topGen ` x ) = j ) <-> E. x e. TopBases ( x ~<_ _om /\ ( topGen ` x ) = J ) ) )
10 6 9 elab3 
 |-  ( J e. { j | E. x e. TopBases ( x ~<_ _om /\ ( topGen ` x ) = j ) } <-> E. x e. TopBases ( x ~<_ _om /\ ( topGen ` x ) = J ) )
11 2 10 bitri 
 |-  ( J e. 2ndc <-> E. x e. TopBases ( x ~<_ _om /\ ( topGen ` x ) = J ) )