Metamath Proof Explorer


Theorem 2ndci

Description: A countable basis generates a second-countable topology. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion 2ndci
|- ( ( B e. TopBases /\ B ~<_ _om ) -> ( topGen ` B ) e. 2ndc )

Proof

Step Hyp Ref Expression
1 simpl
 |-  ( ( B e. TopBases /\ B ~<_ _om ) -> B e. TopBases )
2 simpr
 |-  ( ( B e. TopBases /\ B ~<_ _om ) -> B ~<_ _om )
3 eqidd
 |-  ( ( B e. TopBases /\ B ~<_ _om ) -> ( topGen ` B ) = ( topGen ` B ) )
4 breq1
 |-  ( x = B -> ( x ~<_ _om <-> B ~<_ _om ) )
5 fveqeq2
 |-  ( x = B -> ( ( topGen ` x ) = ( topGen ` B ) <-> ( topGen ` B ) = ( topGen ` B ) ) )
6 4 5 anbi12d
 |-  ( x = B -> ( ( x ~<_ _om /\ ( topGen ` x ) = ( topGen ` B ) ) <-> ( B ~<_ _om /\ ( topGen ` B ) = ( topGen ` B ) ) ) )
7 6 rspcev
 |-  ( ( B e. TopBases /\ ( B ~<_ _om /\ ( topGen ` B ) = ( topGen ` B ) ) ) -> E. x e. TopBases ( x ~<_ _om /\ ( topGen ` x ) = ( topGen ` B ) ) )
8 1 2 3 7 syl12anc
 |-  ( ( B e. TopBases /\ B ~<_ _om ) -> E. x e. TopBases ( x ~<_ _om /\ ( topGen ` x ) = ( topGen ` B ) ) )
9 is2ndc
 |-  ( ( topGen ` B ) e. 2ndc <-> E. x e. TopBases ( x ~<_ _om /\ ( topGen ` x ) = ( topGen ` B ) ) )
10 8 9 sylibr
 |-  ( ( B e. TopBases /\ B ~<_ _om ) -> ( topGen ` B ) e. 2ndc )