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 topGenran.2nd𝜔

Proof

Step Hyp Ref Expression
1 eqid topGen.×=topGen.×
2 1 tgqioo topGenran.=topGen.×
3 qtopbas .×TopBases
4 omelon ωOn
5 qnnen
6 xpen ××
7 5 5 6 mp2an ××
8 xpnnen ×
9 7 8 entri ×
10 nnenom ω
11 9 10 entr2i ω×
12 isnumi ωOnω××domcard
13 4 11 12 mp2an ×domcard
14 ioof .:*×*𝒫
15 ffun .:*×*𝒫Fun.
16 14 15 ax-mp Fun.
17 qssre
18 ressxr *
19 17 18 sstri *
20 xpss12 **×*×*
21 19 19 20 mp2an ×*×*
22 14 fdmi dom.=*×*
23 21 22 sseqtrri ×dom.
24 fores Fun.×dom..×:×onto.×
25 16 23 24 mp2an .×:×onto.×
26 fodomnum ×domcard.×:×onto.×.××
27 13 25 26 mp2 .××
28 9 10 entri ×ω
29 domentr .×××ω.×ω
30 27 28 29 mp2an .×ω
31 2ndci .×TopBases.×ωtopGen.×2nd𝜔
32 3 30 31 mp2an topGen.×2nd𝜔
33 2 32 eqeltri topGenran.2nd𝜔