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 
|- ( ( A ~~ B /\ C ~~ D ) -> ( A |_| C ) ~~ ( B |_| D ) )

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 relen 
 |-  Rel ~~
3 2 brrelex1i 
 |-  ( A ~~ B -> A e. _V )
4 xpsnen2g 
 |-  ( ( (/) e. _V /\ A e. _V ) -> ( { (/) } X. A ) ~~ A )
5 1 3 4 sylancr 
 |-  ( A ~~ B -> ( { (/) } X. A ) ~~ A )
6 2 brrelex2i 
 |-  ( A ~~ B -> B e. _V )
7 xpsnen2g 
 |-  ( ( (/) e. _V /\ B e. _V ) -> ( { (/) } X. B ) ~~ B )
8 1 6 7 sylancr 
 |-  ( A ~~ B -> ( { (/) } X. B ) ~~ B )
9 8 ensymd 
 |-  ( A ~~ B -> B ~~ ( { (/) } X. B ) )
10 entr 
 |-  ( ( A ~~ B /\ B ~~ ( { (/) } X. B ) ) -> A ~~ ( { (/) } X. B ) )
11 9 10 mpdan 
 |-  ( A ~~ B -> A ~~ ( { (/) } X. B ) )
12 entr 
 |-  ( ( ( { (/) } X. A ) ~~ A /\ A ~~ ( { (/) } X. B ) ) -> ( { (/) } X. A ) ~~ ( { (/) } X. B ) )
13 5 11 12 syl2anc 
 |-  ( A ~~ B -> ( { (/) } X. A ) ~~ ( { (/) } X. B ) )
14 1on 
 |-  1o e. On
15 2 brrelex1i 
 |-  ( C ~~ D -> C e. _V )
16 xpsnen2g 
 |-  ( ( 1o e. On /\ C e. _V ) -> ( { 1o } X. C ) ~~ C )
17 14 15 16 sylancr 
 |-  ( C ~~ D -> ( { 1o } X. C ) ~~ C )
18 2 brrelex2i 
 |-  ( C ~~ D -> D e. _V )
19 xpsnen2g 
 |-  ( ( 1o e. On /\ D e. _V ) -> ( { 1o } X. D ) ~~ D )
20 14 18 19 sylancr 
 |-  ( C ~~ D -> ( { 1o } X. D ) ~~ D )
21 20 ensymd 
 |-  ( C ~~ D -> D ~~ ( { 1o } X. D ) )
22 entr 
 |-  ( ( C ~~ D /\ D ~~ ( { 1o } X. D ) ) -> C ~~ ( { 1o } X. D ) )
23 21 22 mpdan 
 |-  ( C ~~ D -> C ~~ ( { 1o } X. D ) )
24 entr 
 |-  ( ( ( { 1o } X. C ) ~~ C /\ C ~~ ( { 1o } X. D ) ) -> ( { 1o } X. C ) ~~ ( { 1o } X. D ) )
25 17 23 24 syl2anc 
 |-  ( C ~~ D -> ( { 1o } X. C ) ~~ ( { 1o } X. D ) )
26 xp01disjl 
 |-  ( ( { (/) } X. A ) i^i ( { 1o } X. C ) ) = (/)
27 xp01disjl 
 |-  ( ( { (/) } X. B ) i^i ( { 1o } X. D ) ) = (/)
28 unen 
 |-  ( ( ( ( { (/) } X. A ) ~~ ( { (/) } X. B ) /\ ( { 1o } X. C ) ~~ ( { 1o } X. D ) ) /\ ( ( ( { (/) } X. A ) i^i ( { 1o } X. C ) ) = (/) /\ ( ( { (/) } X. B ) i^i ( { 1o } X. D ) ) = (/) ) ) -> ( ( { (/) } X. A ) u. ( { 1o } X. C ) ) ~~ ( ( { (/) } X. B ) u. ( { 1o } X. D ) ) )
29 26 27 28 mpanr12 
 |-  ( ( ( { (/) } X. A ) ~~ ( { (/) } X. B ) /\ ( { 1o } X. C ) ~~ ( { 1o } X. D ) ) -> ( ( { (/) } X. A ) u. ( { 1o } X. C ) ) ~~ ( ( { (/) } X. B ) u. ( { 1o } X. D ) ) )
30 13 25 29 syl2an 
 |-  ( ( A ~~ B /\ C ~~ D ) -> ( ( { (/) } X. A ) u. ( { 1o } X. C ) ) ~~ ( ( { (/) } X. B ) u. ( { 1o } X. D ) ) )
31 df-dju 
 |-  ( A |_| C ) = ( ( { (/) } X. A ) u. ( { 1o } X. C ) )
32 df-dju 
 |-  ( B |_| D ) = ( ( { (/) } X. B ) u. ( { 1o } X. D ) )
33 30 31 32 3brtr4g 
 |-  ( ( A ~~ B /\ C ~~ D ) -> ( A |_| C ) ~~ ( B |_| D ) )