Step |
Hyp |
Ref |
Expression |
1 |
|
alephon |
⊢ ( ℵ ‘ 𝐵 ) ∈ On |
2 |
|
onenon |
⊢ ( ( ℵ ‘ 𝐵 ) ∈ On → ( ℵ ‘ 𝐵 ) ∈ dom card ) |
3 |
1 2
|
mp1i |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( ℵ ‘ 𝐵 ) ∈ dom card ) |
4 |
|
fvex |
⊢ ( ℵ ‘ 𝐵 ) ∈ V |
5 |
|
simplr |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → 𝐵 ∈ On ) |
6 |
|
alephgeom |
⊢ ( 𝐵 ∈ On ↔ ω ⊆ ( ℵ ‘ 𝐵 ) ) |
7 |
5 6
|
sylib |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ω ⊆ ( ℵ ‘ 𝐵 ) ) |
8 |
|
ssdomg |
⊢ ( ( ℵ ‘ 𝐵 ) ∈ V → ( ω ⊆ ( ℵ ‘ 𝐵 ) → ω ≼ ( ℵ ‘ 𝐵 ) ) ) |
9 |
4 7 8
|
mpsyl |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ω ≼ ( ℵ ‘ 𝐵 ) ) |
10 |
|
fvex |
⊢ ( ℵ ‘ 𝐴 ) ∈ V |
11 |
|
ordom |
⊢ Ord ω |
12 |
|
2onn |
⊢ 2o ∈ ω |
13 |
|
ordelss |
⊢ ( ( Ord ω ∧ 2o ∈ ω ) → 2o ⊆ ω ) |
14 |
11 12 13
|
mp2an |
⊢ 2o ⊆ ω |
15 |
|
simpll |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 ∈ On ) |
16 |
|
alephgeom |
⊢ ( 𝐴 ∈ On ↔ ω ⊆ ( ℵ ‘ 𝐴 ) ) |
17 |
15 16
|
sylib |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ω ⊆ ( ℵ ‘ 𝐴 ) ) |
18 |
14 17
|
sstrid |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → 2o ⊆ ( ℵ ‘ 𝐴 ) ) |
19 |
|
ssdomg |
⊢ ( ( ℵ ‘ 𝐴 ) ∈ V → ( 2o ⊆ ( ℵ ‘ 𝐴 ) → 2o ≼ ( ℵ ‘ 𝐴 ) ) ) |
20 |
10 18 19
|
mpsyl |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → 2o ≼ ( ℵ ‘ 𝐴 ) ) |
21 |
|
alephord3 |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ ( ℵ ‘ 𝐴 ) ⊆ ( ℵ ‘ 𝐵 ) ) ) |
22 |
|
ssdomg |
⊢ ( ( ℵ ‘ 𝐵 ) ∈ V → ( ( ℵ ‘ 𝐴 ) ⊆ ( ℵ ‘ 𝐵 ) → ( ℵ ‘ 𝐴 ) ≼ ( ℵ ‘ 𝐵 ) ) ) |
23 |
4 22
|
ax-mp |
⊢ ( ( ℵ ‘ 𝐴 ) ⊆ ( ℵ ‘ 𝐵 ) → ( ℵ ‘ 𝐴 ) ≼ ( ℵ ‘ 𝐵 ) ) |
24 |
21 23
|
syl6bi |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ( ℵ ‘ 𝐴 ) ≼ ( ℵ ‘ 𝐵 ) ) ) |
25 |
24
|
imp |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( ℵ ‘ 𝐴 ) ≼ ( ℵ ‘ 𝐵 ) ) |
26 |
4
|
canth2 |
⊢ ( ℵ ‘ 𝐵 ) ≺ 𝒫 ( ℵ ‘ 𝐵 ) |
27 |
|
sdomdom |
⊢ ( ( ℵ ‘ 𝐵 ) ≺ 𝒫 ( ℵ ‘ 𝐵 ) → ( ℵ ‘ 𝐵 ) ≼ 𝒫 ( ℵ ‘ 𝐵 ) ) |
28 |
26 27
|
ax-mp |
⊢ ( ℵ ‘ 𝐵 ) ≼ 𝒫 ( ℵ ‘ 𝐵 ) |
29 |
|
domtr |
⊢ ( ( ( ℵ ‘ 𝐴 ) ≼ ( ℵ ‘ 𝐵 ) ∧ ( ℵ ‘ 𝐵 ) ≼ 𝒫 ( ℵ ‘ 𝐵 ) ) → ( ℵ ‘ 𝐴 ) ≼ 𝒫 ( ℵ ‘ 𝐵 ) ) |
30 |
25 28 29
|
sylancl |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( ℵ ‘ 𝐴 ) ≼ 𝒫 ( ℵ ‘ 𝐵 ) ) |
31 |
|
mappwen |
⊢ ( ( ( ( ℵ ‘ 𝐵 ) ∈ dom card ∧ ω ≼ ( ℵ ‘ 𝐵 ) ) ∧ ( 2o ≼ ( ℵ ‘ 𝐴 ) ∧ ( ℵ ‘ 𝐴 ) ≼ 𝒫 ( ℵ ‘ 𝐵 ) ) ) → ( ( ℵ ‘ 𝐴 ) ↑m ( ℵ ‘ 𝐵 ) ) ≈ 𝒫 ( ℵ ‘ 𝐵 ) ) |
32 |
3 9 20 30 31
|
syl22anc |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( ( ℵ ‘ 𝐴 ) ↑m ( ℵ ‘ 𝐵 ) ) ≈ 𝒫 ( ℵ ‘ 𝐵 ) ) |
33 |
4
|
pw2en |
⊢ 𝒫 ( ℵ ‘ 𝐵 ) ≈ ( 2o ↑m ( ℵ ‘ 𝐵 ) ) |
34 |
|
enen2 |
⊢ ( 𝒫 ( ℵ ‘ 𝐵 ) ≈ ( 2o ↑m ( ℵ ‘ 𝐵 ) ) → ( ( ( ℵ ‘ 𝐴 ) ↑m ( ℵ ‘ 𝐵 ) ) ≈ 𝒫 ( ℵ ‘ 𝐵 ) ↔ ( ( ℵ ‘ 𝐴 ) ↑m ( ℵ ‘ 𝐵 ) ) ≈ ( 2o ↑m ( ℵ ‘ 𝐵 ) ) ) ) |
35 |
33 34
|
ax-mp |
⊢ ( ( ( ℵ ‘ 𝐴 ) ↑m ( ℵ ‘ 𝐵 ) ) ≈ 𝒫 ( ℵ ‘ 𝐵 ) ↔ ( ( ℵ ‘ 𝐴 ) ↑m ( ℵ ‘ 𝐵 ) ) ≈ ( 2o ↑m ( ℵ ‘ 𝐵 ) ) ) |
36 |
32 35
|
sylib |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( ( ℵ ‘ 𝐴 ) ↑m ( ℵ ‘ 𝐵 ) ) ≈ ( 2o ↑m ( ℵ ‘ 𝐵 ) ) ) |