Theorem alephexp2

Description: An expression equinumerous to 2 to an aleph power. The proof equates the two laws for cardinal exponentiation alephexp1 (which works if the base is less than or equal to the exponent) and infmap (which works if the exponent is less than or equal to the base). They can be equated only when the base is equal to the exponent, and this is the result. (Contributed by NM, 23-Oct-2004)

	Ref	Expression
Assertion	alephexp2	⊢ ( 𝐴 ∈ On → ( 2o ↑m ( ℵ ‘ 𝐴 ) ) ≈ { 𝑥 ∣ ( 𝑥 ⊆ ( ℵ ‘ 𝐴 ) ∧ 𝑥 ≈ ( ℵ ‘ 𝐴 ) ) } )

Proof

Step	Hyp	Ref	Expression
1		alephgeom	⊢ ( 𝐴 ∈ On ↔ ω ⊆ ( ℵ ‘ 𝐴 ) )
2		fvex	⊢ ( ℵ ‘ 𝐴 ) ∈ V
3		ssdomg	⊢ ( ( ℵ ‘ 𝐴 ) ∈ V → ( ω ⊆ ( ℵ ‘ 𝐴 ) → ω ≼ ( ℵ ‘ 𝐴 ) ) )
4	2 3	ax-mp	⊢ ( ω ⊆ ( ℵ ‘ 𝐴 ) → ω ≼ ( ℵ ‘ 𝐴 ) )
5	1 4	sylbi	⊢ ( 𝐴 ∈ On → ω ≼ ( ℵ ‘ 𝐴 ) )
6		domrefg	⊢ ( ( ℵ ‘ 𝐴 ) ∈ V → ( ℵ ‘ 𝐴 ) ≼ ( ℵ ‘ 𝐴 ) )
7	2 6	ax-mp	⊢ ( ℵ ‘ 𝐴 ) ≼ ( ℵ ‘ 𝐴 )
8		infmap	⊢ ( ( ω ≼ ( ℵ ‘ 𝐴 ) ∧ ( ℵ ‘ 𝐴 ) ≼ ( ℵ ‘ 𝐴 ) ) → ( ( ℵ ‘ 𝐴 ) ↑m ( ℵ ‘ 𝐴 ) ) ≈ { 𝑥 ∣ ( 𝑥 ⊆ ( ℵ ‘ 𝐴 ) ∧ 𝑥 ≈ ( ℵ ‘ 𝐴 ) ) } )
9	5 7 8	sylancl	⊢ ( 𝐴 ∈ On → ( ( ℵ ‘ 𝐴 ) ↑m ( ℵ ‘ 𝐴 ) ) ≈ { 𝑥 ∣ ( 𝑥 ⊆ ( ℵ ‘ 𝐴 ) ∧ 𝑥 ≈ ( ℵ ‘ 𝐴 ) ) } )
10		pm3.2	⊢ ( 𝐴 ∈ On → ( 𝐴 ∈ On → ( 𝐴 ∈ On ∧ 𝐴 ∈ On ) ) )
11	10	pm2.43i	⊢ ( 𝐴 ∈ On → ( 𝐴 ∈ On ∧ 𝐴 ∈ On ) )
12		ssid	⊢ 𝐴 ⊆ 𝐴
13		alephexp1	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ∈ On ) ∧ 𝐴 ⊆ 𝐴 ) → ( ( ℵ ‘ 𝐴 ) ↑m ( ℵ ‘ 𝐴 ) ) ≈ ( 2o ↑m ( ℵ ‘ 𝐴 ) ) )
14	11 12 13	sylancl	⊢ ( 𝐴 ∈ On → ( ( ℵ ‘ 𝐴 ) ↑m ( ℵ ‘ 𝐴 ) ) ≈ ( 2o ↑m ( ℵ ‘ 𝐴 ) ) )
15		enen1	⊢ ( ( ( ℵ ‘ 𝐴 ) ↑m ( ℵ ‘ 𝐴 ) ) ≈ ( 2o ↑m ( ℵ ‘ 𝐴 ) ) → ( ( ( ℵ ‘ 𝐴 ) ↑m ( ℵ ‘ 𝐴 ) ) ≈ { 𝑥 ∣ ( 𝑥 ⊆ ( ℵ ‘ 𝐴 ) ∧ 𝑥 ≈ ( ℵ ‘ 𝐴 ) ) } ↔ ( 2o ↑m ( ℵ ‘ 𝐴 ) ) ≈ { 𝑥 ∣ ( 𝑥 ⊆ ( ℵ ‘ 𝐴 ) ∧ 𝑥 ≈ ( ℵ ‘ 𝐴 ) ) } ) )
16	14 15	syl	⊢ ( 𝐴 ∈ On → ( ( ( ℵ ‘ 𝐴 ) ↑m ( ℵ ‘ 𝐴 ) ) ≈ { 𝑥 ∣ ( 𝑥 ⊆ ( ℵ ‘ 𝐴 ) ∧ 𝑥 ≈ ( ℵ ‘ 𝐴 ) ) } ↔ ( 2o ↑m ( ℵ ‘ 𝐴 ) ) ≈ { 𝑥 ∣ ( 𝑥 ⊆ ( ℵ ‘ 𝐴 ) ∧ 𝑥 ≈ ( ℵ ‘ 𝐴 ) ) } ) )
17	9 16	mpbid	⊢ ( 𝐴 ∈ On → ( 2o ↑m ( ℵ ‘ 𝐴 ) ) ≈ { 𝑥 ∣ ( 𝑥 ⊆ ( ℵ ‘ 𝐴 ) ∧ 𝑥 ≈ ( ℵ ‘ 𝐴 ) ) } )