Theorem 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	⊢ ( ℝ × ℝ ) ≈ ℝ

Proof

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