Metamath Proof Explorer

Theorem alephadd

Description: The sum 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 alephadd ( ( ℵ ‘ 𝐴 ) ⊔ ( ℵ ‘ 𝐵 ) ) ≈ ( ( ℵ ‘ 𝐴 ) ∪ ( ℵ ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fvex ⊢ ( ℵ ‘ 𝐴 ) ∈ V
2 fvex ⊢ ( ℵ ‘ 𝐵 ) ∈ V
3 djuex ⊢ ( ( ( ℵ ‘ 𝐴 ) ∈ V ∧ ( ℵ ‘ 𝐵 ) ∈ V ) → ( ( ℵ ‘ 𝐴 ) ⊔ ( ℵ ‘ 𝐵 ) ) ∈ V )
4 1 2 3 mp2an ⊢ ( ( ℵ ‘ 𝐴 ) ⊔ ( ℵ ‘ 𝐵 ) ) ∈ V
5 alephfnon ⊢ ℵ Fn On
6 5 fndmi ⊢ dom ℵ = On
7 6 eleq2i ⊢ ( 𝐴 ∈ dom ℵ ↔ 𝐴 ∈ On )
8 7 notbii ⊢ ( ¬ 𝐴 ∈ dom ℵ ↔ ¬ 𝐴 ∈ On )
9 6 eleq2i ⊢ ( 𝐵 ∈ dom ℵ ↔ 𝐵 ∈ On )
10 9 notbii ⊢ ( ¬ 𝐵 ∈ dom ℵ ↔ ¬ 𝐵 ∈ On )
11 df-dju ⊢ ( ∅ ⊔ ∅ ) = ( ( { ∅ } × ∅ ) ∪ ( { 1o } × ∅ ) )
12 xpundir ⊢ ( ( { ∅ } ∪ { 1o } ) × ∅ ) = ( ( { ∅ } × ∅ ) ∪ ( { 1o } × ∅ ) )
13 xp0 ⊢ ( ( { ∅ } ∪ { 1o } ) × ∅ ) = ∅
14 11 12 13 3eqtr2i ⊢ ( ∅ ⊔ ∅ ) = ∅
15 ndmfv ⊢ ( ¬ 𝐴 ∈ dom ℵ → ( ℵ ‘ 𝐴 ) = ∅ )
16 ndmfv ⊢ ( ¬ 𝐵 ∈ dom ℵ → ( ℵ ‘ 𝐵 ) = ∅ )
17 djueq12 ⊢ ( ( ( ℵ ‘ 𝐴 ) = ∅ ∧ ( ℵ ‘ 𝐵 ) = ∅ ) → ( ( ℵ ‘ 𝐴 ) ⊔ ( ℵ ‘ 𝐵 ) ) = ( ∅ ⊔ ∅ ) )
18 15 16 17 syl2an ⊢ ( ( ¬ 𝐴 ∈ dom ℵ ∧ ¬ 𝐵 ∈ dom ℵ ) → ( ( ℵ ‘ 𝐴 ) ⊔ ( ℵ ‘ 𝐵 ) ) = ( ∅ ⊔ ∅ ) )
19 15 adantr ⊢ ( ( ¬ 𝐴 ∈ dom ℵ ∧ ¬ 𝐵 ∈ dom ℵ ) → ( ℵ ‘ 𝐴 ) = ∅ )
20 16 adantl ⊢ ( ( ¬ 𝐴 ∈ dom ℵ ∧ ¬ 𝐵 ∈ dom ℵ ) → ( ℵ ‘ 𝐵 ) = ∅ )
21 19 20 uneq12d ⊢ ( ( ¬ 𝐴 ∈ dom ℵ ∧ ¬ 𝐵 ∈ dom ℵ ) → ( ( ℵ ‘ 𝐴 ) ∪ ( ℵ ‘ 𝐵 ) ) = ( ∅ ∪ ∅ ) )
22 un0 ⊢ ( ∅ ∪ ∅ ) = ∅
23 21 22 eqtrdi ⊢ ( ( ¬ 𝐴 ∈ dom ℵ ∧ ¬ 𝐵 ∈ dom ℵ ) → ( ( ℵ ‘ 𝐴 ) ∪ ( ℵ ‘ 𝐵 ) ) = ∅ )
24 14 18 23 3eqtr4a ⊢ ( ( ¬ 𝐴 ∈ dom ℵ ∧ ¬ 𝐵 ∈ dom ℵ ) → ( ( ℵ ‘ 𝐴 ) ⊔ ( ℵ ‘ 𝐵 ) ) = ( ( ℵ ‘ 𝐴 ) ∪ ( ℵ ‘ 𝐵 ) ) )
25 8 10 24 syl2anbr ⊢ ( ( ¬ 𝐴 ∈ On ∧ ¬ 𝐵 ∈ On ) → ( ( ℵ ‘ 𝐴 ) ⊔ ( ℵ ‘ 𝐵 ) ) = ( ( ℵ ‘ 𝐴 ) ∪ ( ℵ ‘ 𝐵 ) ) )
26 eqeng ⊢ ( ( ( ℵ ‘ 𝐴 ) ⊔ ( ℵ ‘ 𝐵 ) ) ∈ V → ( ( ( ℵ ‘ 𝐴 ) ⊔ ( ℵ ‘ 𝐵 ) ) = ( ( ℵ ‘ 𝐴 ) ∪ ( ℵ ‘ 𝐵 ) ) → ( ( ℵ ‘ 𝐴 ) ⊔ ( ℵ ‘ 𝐵 ) ) ≈ ( ( ℵ ‘ 𝐴 ) ∪ ( ℵ ‘ 𝐵 ) ) ) )
27 4 25 26 mpsyl ⊢ ( ( ¬ 𝐴 ∈ On ∧ ¬ 𝐵 ∈ On ) → ( ( ℵ ‘ 𝐴 ) ⊔ ( ℵ ‘ 𝐵 ) ) ≈ ( ( ℵ ‘ 𝐴 ) ∪ ( ℵ ‘ 𝐵 ) ) )
28 27 ex ⊢ ( ¬ 𝐴 ∈ On → ( ¬ 𝐵 ∈ On → ( ( ℵ ‘ 𝐴 ) ⊔ ( ℵ ‘ 𝐵 ) ) ≈ ( ( ℵ ‘ 𝐴 ) ∪ ( ℵ ‘ 𝐵 ) ) ) )
29 alephgeom ⊢ ( 𝐴 ∈ On ↔ ω ⊆ ( ℵ ‘ 𝐴 ) )
30 ssdomg ⊢ ( ( ℵ ‘ 𝐴 ) ∈ V → ( ω ⊆ ( ℵ ‘ 𝐴 ) → ω ≼ ( ℵ ‘ 𝐴 ) ) )
31 1 30 ax-mp ⊢ ( ω ⊆ ( ℵ ‘ 𝐴 ) → ω ≼ ( ℵ ‘ 𝐴 ) )
32 alephon ⊢ ( ℵ ‘ 𝐴 ) ∈ On
33 onenon ⊢ ( ( ℵ ‘ 𝐴 ) ∈ On → ( ℵ ‘ 𝐴 ) ∈ dom card )
34 32 33 ax-mp ⊢ ( ℵ ‘ 𝐴 ) ∈ dom card
35 alephon ⊢ ( ℵ ‘ 𝐵 ) ∈ On
36 onenon ⊢ ( ( ℵ ‘ 𝐵 ) ∈ On → ( ℵ ‘ 𝐵 ) ∈ dom card )
37 35 36 ax-mp ⊢ ( ℵ ‘ 𝐵 ) ∈ dom card
38 infdju ⊢ ( ( ( ℵ ‘ 𝐴 ) ∈ dom card ∧ ( ℵ ‘ 𝐵 ) ∈ dom card ∧ ω ≼ ( ℵ ‘ 𝐴 ) ) → ( ( ℵ ‘ 𝐴 ) ⊔ ( ℵ ‘ 𝐵 ) ) ≈ ( ( ℵ ‘ 𝐴 ) ∪ ( ℵ ‘ 𝐵 ) ) )
39 34 37 38 mp3an12 ⊢ ( ω ≼ ( ℵ ‘ 𝐴 ) → ( ( ℵ ‘ 𝐴 ) ⊔ ( ℵ ‘ 𝐵 ) ) ≈ ( ( ℵ ‘ 𝐴 ) ∪ ( ℵ ‘ 𝐵 ) ) )
40 31 39 syl ⊢ ( ω ⊆ ( ℵ ‘ 𝐴 ) → ( ( ℵ ‘ 𝐴 ) ⊔ ( ℵ ‘ 𝐵 ) ) ≈ ( ( ℵ ‘ 𝐴 ) ∪ ( ℵ ‘ 𝐵 ) ) )
41 29 40 sylbi ⊢ ( 𝐴 ∈ On → ( ( ℵ ‘ 𝐴 ) ⊔ ( ℵ ‘ 𝐵 ) ) ≈ ( ( ℵ ‘ 𝐴 ) ∪ ( ℵ ‘ 𝐵 ) ) )
42 alephgeom ⊢ ( 𝐵 ∈ On ↔ ω ⊆ ( ℵ ‘ 𝐵 ) )
43 ssdomg ⊢ ( ( ℵ ‘ 𝐵 ) ∈ V → ( ω ⊆ ( ℵ ‘ 𝐵 ) → ω ≼ ( ℵ ‘ 𝐵 ) ) )
44 2 43 ax-mp ⊢ ( ω ⊆ ( ℵ ‘ 𝐵 ) → ω ≼ ( ℵ ‘ 𝐵 ) )
45 djucomen ⊢ ( ( ( ℵ ‘ 𝐴 ) ∈ V ∧ ( ℵ ‘ 𝐵 ) ∈ V ) → ( ( ℵ ‘ 𝐴 ) ⊔ ( ℵ ‘ 𝐵 ) ) ≈ ( ( ℵ ‘ 𝐵 ) ⊔ ( ℵ ‘ 𝐴 ) ) )
46 1 2 45 mp2an ⊢ ( ( ℵ ‘ 𝐴 ) ⊔ ( ℵ ‘ 𝐵 ) ) ≈ ( ( ℵ ‘ 𝐵 ) ⊔ ( ℵ ‘ 𝐴 ) )
47 infdju ⊢ ( ( ( ℵ ‘ 𝐵 ) ∈ dom card ∧ ( ℵ ‘ 𝐴 ) ∈ dom card ∧ ω ≼ ( ℵ ‘ 𝐵 ) ) → ( ( ℵ ‘ 𝐵 ) ⊔ ( ℵ ‘ 𝐴 ) ) ≈ ( ( ℵ ‘ 𝐵 ) ∪ ( ℵ ‘ 𝐴 ) ) )
48 37 34 47 mp3an12 ⊢ ( ω ≼ ( ℵ ‘ 𝐵 ) → ( ( ℵ ‘ 𝐵 ) ⊔ ( ℵ ‘ 𝐴 ) ) ≈ ( ( ℵ ‘ 𝐵 ) ∪ ( ℵ ‘ 𝐴 ) ) )
49 entr ⊢ ( ( ( ( ℵ ‘ 𝐴 ) ⊔ ( ℵ ‘ 𝐵 ) ) ≈ ( ( ℵ ‘ 𝐵 ) ⊔ ( ℵ ‘ 𝐴 ) ) ∧ ( ( ℵ ‘ 𝐵 ) ⊔ ( ℵ ‘ 𝐴 ) ) ≈ ( ( ℵ ‘ 𝐵 ) ∪ ( ℵ ‘ 𝐴 ) ) ) → ( ( ℵ ‘ 𝐴 ) ⊔ ( ℵ ‘ 𝐵 ) ) ≈ ( ( ℵ ‘ 𝐵 ) ∪ ( ℵ ‘ 𝐴 ) ) )
50 46 48 49 sylancr ⊢ ( ω ≼ ( ℵ ‘ 𝐵 ) → ( ( ℵ ‘ 𝐴 ) ⊔ ( ℵ ‘ 𝐵 ) ) ≈ ( ( ℵ ‘ 𝐵 ) ∪ ( ℵ ‘ 𝐴 ) ) )
51 uncom ⊢ ( ( ℵ ‘ 𝐵 ) ∪ ( ℵ ‘ 𝐴 ) ) = ( ( ℵ ‘ 𝐴 ) ∪ ( ℵ ‘ 𝐵 ) )
52 50 51 breqtrdi ⊢ ( ω ≼ ( ℵ ‘ 𝐵 ) → ( ( ℵ ‘ 𝐴 ) ⊔ ( ℵ ‘ 𝐵 ) ) ≈ ( ( ℵ ‘ 𝐴 ) ∪ ( ℵ ‘ 𝐵 ) ) )
53 44 52 syl ⊢ ( ω ⊆ ( ℵ ‘ 𝐵 ) → ( ( ℵ ‘ 𝐴 ) ⊔ ( ℵ ‘ 𝐵 ) ) ≈ ( ( ℵ ‘ 𝐴 ) ∪ ( ℵ ‘ 𝐵 ) ) )
54 42 53 sylbi ⊢ ( 𝐵 ∈ On → ( ( ℵ ‘ 𝐴 ) ⊔ ( ℵ ‘ 𝐵 ) ) ≈ ( ( ℵ ‘ 𝐴 ) ∪ ( ℵ ‘ 𝐵 ) ) )
55 28 41 54 pm2.61ii ⊢ ( ( ℵ ‘ 𝐴 ) ⊔ ( ℵ ‘ 𝐵 ) ) ≈ ( ( ℵ ‘ 𝐴 ) ∪ ( ℵ ‘ 𝐵 ) )