Metamath Proof Explorer


Theorem infdju

Description: The sum of two cardinal numbers is their maximum, if one of them is infinite. Proposition 10.41 of TakeutiZaring p. 95. (Contributed by NM, 28-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion infdju AdomcardBdomcardωAA⊔︀BAB

Proof

Step Hyp Ref Expression
1 unnum AdomcardBdomcardABdomcard
2 1 3adant3 AdomcardBdomcardωAABdomcard
3 ssun2 BAB
4 ssdomg ABdomcardBABBAB
5 2 3 4 mpisyl AdomcardBdomcardωABAB
6 simp1 AdomcardBdomcardωAAdomcard
7 djudom2 BABAdomcardA⊔︀BA⊔︀AB
8 5 6 7 syl2anc AdomcardBdomcardωAA⊔︀BA⊔︀AB
9 djucomen AdomcardABdomcardA⊔︀ABAB⊔︀A
10 6 2 9 syl2anc AdomcardBdomcardωAA⊔︀ABAB⊔︀A
11 domentr A⊔︀BA⊔︀ABA⊔︀ABAB⊔︀AA⊔︀BAB⊔︀A
12 8 10 11 syl2anc AdomcardBdomcardωAA⊔︀BAB⊔︀A
13 simp3 AdomcardBdomcardωAωA
14 ssun1 AAB
15 ssdomg ABdomcardAABAAB
16 2 14 15 mpisyl AdomcardBdomcardωAAAB
17 domtr ωAAABωAB
18 13 16 17 syl2anc AdomcardBdomcardωAωAB
19 infdjuabs ABdomcardωABAABAB⊔︀AAB
20 2 18 16 19 syl3anc AdomcardBdomcardωAAB⊔︀AAB
21 domentr A⊔︀BAB⊔︀AAB⊔︀AABA⊔︀BAB
22 12 20 21 syl2anc AdomcardBdomcardωAA⊔︀BAB
23 undjudom AdomcardBdomcardABA⊔︀B
24 23 3adant3 AdomcardBdomcardωAABA⊔︀B
25 sbth A⊔︀BABABA⊔︀BA⊔︀BAB
26 22 24 25 syl2anc AdomcardBdomcardωAA⊔︀BAB