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 ⊢ ℵ ⁡ A ⊔︀ ℵ ⁡ B ≈ ℵ ⁡ A ∪ ℵ ⁡ B

Proof

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