Description: Absorption law for addition to an infinite cardinal. (Contributed by NM, 30-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | infdjuabs | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp3 | |
|
2 | reldom | |
|
3 | 2 | brrelex2i | |
4 | djudom2 | |
|
5 | 1 3 4 | syl2anc2 | |
6 | xp2dju | |
|
7 | 5 6 | breqtrrdi | |
8 | simp1 | |
|
9 | 2onn | |
|
10 | nnsdom | |
|
11 | sdomdom | |
|
12 | 9 10 11 | mp2b | |
13 | simp2 | |
|
14 | domtr | |
|
15 | 12 13 14 | sylancr | |
16 | xpdom1g | |
|
17 | 8 15 16 | syl2anc | |
18 | domtr | |
|
19 | 7 17 18 | syl2anc | |
20 | infxpidm2 | |
|
21 | 20 | 3adant3 | |
22 | domentr | |
|
23 | 19 21 22 | syl2anc | |
24 | 2 | brrelex1i | |
25 | 24 | 3ad2ant3 | |
26 | djudoml | |
|
27 | 8 25 26 | syl2anc | |
28 | sbth | |
|
29 | 23 27 28 | syl2anc | |