Description: Cardinal addition dominates union. (Contributed by NM, 28-Sep-2004) (Revised by Jim Kingdon, 15-Aug-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | undjudom | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0ex | |
|
2 | xpsnen2g | |
|
3 | 1 2 | mpan | |
4 | ensym | |
|
5 | endom | |
|
6 | 3 4 5 | 3syl | |
7 | 1on | |
|
8 | xpsnen2g | |
|
9 | 7 8 | mpan | |
10 | ensym | |
|
11 | endom | |
|
12 | 9 10 11 | 3syl | |
13 | xp01disjl | |
|
14 | undom | |
|
15 | 13 14 | mpan2 | |
16 | 6 12 15 | syl2an | |
17 | df-dju | |
|
18 | 16 17 | breqtrrdi | |