Theorem rpnnen

Description: The cardinality of the continuum is the same as the powerset of _om . This is a stronger statement than ruc , which only asserts that RR is uncountable, i.e. has a cardinality larger than _om . The main proof is in two parts, rpnnen1 and rpnnen2 , each showing an injection in one direction, and this last part uses sbth to prove that the sets are equinumerous. By constructing explicit injections, we avoid the use of AC. (Contributed by Mario Carneiro, 13-May-2013) (Revised by Mario Carneiro, 23-Aug-2014)

	Ref	Expression
Assertion	rpnnen	$$⊢ℝ\approx 𝒫\mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		nnex	$$⊢\mathbb{N}\in \mathrm{V}$$
2		qex	$$⊢\mathbb{Q}\in \mathrm{V}$$
3	1 2	rpnnen1	$$⊢ℝ\preccurlyeq \left({\mathbb{Q}}^{\mathbb{N}}\right)$$
4		qnnen	$$⊢\mathbb{Q}\approx \mathbb{N}$$
5	1	canth2	$$⊢\mathbb{N}\prec 𝒫\mathbb{N}$$
6		ensdomtr	$$⊢\left(\mathbb{Q}\approx \mathbb{N}\wedge \mathbb{N}\prec 𝒫\mathbb{N}\right)\to \mathbb{Q}\prec 𝒫\mathbb{N}$$
7	4 5 6	mp2an	$$⊢\mathbb{Q}\prec 𝒫\mathbb{N}$$
8		sdomdom	$$⊢\mathbb{Q}\prec 𝒫\mathbb{N}\to \mathbb{Q}\preccurlyeq 𝒫\mathbb{N}$$
9		mapdom1	$$⊢\mathbb{Q}\preccurlyeq 𝒫\mathbb{N}\to \left({\mathbb{Q}}^{\mathbb{N}}\right)\preccurlyeq \left({𝒫\mathbb{N}}^{\mathbb{N}}\right)$$
10	7 8 9	mp2b	$$⊢\left({\mathbb{Q}}^{\mathbb{N}}\right)\preccurlyeq \left({𝒫\mathbb{N}}^{\mathbb{N}}\right)$$
11	1	pw2en	$$⊢𝒫\mathbb{N}\approx \left({2_{𝑜}}^{\mathbb{N}}\right)$$
12	1	enref	$$⊢\mathbb{N}\approx \mathbb{N}$$
13		mapen	$$⊢\left(𝒫\mathbb{N}\approx \left({2_{𝑜}}^{\mathbb{N}}\right)\wedge \mathbb{N}\approx \mathbb{N}\right)\to \left({𝒫\mathbb{N}}^{\mathbb{N}}\right)\approx \left({\left({2_{𝑜}}^{\mathbb{N}}\right)}^{\mathbb{N}}\right)$$
14	11 12 13	mp2an	$$⊢\left({𝒫\mathbb{N}}^{\mathbb{N}}\right)\approx \left({\left({2_{𝑜}}^{\mathbb{N}}\right)}^{\mathbb{N}}\right)$$
15		domentr	$$⊢\left(\left({\mathbb{Q}}^{\mathbb{N}}\right)\preccurlyeq \left({𝒫\mathbb{N}}^{\mathbb{N}}\right)\wedge \left({𝒫\mathbb{N}}^{\mathbb{N}}\right)\approx \left({\left({2_{𝑜}}^{\mathbb{N}}\right)}^{\mathbb{N}}\right)\right)\to \left({\mathbb{Q}}^{\mathbb{N}}\right)\preccurlyeq \left({\left({2_{𝑜}}^{\mathbb{N}}\right)}^{\mathbb{N}}\right)$$
16	10 14 15	mp2an	$$⊢\left({\mathbb{Q}}^{\mathbb{N}}\right)\preccurlyeq \left({\left({2_{𝑜}}^{\mathbb{N}}\right)}^{\mathbb{N}}\right)$$
17		2onn	$$⊢2_{𝑜}\in \mathrm{\omega }$$
18		mapxpen	$$⊢\left(2_{𝑜}\in \mathrm{\omega }\wedge \mathbb{N}\in \mathrm{V}\wedge \mathbb{N}\in \mathrm{V}\right)\to \left({\left({2_{𝑜}}^{\mathbb{N}}\right)}^{\mathbb{N}}\right)\approx \left({2_{𝑜}}^{\left(\mathbb{N}\times \mathbb{N}\right)}\right)$$
19	17 1 1 18	mp3an	$$⊢\left({\left({2_{𝑜}}^{\mathbb{N}}\right)}^{\mathbb{N}}\right)\approx \left({2_{𝑜}}^{\left(\mathbb{N}\times \mathbb{N}\right)}\right)$$
20	17	elexi	$$⊢2_{𝑜}\in \mathrm{V}$$
21	20	enref	$$⊢2_{𝑜}\approx 2_{𝑜}$$
22		xpnnen	$$⊢\left(\mathbb{N}\times \mathbb{N}\right)\approx \mathbb{N}$$
23		mapen	$$⊢\left(2_{𝑜}\approx 2_{𝑜}\wedge \left(\mathbb{N}\times \mathbb{N}\right)\approx \mathbb{N}\right)\to \left({2_{𝑜}}^{\left(\mathbb{N}\times \mathbb{N}\right)}\right)\approx \left({2_{𝑜}}^{\mathbb{N}}\right)$$
24	21 22 23	mp2an	$$⊢\left({2_{𝑜}}^{\left(\mathbb{N}\times \mathbb{N}\right)}\right)\approx \left({2_{𝑜}}^{\mathbb{N}}\right)$$
25	19 24	entri	$$⊢\left({\left({2_{𝑜}}^{\mathbb{N}}\right)}^{\mathbb{N}}\right)\approx \left({2_{𝑜}}^{\mathbb{N}}\right)$$
26	25 11	entr4i	$$⊢\left({\left({2_{𝑜}}^{\mathbb{N}}\right)}^{\mathbb{N}}\right)\approx 𝒫\mathbb{N}$$
27		domentr	$$⊢\left(\left({\mathbb{Q}}^{\mathbb{N}}\right)\preccurlyeq \left({\left({2_{𝑜}}^{\mathbb{N}}\right)}^{\mathbb{N}}\right)\wedge \left({\left({2_{𝑜}}^{\mathbb{N}}\right)}^{\mathbb{N}}\right)\approx 𝒫\mathbb{N}\right)\to \left({\mathbb{Q}}^{\mathbb{N}}\right)\preccurlyeq 𝒫\mathbb{N}$$
28	16 26 27	mp2an	$$⊢\left({\mathbb{Q}}^{\mathbb{N}}\right)\preccurlyeq 𝒫\mathbb{N}$$
29		domtr	$$⊢\left(ℝ\preccurlyeq \left({\mathbb{Q}}^{\mathbb{N}}\right)\wedge \left({\mathbb{Q}}^{\mathbb{N}}\right)\preccurlyeq 𝒫\mathbb{N}\right)\to ℝ\preccurlyeq 𝒫\mathbb{N}$$
30	3 28 29	mp2an	$$⊢ℝ\preccurlyeq 𝒫\mathbb{N}$$
31		rpnnen2	$$⊢𝒫\mathbb{N}\preccurlyeq \left[0,1\right]$$
32		reex	$$⊢ℝ\in \mathrm{V}$$
33		unitssre	$$⊢\left[0,1\right]\subseteq ℝ$$
34		ssdomg	$$⊢ℝ\in \mathrm{V}\to \left(\left[0,1\right]\subseteq ℝ\to \left[0,1\right]\preccurlyeq ℝ\right)$$
35	32 33 34	mp2	$$⊢\left[0,1\right]\preccurlyeq ℝ$$
36		domtr	$$⊢\left(𝒫\mathbb{N}\preccurlyeq \left[0,1\right]\wedge \left[0,1\right]\preccurlyeq ℝ\right)\to 𝒫\mathbb{N}\preccurlyeq ℝ$$
37	31 35 36	mp2an	$$⊢𝒫\mathbb{N}\preccurlyeq ℝ$$
38		sbth	$$⊢\left(ℝ\preccurlyeq 𝒫\mathbb{N}\wedge 𝒫\mathbb{N}\preccurlyeq ℝ\right)\to ℝ\approx 𝒫\mathbb{N}$$
39	30 37 38	mp2an	$$⊢ℝ\approx 𝒫\mathbb{N}$$