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

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 ( ( 𝐴 ∈ 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 ) → ( ( ℵ ‘ 𝐴 ) × ( ℵ ‘ 𝐵 ) ) ≈ ( ( ℵ ‘ 𝐴 ) ∪ ( ℵ ‘ 𝐵 ) ) )