Metamath Proof Explorer

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 ⊢ A ∈ On ∧ B ∈ On → ℵ ⁡ A × ℵ ⁡ B ≈ ℵ ⁡ A ∪ ℵ ⁡ B

Proof

Step Hyp Ref Expression
1 alephgeom ⊢ A ∈ On ↔ ω ⊆ ℵ ⁡ A
2 fvex ⊢ ℵ ⁡ A ∈ V
3 ssdomg ⊢ ℵ ⁡ A ∈ V → ω ⊆ ℵ ⁡ A → ω ≼ ℵ ⁡ A
4 2 3 ax-mp ⊢ ω ⊆ ℵ ⁡ A → ω ≼ ℵ ⁡ A
5 1 4 sylbi ⊢ A ∈ On → ω ≼ ℵ ⁡ A
6 alephon ⊢ ℵ ⁡ A ∈ On
7 onenon ⊢ ℵ ⁡ A ∈ On → ℵ ⁡ A ∈ dom ⁡ card
8 6 7 ax-mp ⊢ ℵ ⁡ A ∈ dom ⁡ card
9 5 8 jctil ⊢ A ∈ On → ℵ ⁡ A ∈ dom ⁡ card ∧ ω ≼ ℵ ⁡ A
10 alephgeom ⊢ B ∈ On ↔ ω ⊆ ℵ ⁡ B
11 fvex ⊢ ℵ ⁡ B ∈ V
12 ssdomg ⊢ ℵ ⁡ B ∈ V → ω ⊆ ℵ ⁡ B → ω ≼ ℵ ⁡ B
13 11 12 ax-mp ⊢ ω ⊆ ℵ ⁡ B → ω ≼ ℵ ⁡ B
14 infn0 ⊢ ω ≼ ℵ ⁡ B → ℵ ⁡ B ≠ ∅
15 13 14 syl ⊢ ω ⊆ ℵ ⁡ B → ℵ ⁡ B ≠ ∅
16 10 15 sylbi ⊢ B ∈ On → ℵ ⁡ B ≠ ∅
17 alephon ⊢ ℵ ⁡ B ∈ On
18 onenon ⊢ ℵ ⁡ B ∈ On → ℵ ⁡ B ∈ dom ⁡ card
19 17 18 ax-mp ⊢ ℵ ⁡ B ∈ dom ⁡ card
20 16 19 jctil ⊢ B ∈ On → ℵ ⁡ B ∈ dom ⁡ card ∧ ℵ ⁡ B ≠ ∅
21 infxp ⊢ ℵ ⁡ A ∈ dom ⁡ card ∧ ω ≼ ℵ ⁡ A ∧ ℵ ⁡ B ∈ dom ⁡ card ∧ ℵ ⁡ B ≠ ∅ → ℵ ⁡ A × ℵ ⁡ B ≈ ℵ ⁡ A ∪ ℵ ⁡ B
22 9 20 21 syl2an ⊢ A ∈ On ∧ B ∈ On → ℵ ⁡ A × ℵ ⁡ B ≈ ℵ ⁡ A ∪ ℵ ⁡ B