Metamath Proof Explorer

Theorem 2ndcredom

Description: A second-countable space has at most the cardinality of the continuum. (Contributed by Mario Carneiro, 9-Apr-2015)

Ref Expression
Assertion 2ndcredom 
|- ( J e. 2ndc -> J ~<_ RR )

Proof

Step Hyp Ref Expression
1 is2ndc 
 |-  ( J e. 2ndc <-> E. x e. TopBases ( x ~<_ _om /\ ( topGen ` x ) = J ) )
2 tgdom 
 |-  ( x e. TopBases -> ( topGen ` x ) ~<_ ~P x )
3 simpr 
 |-  ( ( x e. TopBases /\ x ~<_ _om ) -> x ~<_ _om )
4 nnenom 
 |-  NN ~~ _om
5 4 ensymi 
 |-  _om ~~ NN
6 domentr 
 |-  ( ( x ~<_ _om /\ _om ~~ NN ) -> x ~<_ NN )
7 3 5 6 sylancl 
 |-  ( ( x e. TopBases /\ x ~<_ _om ) -> x ~<_ NN )
8 pwdom 
 |-  ( x ~<_ NN -> ~P x ~<_ ~P NN )
9 7 8 syl 
 |-  ( ( x e. TopBases /\ x ~<_ _om ) -> ~P x ~<_ ~P NN )
10 rpnnen 
 |-  RR ~~ ~P NN
11 10 ensymi 
 |-  ~P NN ~~ RR
12 domentr 
 |-  ( ( ~P x ~<_ ~P NN /\ ~P NN ~~ RR ) -> ~P x ~<_ RR )
13 9 11 12 sylancl 
 |-  ( ( x e. TopBases /\ x ~<_ _om ) -> ~P x ~<_ RR )
14 domtr 
 |-  ( ( ( topGen ` x ) ~<_ ~P x /\ ~P x ~<_ RR ) -> ( topGen ` x ) ~<_ RR )
15 2 13 14 syl2an2r 
 |-  ( ( x e. TopBases /\ x ~<_ _om ) -> ( topGen ` x ) ~<_ RR )
16 breq1 
 |-  ( ( topGen ` x ) = J -> ( ( topGen ` x ) ~<_ RR <-> J ~<_ RR ) )
17 15 16 syl5ibcom 
 |-  ( ( x e. TopBases /\ x ~<_ _om ) -> ( ( topGen ` x ) = J -> J ~<_ RR ) )
18 17 expimpd 
 |-  ( x e. TopBases -> ( ( x ~<_ _om /\ ( topGen ` x ) = J ) -> J ~<_ RR ) )
19 18 rexlimiv 
 |-  ( E. x e. TopBases ( x ~<_ _om /\ ( topGen ` x ) = J ) -> J ~<_ RR )
20 1 19 sylbi 
 |-  ( J e. 2ndc -> J ~<_ RR )