Theorem alephmul

Description: The product of two alephs is their maximum. Equation 6.1 of Jech p. 42. (Contributed by NM, 29-Sep-2004) (Revised by Mario Carneiro, 30-Apr-2015)

	Ref	Expression
Assertion	alephmul	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( ℵ ‘ 𝐴 ) × ( ℵ ‘ 𝐵 ) ) ≈ ( ( ℵ ‘ 𝐴 ) ∪ ( ℵ ‘ 𝐵 ) ) )

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		alephon	⊢ ( ℵ ‘ 𝐴 ) ∈ On
7		onenon	⊢ ( ( ℵ ‘ 𝐴 ) ∈ On → ( ℵ ‘ 𝐴 ) ∈ dom card )
8	6 7	ax-mp	⊢ ( ℵ ‘ 𝐴 ) ∈ dom card
9	5 8	jctil	⊢ ( 𝐴 ∈ On → ( ( ℵ ‘ 𝐴 ) ∈ dom card ∧ ω ≼ ( ℵ ‘ 𝐴 ) ) )
10		alephgeom	⊢ ( 𝐵 ∈ On ↔ ω ⊆ ( ℵ ‘ 𝐵 ) )
11		fvex	⊢ ( ℵ ‘ 𝐵 ) ∈ V
12		ssdomg	⊢ ( ( ℵ ‘ 𝐵 ) ∈ V → ( ω ⊆ ( ℵ ‘ 𝐵 ) → ω ≼ ( ℵ ‘ 𝐵 ) ) )
13	11 12	ax-mp	⊢ ( ω ⊆ ( ℵ ‘ 𝐵 ) → ω ≼ ( ℵ ‘ 𝐵 ) )
14		infn0	⊢ ( ω ≼ ( ℵ ‘ 𝐵 ) → ( ℵ ‘ 𝐵 ) ≠ ∅ )
15	13 14	syl	⊢ ( ω ⊆ ( ℵ ‘ 𝐵 ) → ( ℵ ‘ 𝐵 ) ≠ ∅ )
16	10 15	sylbi	⊢ ( 𝐵 ∈ On → ( ℵ ‘ 𝐵 ) ≠ ∅ )
17		alephon	⊢ ( ℵ ‘ 𝐵 ) ∈ On
18		onenon	⊢ ( ( ℵ ‘ 𝐵 ) ∈ On → ( ℵ ‘ 𝐵 ) ∈ dom card )
19	17 18	ax-mp	⊢ ( ℵ ‘ 𝐵 ) ∈ dom card
20	16 19	jctil	⊢ ( 𝐵 ∈ On → ( ( ℵ ‘ 𝐵 ) ∈ dom card ∧ ( ℵ ‘ 𝐵 ) ≠ ∅ ) )
21		infxp	⊢ ( ( ( ( ℵ ‘ 𝐴 ) ∈ dom card ∧ ω ≼ ( ℵ ‘ 𝐴 ) ) ∧ ( ( ℵ ‘ 𝐵 ) ∈ dom card ∧ ( ℵ ‘ 𝐵 ) ≠ ∅ ) ) → ( ( ℵ ‘ 𝐴 ) × ( ℵ ‘ 𝐵 ) ) ≈ ( ( ℵ ‘ 𝐴 ) ∪ ( ℵ ‘ 𝐵 ) ) )
22	9 20 21	syl2an	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( ℵ ‘ 𝐴 ) × ( ℵ ‘ 𝐵 ) ) ≈ ( ( ℵ ‘ 𝐴 ) ∪ ( ℵ ‘ 𝐵 ) ) )