Description: Disjoint unions of equinumerous sets are equinumerous. (Contributed by NM, 28-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | djuen | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0ex | |
|
2 | relen | |
|
3 | 2 | brrelex1i | |
4 | xpsnen2g | |
|
5 | 1 3 4 | sylancr | |
6 | 2 | brrelex2i | |
7 | xpsnen2g | |
|
8 | 1 6 7 | sylancr | |
9 | 8 | ensymd | |
10 | entr | |
|
11 | 9 10 | mpdan | |
12 | entr | |
|
13 | 5 11 12 | syl2anc | |
14 | 1on | |
|
15 | 2 | brrelex1i | |
16 | xpsnen2g | |
|
17 | 14 15 16 | sylancr | |
18 | 2 | brrelex2i | |
19 | xpsnen2g | |
|
20 | 14 18 19 | sylancr | |
21 | 20 | ensymd | |
22 | entr | |
|
23 | 21 22 | mpdan | |
24 | entr | |
|
25 | 17 23 24 | syl2anc | |
26 | xp01disjl | |
|
27 | xp01disjl | |
|
28 | unen | |
|
29 | 26 27 28 | mpanr12 | |
30 | 13 25 29 | syl2an | |
31 | df-dju | |
|
32 | df-dju | |
|
33 | 30 31 32 | 3brtr4g | |