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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unnum | |
|
2 | 1 | 3adant3 | |
3 | ssun2 | |
|
4 | ssdomg | |
|
5 | 2 3 4 | mpisyl | |
6 | simp1 | |
|
7 | djudom2 | |
|
8 | 5 6 7 | syl2anc | |
9 | djucomen | |
|
10 | 6 2 9 | syl2anc | |
11 | domentr | |
|
12 | 8 10 11 | syl2anc | |
13 | simp3 | |
|
14 | ssun1 | |
|
15 | ssdomg | |
|
16 | 2 14 15 | mpisyl | |
17 | domtr | |
|
18 | 13 16 17 | syl2anc | |
19 | infdjuabs | |
|
20 | 2 18 16 19 | syl3anc | |
21 | domentr | |
|
22 | 12 20 21 | syl2anc | |
23 | undjudom | |
|
24 | 23 | 3adant3 | |
25 | sbth | |
|
26 | 22 24 25 | syl2anc | |