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 ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴𝐵 ) → ( ( ℵ ‘ 𝐴 ) ↑m ( ℵ ‘ 𝐵 ) ) ≈ ( 2om ( ℵ ‘ 𝐵 ) ) )

Proof

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 𝒫 ( ℵ ‘ 𝐵 ) ≈ ( 2om ( ℵ ‘ 𝐵 ) )
34 enen2 ( 𝒫 ( ℵ ‘ 𝐵 ) ≈ ( 2om ( ℵ ‘ 𝐵 ) ) → ( ( ( ℵ ‘ 𝐴 ) ↑m ( ℵ ‘ 𝐵 ) ) ≈ 𝒫 ( ℵ ‘ 𝐵 ) ↔ ( ( ℵ ‘ 𝐴 ) ↑m ( ℵ ‘ 𝐵 ) ) ≈ ( 2om ( ℵ ‘ 𝐵 ) ) ) )
35 33 34 ax-mp ( ( ( ℵ ‘ 𝐴 ) ↑m ( ℵ ‘ 𝐵 ) ) ≈ 𝒫 ( ℵ ‘ 𝐵 ) ↔ ( ( ℵ ‘ 𝐴 ) ↑m ( ℵ ‘ 𝐵 ) ) ≈ ( 2om ( ℵ ‘ 𝐵 ) ) )
36 32 35 sylib ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴𝐵 ) → ( ( ℵ ‘ 𝐴 ) ↑m ( ℵ ‘ 𝐵 ) ) ≈ ( 2om ( ℵ ‘ 𝐵 ) ) )