Metamath Proof Explorer

Theorem re2ndc

Description: The standard topology on the reals is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion re2ndc 
|- ( topGen ` ran (,) ) e. 2ndc

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( topGen ` ( (,) " ( QQ X. QQ ) ) ) = ( topGen ` ( (,) " ( QQ X. QQ ) ) )
2 1 tgqioo 
 |-  ( topGen ` ran (,) ) = ( topGen ` ( (,) " ( QQ X. QQ ) ) )
3 qtopbas 
 |-  ( (,) " ( QQ X. QQ ) ) e. TopBases
4 omelon 
 |-  _om e. On
5 qnnen 
 |-  QQ ~~ NN
6 xpen 
 |-  ( ( QQ ~~ NN /\ QQ ~~ NN ) -> ( QQ X. QQ ) ~~ ( NN X. NN ) )
7 5 5 6 mp2an 
 |-  ( QQ X. QQ ) ~~ ( NN X. NN )
8 xpnnen 
 |-  ( NN X. NN ) ~~ NN
9 7 8 entri 
 |-  ( QQ X. QQ ) ~~ NN
10 nnenom 
 |-  NN ~~ _om
11 9 10 entr2i 
 |-  _om ~~ ( QQ X. QQ )
12 isnumi 
 |-  ( ( _om e. On /\ _om ~~ ( QQ X. QQ ) ) -> ( QQ X. QQ ) e. dom card )
13 4 11 12 mp2an 
 |-  ( QQ X. QQ ) e. dom card
14 ioof 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
15 ffun 
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> Fun (,) )
16 14 15 ax-mp 
 |-  Fun (,)
17 qssre 
 |-  QQ C_ RR
18 ressxr 
 |-  RR C_ RR*
19 17 18 sstri 
 |-  QQ C_ RR*
20 xpss12 
 |-  ( ( QQ C_ RR* /\ QQ C_ RR* ) -> ( QQ X. QQ ) C_ ( RR* X. RR* ) )
21 19 19 20 mp2an 
 |-  ( QQ X. QQ ) C_ ( RR* X. RR* )
22 14 fdmi 
 |-  dom (,) = ( RR* X. RR* )
23 21 22 sseqtrri 
 |-  ( QQ X. QQ ) C_ dom (,)
24 fores 
 |-  ( ( Fun (,) /\ ( QQ X. QQ ) C_ dom (,) ) -> ( (,) |` ( QQ X. QQ ) ) : ( QQ X. QQ ) -onto-> ( (,) " ( QQ X. QQ ) ) )
25 16 23 24 mp2an 
 |-  ( (,) |` ( QQ X. QQ ) ) : ( QQ X. QQ ) -onto-> ( (,) " ( QQ X. QQ ) )
26 fodomnum 
 |-  ( ( QQ X. QQ ) e. dom card -> ( ( (,) |` ( QQ X. QQ ) ) : ( QQ X. QQ ) -onto-> ( (,) " ( QQ X. QQ ) ) -> ( (,) " ( QQ X. QQ ) ) ~<_ ( QQ X. QQ ) ) )
27 13 25 26 mp2 
 |-  ( (,) " ( QQ X. QQ ) ) ~<_ ( QQ X. QQ )
28 9 10 entri 
 |-  ( QQ X. QQ ) ~~ _om
29 domentr 
 |-  ( ( ( (,) " ( QQ X. QQ ) ) ~<_ ( QQ X. QQ ) /\ ( QQ X. QQ ) ~~ _om ) -> ( (,) " ( QQ X. QQ ) ) ~<_ _om )
30 27 28 29 mp2an 
 |-  ( (,) " ( QQ X. QQ ) ) ~<_ _om
31 2ndci 
 |-  ( ( ( (,) " ( QQ X. QQ ) ) e. TopBases /\ ( (,) " ( QQ X. QQ ) ) ~<_ _om ) -> ( topGen ` ( (,) " ( QQ X. QQ ) ) ) e. 2ndc )
32 3 30 31 mp2an 
 |-  ( topGen ` ( (,) " ( QQ X. QQ ) ) ) e. 2ndc
33 2 32 eqeltri 
 |-  ( topGen ` ran (,) ) e. 2ndc