Metamath Proof Explorer


Theorem djuen

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 ABCDA⊔︀CB⊔︀D

Proof

Step Hyp Ref Expression
1 0ex V
2 relen Rel
3 2 brrelex1i ABAV
4 xpsnen2g VAV×AA
5 1 3 4 sylancr AB×AA
6 2 brrelex2i ABBV
7 xpsnen2g VBV×BB
8 1 6 7 sylancr AB×BB
9 8 ensymd ABB×B
10 entr ABB×BA×B
11 9 10 mpdan ABA×B
12 entr ×AAA×B×A×B
13 5 11 12 syl2anc AB×A×B
14 1on 1𝑜On
15 2 brrelex1i CDCV
16 xpsnen2g 1𝑜OnCV1𝑜×CC
17 14 15 16 sylancr CD1𝑜×CC
18 2 brrelex2i CDDV
19 xpsnen2g 1𝑜OnDV1𝑜×DD
20 14 18 19 sylancr CD1𝑜×DD
21 20 ensymd CDD1𝑜×D
22 entr CDD1𝑜×DC1𝑜×D
23 21 22 mpdan CDC1𝑜×D
24 entr 1𝑜×CCC1𝑜×D1𝑜×C1𝑜×D
25 17 23 24 syl2anc CD1𝑜×C1𝑜×D
26 xp01disjl ×A1𝑜×C=
27 xp01disjl ×B1𝑜×D=
28 unen ×A×B1𝑜×C1𝑜×D×A1𝑜×C=×B1𝑜×D=×A1𝑜×C×B1𝑜×D
29 26 27 28 mpanr12 ×A×B1𝑜×C1𝑜×D×A1𝑜×C×B1𝑜×D
30 13 25 29 syl2an ABCD×A1𝑜×C×B1𝑜×D
31 df-dju A⊔︀C=×A1𝑜×C
32 df-dju B⊔︀D=×B1𝑜×D
33 30 31 32 3brtr4g ABCDA⊔︀CB⊔︀D