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 ( ℵ ‘ 𝐵 ) ) )