Metamath Proof Explorer

Theorem alephexp1

Description: An exponentiation law for alephs. Lemma 6.1 of Jech p. 42. (Contributed by NM, 29-Sep-2004) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Assertion alephexp1 ⊢ A ∈ On ∧ B ∈ On ∧ A ⊆ B → ℵ ⁡ A ℵ ⁡ B ≈ 2 𝑜 ℵ ⁡ B

Proof

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