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ω