Proof of Theorem alephexp1
Step | Hyp | Ref
| Expression |
1 | | alephon 9710 |
. . . 4
⊢
(ℵ‘𝐵)
∈ On |
2 | | onenon 9592 |
. . . 4
⊢
((ℵ‘𝐵)
∈ On → (ℵ‘𝐵) ∈ dom card) |
3 | 1, 2 | mp1i 13 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → (ℵ‘𝐵) ∈ dom card) |
4 | | fvex 6751 |
. . . 4
⊢
(ℵ‘𝐵)
∈ V |
5 | | simplr 769 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → 𝐵 ∈ On) |
6 | | alephgeom 9723 |
. . . . 5
⊢ (𝐵 ∈ On ↔ ω
⊆ (ℵ‘𝐵)) |
7 | 5, 6 | sylib 221 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → ω ⊆
(ℵ‘𝐵)) |
8 | | ssdomg 8699 |
. . . 4
⊢
((ℵ‘𝐵)
∈ V → (ω ⊆ (ℵ‘𝐵) → ω ≼
(ℵ‘𝐵))) |
9 | 4, 7, 8 | mpsyl 68 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → ω ≼
(ℵ‘𝐵)) |
10 | | fvex 6751 |
. . . 4
⊢
(ℵ‘𝐴)
∈ V |
11 | | ordom 7675 |
. . . . . 6
⊢ Ord
ω |
12 | | 2onn 8391 |
. . . . . 6
⊢
2o ∈ ω |
13 | | ordelss 6249 |
. . . . . 6
⊢ ((Ord
ω ∧ 2o ∈ ω) → 2o ⊆
ω) |
14 | 11, 12, 13 | mp2an 692 |
. . . . 5
⊢
2o ⊆ ω |
15 | | simpll 767 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → 𝐴 ∈ On) |
16 | | alephgeom 9723 |
. . . . . 6
⊢ (𝐴 ∈ On ↔ ω
⊆ (ℵ‘𝐴)) |
17 | 15, 16 | sylib 221 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → ω ⊆
(ℵ‘𝐴)) |
18 | 14, 17 | sstrid 3928 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → 2o ⊆
(ℵ‘𝐴)) |
19 | | ssdomg 8699 |
. . . 4
⊢
((ℵ‘𝐴)
∈ V → (2o ⊆ (ℵ‘𝐴) → 2o ≼
(ℵ‘𝐴))) |
20 | 10, 18, 19 | mpsyl 68 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → 2o ≼
(ℵ‘𝐴)) |
21 | | alephord3 9719 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ (ℵ‘𝐴) ⊆ (ℵ‘𝐵))) |
22 | | ssdomg 8699 |
. . . . . . 7
⊢
((ℵ‘𝐵)
∈ V → ((ℵ‘𝐴) ⊆ (ℵ‘𝐵) → (ℵ‘𝐴) ≼ (ℵ‘𝐵))) |
23 | 4, 22 | ax-mp 5 |
. . . . . 6
⊢
((ℵ‘𝐴)
⊆ (ℵ‘𝐵)
→ (ℵ‘𝐴)
≼ (ℵ‘𝐵)) |
24 | 21, 23 | syl6bi 256 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 → (ℵ‘𝐴) ≼ (ℵ‘𝐵))) |
25 | 24 | imp 410 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → (ℵ‘𝐴) ≼ (ℵ‘𝐵)) |
26 | 4 | canth2 8824 |
. . . . 5
⊢
(ℵ‘𝐵)
≺ 𝒫 (ℵ‘𝐵) |
27 | | sdomdom 8681 |
. . . . 5
⊢
((ℵ‘𝐵)
≺ 𝒫 (ℵ‘𝐵) → (ℵ‘𝐵) ≼ 𝒫 (ℵ‘𝐵)) |
28 | 26, 27 | ax-mp 5 |
. . . 4
⊢
(ℵ‘𝐵)
≼ 𝒫 (ℵ‘𝐵) |
29 | | domtr 8706 |
. . . 4
⊢
(((ℵ‘𝐴)
≼ (ℵ‘𝐵)
∧ (ℵ‘𝐵)
≼ 𝒫 (ℵ‘𝐵)) → (ℵ‘𝐴) ≼ 𝒫 (ℵ‘𝐵)) |
30 | 25, 28, 29 | sylancl 589 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → (ℵ‘𝐴) ≼ 𝒫 (ℵ‘𝐵)) |
31 | | mappwen 9753 |
. . 3
⊢
((((ℵ‘𝐵)
∈ dom card ∧ ω ≼ (ℵ‘𝐵)) ∧ (2o ≼
(ℵ‘𝐴) ∧
(ℵ‘𝐴) ≼
𝒫 (ℵ‘𝐵))) → ((ℵ‘𝐴) ↑m (ℵ‘𝐵)) ≈ 𝒫
(ℵ‘𝐵)) |
32 | 3, 9, 20, 30, 31 | syl22anc 839 |
. 2
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → ((ℵ‘𝐴) ↑m (ℵ‘𝐵)) ≈ 𝒫
(ℵ‘𝐵)) |
33 | 4 | pw2en 8777 |
. . 3
⊢ 𝒫
(ℵ‘𝐵) ≈
(2o ↑m (ℵ‘𝐵)) |
34 | | enen2 8812 |
. . 3
⊢
(𝒫 (ℵ‘𝐵) ≈ (2o ↑m
(ℵ‘𝐵)) →
(((ℵ‘𝐴)
↑m (ℵ‘𝐵)) ≈ 𝒫 (ℵ‘𝐵) ↔ ((ℵ‘𝐴) ↑m
(ℵ‘𝐵)) ≈
(2o ↑m (ℵ‘𝐵)))) |
35 | 33, 34 | ax-mp 5 |
. 2
⊢
(((ℵ‘𝐴)
↑m (ℵ‘𝐵)) ≈ 𝒫 (ℵ‘𝐵) ↔ ((ℵ‘𝐴) ↑m
(ℵ‘𝐵)) ≈
(2o ↑m (ℵ‘𝐵))) |
36 | 32, 35 | sylib 221 |
1
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → ((ℵ‘𝐴) ↑m (ℵ‘𝐵)) ≈ (2o
↑m (ℵ‘𝐵))) |