This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ℵ ‘ 𝐵 ) ) ≈ ( 2o ↑m ( ℵ ‘ 𝐵 ) ) )

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 biimtrdi ⊢ ( ( 𝐴 ∈ 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 ( ℵ ‘ 𝐵 ) ) )