Proof of Theorem alephexp1
| Step | Hyp | Ref
| Expression |
| 1 | | alephon 10109 |
. . . 4
⊢
(ℵ‘𝐵)
∈ On |
| 2 | | onenon 9989 |
. . . 4
⊢
((ℵ‘𝐵)
∈ On → (ℵ‘𝐵) ∈ dom card) |
| 3 | 1, 2 | mp1i 13 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → (ℵ‘𝐵) ∈ dom card) |
| 4 | | fvex 6919 |
. . . 4
⊢
(ℵ‘𝐵)
∈ V |
| 5 | | simplr 769 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → 𝐵 ∈ On) |
| 6 | | alephgeom 10122 |
. . . . 5
⊢ (𝐵 ∈ On ↔ ω
⊆ (ℵ‘𝐵)) |
| 7 | 5, 6 | sylib 218 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → ω ⊆
(ℵ‘𝐵)) |
| 8 | | ssdomg 9040 |
. . . 4
⊢
((ℵ‘𝐵)
∈ V → (ω ⊆ (ℵ‘𝐵) → ω ≼
(ℵ‘𝐵))) |
| 9 | 4, 7, 8 | mpsyl 68 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → ω ≼
(ℵ‘𝐵)) |
| 10 | | fvex 6919 |
. . . 4
⊢
(ℵ‘𝐴)
∈ V |
| 11 | | ordom 7897 |
. . . . . 6
⊢ Ord
ω |
| 12 | | 2onn 8680 |
. . . . . 6
⊢
2o ∈ ω |
| 13 | | ordelss 6400 |
. . . . . 6
⊢ ((Ord
ω ∧ 2o ∈ ω) → 2o ⊆
ω) |
| 14 | 11, 12, 13 | mp2an 692 |
. . . . 5
⊢
2o ⊆ ω |
| 15 | | simpll 767 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → 𝐴 ∈ On) |
| 16 | | alephgeom 10122 |
. . . . . 6
⊢ (𝐴 ∈ On ↔ ω
⊆ (ℵ‘𝐴)) |
| 17 | 15, 16 | sylib 218 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → ω ⊆
(ℵ‘𝐴)) |
| 18 | 14, 17 | sstrid 3995 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → 2o ⊆
(ℵ‘𝐴)) |
| 19 | | ssdomg 9040 |
. . . 4
⊢
((ℵ‘𝐴)
∈ V → (2o ⊆ (ℵ‘𝐴) → 2o ≼
(ℵ‘𝐴))) |
| 20 | 10, 18, 19 | mpsyl 68 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → 2o ≼
(ℵ‘𝐴)) |
| 21 | | alephord3 10118 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ (ℵ‘𝐴) ⊆ (ℵ‘𝐵))) |
| 22 | | ssdomg 9040 |
. . . . . . 7
⊢
((ℵ‘𝐵)
∈ V → ((ℵ‘𝐴) ⊆ (ℵ‘𝐵) → (ℵ‘𝐴) ≼ (ℵ‘𝐵))) |
| 23 | 4, 22 | ax-mp 5 |
. . . . . 6
⊢
((ℵ‘𝐴)
⊆ (ℵ‘𝐵)
→ (ℵ‘𝐴)
≼ (ℵ‘𝐵)) |
| 24 | 21, 23 | biimtrdi 253 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 → (ℵ‘𝐴) ≼ (ℵ‘𝐵))) |
| 25 | 24 | imp 406 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → (ℵ‘𝐴) ≼ (ℵ‘𝐵)) |
| 26 | 4 | canth2 9170 |
. . . . 5
⊢
(ℵ‘𝐵)
≺ 𝒫 (ℵ‘𝐵) |
| 27 | | sdomdom 9020 |
. . . . 5
⊢
((ℵ‘𝐵)
≺ 𝒫 (ℵ‘𝐵) → (ℵ‘𝐵) ≼ 𝒫 (ℵ‘𝐵)) |
| 28 | 26, 27 | ax-mp 5 |
. . . 4
⊢
(ℵ‘𝐵)
≼ 𝒫 (ℵ‘𝐵) |
| 29 | | domtr 9047 |
. . . 4
⊢
(((ℵ‘𝐴)
≼ (ℵ‘𝐵)
∧ (ℵ‘𝐵)
≼ 𝒫 (ℵ‘𝐵)) → (ℵ‘𝐴) ≼ 𝒫 (ℵ‘𝐵)) |
| 30 | 25, 28, 29 | sylancl 586 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → (ℵ‘𝐴) ≼ 𝒫 (ℵ‘𝐵)) |
| 31 | | mappwen 10152 |
. . 3
⊢
((((ℵ‘𝐵)
∈ dom card ∧ ω ≼ (ℵ‘𝐵)) ∧ (2o ≼
(ℵ‘𝐴) ∧
(ℵ‘𝐴) ≼
𝒫 (ℵ‘𝐵))) → ((ℵ‘𝐴) ↑m (ℵ‘𝐵)) ≈ 𝒫
(ℵ‘𝐵)) |
| 32 | 3, 9, 20, 30, 31 | syl22anc 839 |
. 2
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → ((ℵ‘𝐴) ↑m (ℵ‘𝐵)) ≈ 𝒫
(ℵ‘𝐵)) |
| 33 | 4 | pw2en 9119 |
. . 3
⊢ 𝒫
(ℵ‘𝐵) ≈
(2o ↑m (ℵ‘𝐵)) |
| 34 | | enen2 9158 |
. . 3
⊢
(𝒫 (ℵ‘𝐵) ≈ (2o ↑m
(ℵ‘𝐵)) →
(((ℵ‘𝐴)
↑m (ℵ‘𝐵)) ≈ 𝒫 (ℵ‘𝐵) ↔ ((ℵ‘𝐴) ↑m
(ℵ‘𝐵)) ≈
(2o ↑m (ℵ‘𝐵)))) |
| 35 | 33, 34 | ax-mp 5 |
. 2
⊢
(((ℵ‘𝐴)
↑m (ℵ‘𝐵)) ≈ 𝒫 (ℵ‘𝐵) ↔ ((ℵ‘𝐴) ↑m
(ℵ‘𝐵)) ≈
(2o ↑m (ℵ‘𝐵))) |
| 36 | 32, 35 | sylib 218 |
1
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → ((ℵ‘𝐴) ↑m (ℵ‘𝐵)) ≈ (2o
↑m (ℵ‘𝐵))) |