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 ⁡ . ∈ 2 nd 𝜔$

Proof

Step Hyp Ref Expression
1 eqid $⊢ topGen ⁡ . ℚ × ℚ = topGen ⁡ . ℚ × ℚ$
2 1 tgqioo $⊢ topGen ⁡ ran ⁡ . = 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 ∧ ω ≈ ℚ × ℚ → ℚ × ℚ ∈ dom ⁡ card$
13 4 11 12 mp2an $⊢ ℚ × ℚ ∈ dom ⁡ card$
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 $⊢ ℚ × ℚ ∈ dom ⁡ card → . ↾ ℚ × ℚ : ℚ × ℚ ⟶ onto . ℚ × ℚ → . ℚ × ℚ ≼ ℚ × ℚ$
27 13 25 26 mp2 $⊢ . ℚ × ℚ ≼ ℚ × ℚ$
28 9 10 entri $⊢ ℚ × ℚ ≈ ω$
29 domentr $⊢ . ℚ × ℚ ≼ ℚ × ℚ ∧ ℚ × ℚ ≈ ω → . ℚ × ℚ ≼ ω$
30 27 28 29 mp2an $⊢ . ℚ × ℚ ≼ ω$
31 2ndci $⊢ . ℚ × ℚ ∈ TopBases ∧ . ℚ × ℚ ≼ ω → topGen ⁡ . ℚ × ℚ ∈ 2 nd 𝜔$
32 3 30 31 mp2an $⊢ topGen ⁡ . ℚ × ℚ ∈ 2 nd 𝜔$
33 2 32 eqeltri $⊢ topGen ⁡ ran ⁡ . ∈ 2 nd 𝜔$