This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 (,) ) ∈ 2ndω

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 ‘ ( (,) “ ( ℚ × ℚ ) ) ) ∈ 2ndω )
32 3 30 31 mp2an ⊢ ( topGen ‘ ( (,) “ ( ℚ × ℚ ) ) ) ∈ 2ndω
33 2 32 eqeltri ⊢ ( topGen ‘ ran (,) ) ∈ 2ndω