Description: The standard topology on the reals is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | re2ndc | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | |
|
2 | 1 | tgqioo | |
3 | qtopbas | |
|
4 | omelon | |
|
5 | qnnen | |
|
6 | xpen | |
|
7 | 5 5 6 | mp2an | |
8 | xpnnen | |
|
9 | 7 8 | entri | |
10 | nnenom | |
|
11 | 9 10 | entr2i | |
12 | isnumi | |
|
13 | 4 11 12 | mp2an | |
14 | ioof | |
|
15 | ffun | |
|
16 | 14 15 | ax-mp | |
17 | qssre | |
|
18 | ressxr | |
|
19 | 17 18 | sstri | |
20 | xpss12 | |
|
21 | 19 19 20 | mp2an | |
22 | 14 | fdmi | |
23 | 21 22 | sseqtrri | |
24 | fores | |
|
25 | 16 23 24 | mp2an | |
26 | fodomnum | |
|
27 | 13 25 26 | mp2 | |
28 | 9 10 | entri | |
29 | domentr | |
|
30 | 27 28 29 | mp2an | |
31 | 2ndci | |
|
32 | 3 30 31 | mp2an | |
33 | 2 32 | eqeltri | |