Proof of Theorem rexpen
Step | Hyp | Ref
| Expression |
1 | | rpnnen 14795 |
. . . . . 6
⊢ ℝ
≈ 𝒫 ℕ |
2 | | nnenom 12641 |
. . . . . . 7
⊢ ℕ
≈ ω |
3 | | pwen 8018 |
. . . . . . 7
⊢ (ℕ
≈ ω → 𝒫 ℕ ≈ 𝒫
ω) |
4 | 2, 3 | ax-mp 5 |
. . . . . 6
⊢ 𝒫
ℕ ≈ 𝒫 ω |
5 | 1, 4 | entri 7896 |
. . . . 5
⊢ ℝ
≈ 𝒫 ω |
6 | | omex 8423 |
. . . . . 6
⊢ ω
∈ V |
7 | 6 | pw2en 7952 |
. . . . 5
⊢ 𝒫
ω ≈ (2𝑜 ↑𝑚
ω) |
8 | 5, 7 | entri 7896 |
. . . 4
⊢ ℝ
≈ (2𝑜 ↑𝑚
ω) |
9 | | xpen 8008 |
. . . 4
⊢ ((ℝ
≈ (2𝑜 ↑𝑚 ω) ∧
ℝ ≈ (2𝑜 ↑𝑚 ω))
→ (ℝ × ℝ) ≈ ((2𝑜
↑𝑚 ω) × (2𝑜
↑𝑚 ω))) |
10 | 8, 8, 9 | mp2an 704 |
. . 3
⊢ (ℝ
× ℝ) ≈ ((2𝑜 ↑𝑚
ω) × (2𝑜 ↑𝑚
ω)) |
11 | | 2onn 7607 |
. . . . . . . 8
⊢
2𝑜 ∈ ω |
12 | 11 | elexi 3186 |
. . . . . . 7
⊢
2𝑜 ∈ V |
13 | 12, 12, 6 | xpmapen 8013 |
. . . . . 6
⊢
((2𝑜 × 2𝑜)
↑𝑚 ω) ≈ ((2𝑜
↑𝑚 ω) × (2𝑜
↑𝑚 ω)) |
14 | 13 | ensymi 7892 |
. . . . 5
⊢
((2𝑜 ↑𝑚 ω) ×
(2𝑜 ↑𝑚 ω)) ≈
((2𝑜 × 2𝑜)
↑𝑚 ω) |
15 | | ssid 3587 |
. . . . . . . . . . . . 13
⊢
2𝑜 ⊆ 2𝑜 |
16 | | ssnnfi 8064 |
. . . . . . . . . . . . 13
⊢
((2𝑜 ∈ ω ∧ 2𝑜
⊆ 2𝑜) → 2𝑜 ∈
Fin) |
17 | 11, 15, 16 | mp2an 704 |
. . . . . . . . . . . 12
⊢
2𝑜 ∈ Fin |
18 | | xpfi 8116 |
. . . . . . . . . . . 12
⊢
((2𝑜 ∈ Fin ∧ 2𝑜 ∈
Fin) → (2𝑜 × 2𝑜) ∈
Fin) |
19 | 17, 17, 18 | mp2an 704 |
. . . . . . . . . . 11
⊢
(2𝑜 × 2𝑜) ∈
Fin |
20 | | isfinite 8432 |
. . . . . . . . . . 11
⊢
((2𝑜 × 2𝑜) ∈ Fin ↔
(2𝑜 × 2𝑜) ≺
ω) |
21 | 19, 20 | mpbi 219 |
. . . . . . . . . 10
⊢
(2𝑜 × 2𝑜) ≺
ω |
22 | 6 | canth2 7998 |
. . . . . . . . . 10
⊢ ω
≺ 𝒫 ω |
23 | | sdomtr 7983 |
. . . . . . . . . 10
⊢
(((2𝑜 × 2𝑜) ≺ ω
∧ ω ≺ 𝒫 ω) → (2𝑜 ×
2𝑜) ≺ 𝒫 ω) |
24 | 21, 22, 23 | mp2an 704 |
. . . . . . . . 9
⊢
(2𝑜 × 2𝑜) ≺ 𝒫
ω |
25 | | sdomdom 7869 |
. . . . . . . . 9
⊢
((2𝑜 × 2𝑜) ≺ 𝒫
ω → (2𝑜 × 2𝑜) ≼
𝒫 ω) |
26 | 24, 25 | ax-mp 5 |
. . . . . . . 8
⊢
(2𝑜 × 2𝑜) ≼ 𝒫
ω |
27 | | domentr 7901 |
. . . . . . . 8
⊢
(((2𝑜 × 2𝑜) ≼
𝒫 ω ∧ 𝒫 ω ≈ (2𝑜
↑𝑚 ω)) → (2𝑜 ×
2𝑜) ≼ (2𝑜
↑𝑚 ω)) |
28 | 26, 7, 27 | mp2an 704 |
. . . . . . 7
⊢
(2𝑜 × 2𝑜) ≼
(2𝑜 ↑𝑚 ω) |
29 | | mapdom1 8010 |
. . . . . . 7
⊢
((2𝑜 × 2𝑜) ≼
(2𝑜 ↑𝑚 ω) →
((2𝑜 × 2𝑜)
↑𝑚 ω) ≼ ((2𝑜
↑𝑚 ω) ↑𝑚
ω)) |
30 | 28, 29 | ax-mp 5 |
. . . . . 6
⊢
((2𝑜 × 2𝑜)
↑𝑚 ω) ≼ ((2𝑜
↑𝑚 ω) ↑𝑚
ω) |
31 | | mapxpen 8011 |
. . . . . . . 8
⊢
((2𝑜 ∈ ω ∧ ω ∈ V ∧
ω ∈ V) → ((2𝑜 ↑𝑚
ω) ↑𝑚 ω) ≈ (2𝑜
↑𝑚 (ω × ω))) |
32 | 11, 6, 6, 31 | mp3an 1416 |
. . . . . . 7
⊢
((2𝑜 ↑𝑚 ω)
↑𝑚 ω) ≈ (2𝑜
↑𝑚 (ω × ω)) |
33 | 12 | enref 7874 |
. . . . . . . 8
⊢
2𝑜 ≈ 2𝑜 |
34 | | xpomen 8721 |
. . . . . . . 8
⊢ (ω
× ω) ≈ ω |
35 | | mapen 8009 |
. . . . . . . 8
⊢
((2𝑜 ≈ 2𝑜 ∧ (ω
× ω) ≈ ω) → (2𝑜
↑𝑚 (ω × ω)) ≈
(2𝑜 ↑𝑚 ω)) |
36 | 33, 34, 35 | mp2an 704 |
. . . . . . 7
⊢
(2𝑜 ↑𝑚 (ω ×
ω)) ≈ (2𝑜 ↑𝑚
ω) |
37 | 32, 36 | entri 7896 |
. . . . . 6
⊢
((2𝑜 ↑𝑚 ω)
↑𝑚 ω) ≈ (2𝑜
↑𝑚 ω) |
38 | | domentr 7901 |
. . . . . 6
⊢
((((2𝑜 × 2𝑜)
↑𝑚 ω) ≼ ((2𝑜
↑𝑚 ω) ↑𝑚 ω) ∧
((2𝑜 ↑𝑚 ω)
↑𝑚 ω) ≈ (2𝑜
↑𝑚 ω)) → ((2𝑜 ×
2𝑜) ↑𝑚 ω) ≼
(2𝑜 ↑𝑚 ω)) |
39 | 30, 37, 38 | mp2an 704 |
. . . . 5
⊢
((2𝑜 × 2𝑜)
↑𝑚 ω) ≼ (2𝑜
↑𝑚 ω) |
40 | | endomtr 7900 |
. . . . 5
⊢
((((2𝑜 ↑𝑚 ω) ×
(2𝑜 ↑𝑚 ω)) ≈
((2𝑜 × 2𝑜)
↑𝑚 ω) ∧ ((2𝑜 ×
2𝑜) ↑𝑚 ω) ≼
(2𝑜 ↑𝑚 ω)) →
((2𝑜 ↑𝑚 ω) ×
(2𝑜 ↑𝑚 ω)) ≼
(2𝑜 ↑𝑚 ω)) |
41 | 14, 39, 40 | mp2an 704 |
. . . 4
⊢
((2𝑜 ↑𝑚 ω) ×
(2𝑜 ↑𝑚 ω)) ≼
(2𝑜 ↑𝑚 ω) |
42 | | ovex 6577 |
. . . . . . 7
⊢
(2𝑜 ↑𝑚 ω) ∈
V |
43 | | 0ex 4718 |
. . . . . . 7
⊢ ∅
∈ V |
44 | 42, 43 | xpsnen 7929 |
. . . . . 6
⊢
((2𝑜 ↑𝑚 ω) ×
{∅}) ≈ (2𝑜 ↑𝑚
ω) |
45 | 44 | ensymi 7892 |
. . . . 5
⊢
(2𝑜 ↑𝑚 ω) ≈
((2𝑜 ↑𝑚 ω) ×
{∅}) |
46 | | snfi 7923 |
. . . . . . . . . 10
⊢ {∅}
∈ Fin |
47 | | isfinite 8432 |
. . . . . . . . . 10
⊢
({∅} ∈ Fin ↔ {∅} ≺ ω) |
48 | 46, 47 | mpbi 219 |
. . . . . . . . 9
⊢ {∅}
≺ ω |
49 | | sdomtr 7983 |
. . . . . . . . 9
⊢
(({∅} ≺ ω ∧ ω ≺ 𝒫 ω)
→ {∅} ≺ 𝒫 ω) |
50 | 48, 22, 49 | mp2an 704 |
. . . . . . . 8
⊢ {∅}
≺ 𝒫 ω |
51 | | sdomdom 7869 |
. . . . . . . 8
⊢
({∅} ≺ 𝒫 ω → {∅} ≼ 𝒫
ω) |
52 | 50, 51 | ax-mp 5 |
. . . . . . 7
⊢ {∅}
≼ 𝒫 ω |
53 | | domentr 7901 |
. . . . . . 7
⊢
(({∅} ≼ 𝒫 ω ∧ 𝒫 ω ≈
(2𝑜 ↑𝑚 ω)) → {∅}
≼ (2𝑜 ↑𝑚
ω)) |
54 | 52, 7, 53 | mp2an 704 |
. . . . . 6
⊢ {∅}
≼ (2𝑜 ↑𝑚
ω) |
55 | 42 | xpdom2 7940 |
. . . . . 6
⊢
({∅} ≼ (2𝑜 ↑𝑚
ω) → ((2𝑜 ↑𝑚 ω)
× {∅}) ≼ ((2𝑜 ↑𝑚
ω) × (2𝑜 ↑𝑚
ω))) |
56 | 54, 55 | ax-mp 5 |
. . . . 5
⊢
((2𝑜 ↑𝑚 ω) ×
{∅}) ≼ ((2𝑜 ↑𝑚 ω)
× (2𝑜 ↑𝑚
ω)) |
57 | | endomtr 7900 |
. . . . 5
⊢
(((2𝑜 ↑𝑚 ω) ≈
((2𝑜 ↑𝑚 ω) × {∅})
∧ ((2𝑜 ↑𝑚 ω) ×
{∅}) ≼ ((2𝑜 ↑𝑚 ω)
× (2𝑜 ↑𝑚 ω))) →
(2𝑜 ↑𝑚 ω) ≼
((2𝑜 ↑𝑚 ω) ×
(2𝑜 ↑𝑚 ω))) |
58 | 45, 56, 57 | mp2an 704 |
. . . 4
⊢
(2𝑜 ↑𝑚 ω) ≼
((2𝑜 ↑𝑚 ω) ×
(2𝑜 ↑𝑚 ω)) |
59 | | sbth 7965 |
. . . 4
⊢
((((2𝑜 ↑𝑚 ω) ×
(2𝑜 ↑𝑚 ω)) ≼
(2𝑜 ↑𝑚 ω) ∧
(2𝑜 ↑𝑚 ω) ≼
((2𝑜 ↑𝑚 ω) ×
(2𝑜 ↑𝑚 ω))) →
((2𝑜 ↑𝑚 ω) ×
(2𝑜 ↑𝑚 ω)) ≈
(2𝑜 ↑𝑚 ω)) |
60 | 41, 58, 59 | mp2an 704 |
. . 3
⊢
((2𝑜 ↑𝑚 ω) ×
(2𝑜 ↑𝑚 ω)) ≈
(2𝑜 ↑𝑚 ω) |
61 | 10, 60 | entri 7896 |
. 2
⊢ (ℝ
× ℝ) ≈ (2𝑜 ↑𝑚
ω) |
62 | 61, 8 | entr4i 7899 |
1
⊢ (ℝ
× ℝ) ≈ ℝ |