Theorem re2ndc

Description: The standard topology on the reals is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015)

	Ref	Expression
Assertion	re2ndc	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in 2^{nd}𝜔$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{topGen}\left(\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\right)=\mathrm{topGen}\left(\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\right)$$
2	1	tgqioo	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{topGen}\left(\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\right)$$
3		qtopbas	$$⊢\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\in \mathrm{TopBases}$$
4		omelon	$$⊢\mathrm{\omega }\in \mathrm{On}$$
5		qnnen	$$⊢\mathbb{Q}\approx \mathbb{N}$$
6		xpen	$$⊢\left(\mathbb{Q}\approx \mathbb{N}\wedge \mathbb{Q}\approx \mathbb{N}\right)\to \left(\mathbb{Q}\times \mathbb{Q}\right)\approx \left(\mathbb{N}\times \mathbb{N}\right)$$
7	5 5 6	mp2an	$$⊢\left(\mathbb{Q}\times \mathbb{Q}\right)\approx \left(\mathbb{N}\times \mathbb{N}\right)$$
8		xpnnen	$$⊢\left(\mathbb{N}\times \mathbb{N}\right)\approx \mathbb{N}$$
9	7 8	entri	$$⊢\left(\mathbb{Q}\times \mathbb{Q}\right)\approx \mathbb{N}$$
10		nnenom	$$⊢\mathbb{N}\approx \mathrm{\omega }$$
11	9 10	entr2i	$$⊢\mathrm{\omega }\approx \left(\mathbb{Q}\times \mathbb{Q}\right)$$
12		isnumi	$$⊢\left(\mathrm{\omega }\in \mathrm{On}\wedge \mathrm{\omega }\approx \left(\mathbb{Q}\times \mathbb{Q}\right)\right)\to \mathbb{Q}\times \mathbb{Q}\in \mathrm{dom}\mathrm{card}$$
13	4 11 12	mp2an	$$⊢\mathbb{Q}\times \mathbb{Q}\in \mathrm{dom}\mathrm{card}$$
14		ioof	$$⊢\left(.\right):{ℝ}^{*}\times {ℝ}^{*}⟶𝒫ℝ$$
15		ffun	$$⊢\left(.\right):{ℝ}^{*}\times {ℝ}^{*}⟶𝒫ℝ\to \mathrm{Fun}\left(.\right)$$
16	14 15	ax-mp	$$⊢\mathrm{Fun}\left(.\right)$$
17		qssre	$$⊢\mathbb{Q}\subseteq ℝ$$
18		ressxr	$$⊢ℝ\subseteq {ℝ}^{*}$$
19	17 18	sstri	$$⊢\mathbb{Q}\subseteq {ℝ}^{*}$$
20		xpss12	$$⊢\left(\mathbb{Q}\subseteq {ℝ}^{*}\wedge \mathbb{Q}\subseteq {ℝ}^{*}\right)\to \mathbb{Q}\times \mathbb{Q}\subseteq {ℝ}^{*}\times {ℝ}^{*}$$
21	19 19 20	mp2an	$$⊢\mathbb{Q}\times \mathbb{Q}\subseteq {ℝ}^{*}\times {ℝ}^{*}$$
22	14	fdmi	$$⊢\mathrm{dom}\left(.\right)={ℝ}^{*}\times {ℝ}^{*}$$
23	21 22	sseqtrri	$$⊢\mathbb{Q}\times \mathbb{Q}\subseteq \mathrm{dom}\left(.\right)$$
24		fores	$$⊢\left(\mathrm{Fun}\left(.\right)\wedge \mathbb{Q}\times \mathbb{Q}\subseteq \mathrm{dom}\left(.\right)\right)\to \left({\left(.\right)\upharpoonright }_{\left(\mathbb{Q}\times \mathbb{Q}\right)}\right):\mathbb{Q}\times \mathbb{Q}\underset{onto}{⟶}\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]$$
25	16 23 24	mp2an	$$⊢\left({\left(.\right)\upharpoonright }_{\left(\mathbb{Q}\times \mathbb{Q}\right)}\right):\mathbb{Q}\times \mathbb{Q}\underset{onto}{⟶}\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]$$
26		fodomnum	$$⊢\mathbb{Q}\times \mathbb{Q}\in \mathrm{dom}\mathrm{card}\to \left(\left({\left(.\right)\upharpoonright }_{\left(\mathbb{Q}\times \mathbb{Q}\right)}\right):\mathbb{Q}\times \mathbb{Q}\underset{onto}{⟶}\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\to \left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\preccurlyeq \left(\mathbb{Q}\times \mathbb{Q}\right)\right)$$
27	13 25 26	mp2	$$⊢\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\preccurlyeq \left(\mathbb{Q}\times \mathbb{Q}\right)$$
28	9 10	entri	$$⊢\left(\mathbb{Q}\times \mathbb{Q}\right)\approx \mathrm{\omega }$$
29		domentr	$$⊢\left(\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\preccurlyeq \left(\mathbb{Q}\times \mathbb{Q}\right)\wedge \left(\mathbb{Q}\times \mathbb{Q}\right)\approx \mathrm{\omega }\right)\to \left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\preccurlyeq \mathrm{\omega }$$
30	27 28 29	mp2an	$$⊢\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\preccurlyeq \mathrm{\omega }$$
31		2ndci	$$⊢\left(\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\in \mathrm{TopBases}\wedge \left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\preccurlyeq \mathrm{\omega }\right)\to \mathrm{topGen}\left(\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\right)\in 2^{nd}𝜔$$
32	3 30 31	mp2an	$$⊢\mathrm{topGen}\left(\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\right)\in 2^{nd}𝜔$$
33	2 32	eqeltri	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in 2^{nd}𝜔$$