rexpen

Description: The real numbers are equinumerous to their own Cartesian product, even though it is not necessarily true that RR is well-orderable (so we cannot use infxpidm2 directly). (Contributed by NM, 30-Jul-2004) (Revised by Mario Carneiro, 16-Jun-2013)

		Ref	Expression
	Assertion	rexpen	$⊢ ℝ^{2} \approx ℝ$

Proof

Step	Hyp	Ref	Expression
1		rpnnen	$⊢ ℝ \approx 𝒫 ℕ$
2		nnenom	$⊢ ℕ \approx ω$
3		pwen	$⊢ ℕ \approx ω \to 𝒫 ℕ \approx 𝒫 ω$
4	2 3	ax-mp	$⊢ 𝒫 ℕ \approx 𝒫 ω$
5	1 4	entri	$⊢ ℝ \approx 𝒫 ω$
6		omex	$⊢ ω \in V$
7	6	pw2en	$⊢ 𝒫 ω \approx ({2_{𝑜}}^{ω})$
8	5 7	entri	$⊢ ℝ \approx ({2_{𝑜}}^{ω})$
9		xpen	$⊢ (ℝ \approx ({2_{𝑜}}^{ω}) \land ℝ \approx ({2_{𝑜}}^{ω})) \to ℝ^{2} \approx (({2_{𝑜}}^{ω}) \times ({2_{𝑜}}^{ω}))$
10	8 8 9	mp2an	$⊢ ℝ^{2} \approx (({2_{𝑜}}^{ω}) \times ({2_{𝑜}}^{ω}))$
11		2onn	$⊢ 2_{𝑜} \in ω$
12	11	elexi	$⊢ 2_{𝑜} \in V$
13	12 12 6	xpmapen	$⊢ ({(2_{𝑜} \times 2_{𝑜})}^{ω}) \approx (({2_{𝑜}}^{ω}) \times ({2_{𝑜}}^{ω}))$
14	13	ensymi	$⊢ (({2_{𝑜}}^{ω}) \times ({2_{𝑜}}^{ω})) \approx ({(2_{𝑜} \times 2_{𝑜})}^{ω})$
15		ssid	$⊢ 2_{𝑜} \subseteq 2_{𝑜}$
16		ssnnfi	$⊢ (2_{𝑜} \in ω \land 2_{𝑜} \subseteq 2_{𝑜}) \to 2_{𝑜} \in Fin$
17	11 15 16	mp2an	$⊢ 2_{𝑜} \in Fin$
18		xpfi	$⊢ (2_{𝑜} \in Fin \land 2_{𝑜} \in Fin) \to 2_{𝑜} \times 2_{𝑜} \in Fin$
19	17 17 18	mp2an	$⊢ 2_{𝑜} \times 2_{𝑜} \in Fin$
20		isfinite	$⊢ 2_{𝑜} \times 2_{𝑜} \in Fin \leftrightarrow (2_{𝑜} \times 2_{𝑜}) ≺ ω$
21	19 20	mpbi	$⊢ (2_{𝑜} \times 2_{𝑜}) ≺ ω$
22	6	canth2	$⊢ ω ≺ 𝒫 ω$
23		sdomtr	$⊢ ((2_{𝑜} \times 2_{𝑜}) ≺ ω \land ω ≺ 𝒫 ω) \to (2_{𝑜} \times 2_{𝑜}) ≺ 𝒫 ω$
24	21 22 23	mp2an	$⊢ (2_{𝑜} \times 2_{𝑜}) ≺ 𝒫 ω$
25		sdomdom	$⊢ (2_{𝑜} \times 2_{𝑜}) ≺ 𝒫 ω \to (2_{𝑜} \times 2_{𝑜}) ≼ 𝒫 ω$
26	24 25	ax-mp	$⊢ (2_{𝑜} \times 2_{𝑜}) ≼ 𝒫 ω$
27		domentr	$⊢ ((2_{𝑜} \times 2_{𝑜}) ≼ 𝒫 ω \land 𝒫 ω \approx ({2_{𝑜}}^{ω})) \to (2_{𝑜} \times 2_{𝑜}) ≼ ({2_{𝑜}}^{ω})$
28	26 7 27	mp2an	$⊢ (2_{𝑜} \times 2_{𝑜}) ≼ ({2_{𝑜}}^{ω})$
29		mapdom1	$⊢ (2_{𝑜} \times 2_{𝑜}) ≼ ({2_{𝑜}}^{ω}) \to ({(2_{𝑜} \times 2_{𝑜})}^{ω}) ≼ ({({2_{𝑜}}^{ω})}^{ω})$
30	28 29	ax-mp	$⊢ ({(2_{𝑜} \times 2_{𝑜})}^{ω}) ≼ ({({2_{𝑜}}^{ω})}^{ω})$
31		mapxpen	$⊢ (2_{𝑜} \in ω \land ω \in V \land ω \in V) \to ({({2_{𝑜}}^{ω})}^{ω}) \approx ({2_{𝑜}}^{(ω \times ω)})$
32	11 6 6 31	mp3an	$⊢ ({({2_{𝑜}}^{ω})}^{ω}) \approx ({2_{𝑜}}^{(ω \times ω)})$
33	12	enref	$⊢ 2_{𝑜} \approx 2_{𝑜}$
34		xpomen	$⊢ (ω \times ω) \approx ω$
35		mapen	$⊢ (2_{𝑜} \approx 2_{𝑜} \land (ω \times ω) \approx ω) \to ({2_{𝑜}}^{(ω \times ω)}) \approx ({2_{𝑜}}^{ω})$
36	33 34 35	mp2an	$⊢ ({2_{𝑜}}^{(ω \times ω)}) \approx ({2_{𝑜}}^{ω})$
37	32 36	entri	$⊢ ({({2_{𝑜}}^{ω})}^{ω}) \approx ({2_{𝑜}}^{ω})$
38		domentr	$⊢ (({(2_{𝑜} \times 2_{𝑜})}^{ω}) ≼ ({({2_{𝑜}}^{ω})}^{ω}) \land ({({2_{𝑜}}^{ω})}^{ω}) \approx ({2_{𝑜}}^{ω})) \to ({(2_{𝑜} \times 2_{𝑜})}^{ω}) ≼ ({2_{𝑜}}^{ω})$
39	30 37 38	mp2an	$⊢ ({(2_{𝑜} \times 2_{𝑜})}^{ω}) ≼ ({2_{𝑜}}^{ω})$
40		endomtr	$⊢ ((({2_{𝑜}}^{ω}) \times ({2_{𝑜}}^{ω})) \approx ({(2_{𝑜} \times 2_{𝑜})}^{ω}) \land ({(2_{𝑜} \times 2_{𝑜})}^{ω}) ≼ ({2_{𝑜}}^{ω})) \to (({2_{𝑜}}^{ω}) \times ({2_{𝑜}}^{ω})) ≼ ({2_{𝑜}}^{ω})$
41	14 39 40	mp2an	$⊢ (({2_{𝑜}}^{ω}) \times ({2_{𝑜}}^{ω})) ≼ ({2_{𝑜}}^{ω})$
42		ovex	$⊢ {2_{𝑜}}^{ω} \in V$
43		0ex	$⊢ \emptyset \in V$
44	42 43	xpsnen	$⊢ (({2_{𝑜}}^{ω}) \times \{\emptyset\}) \approx ({2_{𝑜}}^{ω})$
45	44	ensymi	$⊢ ({2_{𝑜}}^{ω}) \approx (({2_{𝑜}}^{ω}) \times \{\emptyset\})$
46		snfi	$⊢ \{\emptyset\} \in Fin$
47		isfinite	$⊢ \{\emptyset\} \in Fin \leftrightarrow \{\emptyset\} ≺ ω$
48	46 47	mpbi	$⊢ \{\emptyset\} ≺ ω$
49		sdomtr	$⊢ (\{\emptyset\} ≺ ω \land ω ≺ 𝒫 ω) \to \{\emptyset\} ≺ 𝒫 ω$
50	48 22 49	mp2an	$⊢ \{\emptyset\} ≺ 𝒫 ω$
51		sdomdom	$⊢ \{\emptyset\} ≺ 𝒫 ω \to \{\emptyset\} ≼ 𝒫 ω$
52	50 51	ax-mp	$⊢ \{\emptyset\} ≼ 𝒫 ω$
53		domentr	$⊢ (\{\emptyset\} ≼ 𝒫 ω \land 𝒫 ω \approx ({2_{𝑜}}^{ω})) \to \{\emptyset\} ≼ ({2_{𝑜}}^{ω})$
54	52 7 53	mp2an	$⊢ \{\emptyset\} ≼ ({2_{𝑜}}^{ω})$
55	42	xpdom2	$⊢ \{\emptyset\} ≼ ({2_{𝑜}}^{ω}) \to (({2_{𝑜}}^{ω}) \times \{\emptyset\}) ≼ (({2_{𝑜}}^{ω}) \times ({2_{𝑜}}^{ω}))$
56	54 55	ax-mp	$⊢ (({2_{𝑜}}^{ω}) \times \{\emptyset\}) ≼ (({2_{𝑜}}^{ω}) \times ({2_{𝑜}}^{ω}))$
57		endomtr	$⊢ (({2_{𝑜}}^{ω}) \approx (({2_{𝑜}}^{ω}) \times \{\emptyset\}) \land (({2_{𝑜}}^{ω}) \times \{\emptyset\}) ≼ (({2_{𝑜}}^{ω}) \times ({2_{𝑜}}^{ω}))) \to ({2_{𝑜}}^{ω}) ≼ (({2_{𝑜}}^{ω}) \times ({2_{𝑜}}^{ω}))$
58	45 56 57	mp2an	$⊢ ({2_{𝑜}}^{ω}) ≼ (({2_{𝑜}}^{ω}) \times ({2_{𝑜}}^{ω}))$
59		sbth	$⊢ ((({2_{𝑜}}^{ω}) \times ({2_{𝑜}}^{ω})) ≼ ({2_{𝑜}}^{ω}) \land ({2_{𝑜}}^{ω}) ≼ (({2_{𝑜}}^{ω}) \times ({2_{𝑜}}^{ω}))) \to (({2_{𝑜}}^{ω}) \times ({2_{𝑜}}^{ω})) \approx ({2_{𝑜}}^{ω})$
60	41 58 59	mp2an	$⊢ (({2_{𝑜}}^{ω}) \times ({2_{𝑜}}^{ω})) \approx ({2_{𝑜}}^{ω})$
61	10 60	entri	$⊢ ℝ^{2} \approx ({2_{𝑜}}^{ω})$
62	61 8	entr4i	$⊢ ℝ^{2} \approx ℝ$

Metamath Proof Explorer

Theorem rexpen

Proof