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 ⊢ℵFnOn
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