Metamath Proof Explorer


Theorem djuenun

Description: Disjoint union is equinumerous to union for disjoint sets. (Contributed by Mario Carneiro, 29-Apr-2015) (Revised by Jim Kingdon, 19-Aug-2023)

Ref Expression
Assertion djuenun
|- ( ( A ~~ B /\ C ~~ D /\ ( B i^i D ) = (/) ) -> ( A |_| C ) ~~ ( B u. D ) )

Proof

Step Hyp Ref Expression
1 djuen
 |-  ( ( A ~~ B /\ C ~~ D ) -> ( A |_| C ) ~~ ( B |_| D ) )
2 1 3adant3
 |-  ( ( A ~~ B /\ C ~~ D /\ ( B i^i D ) = (/) ) -> ( A |_| C ) ~~ ( B |_| D ) )
3 relen
 |-  Rel ~~
4 3 brrelex2i
 |-  ( A ~~ B -> B e. _V )
5 3 brrelex2i
 |-  ( C ~~ D -> D e. _V )
6 id
 |-  ( ( B i^i D ) = (/) -> ( B i^i D ) = (/) )
7 endjudisj
 |-  ( ( B e. _V /\ D e. _V /\ ( B i^i D ) = (/) ) -> ( B |_| D ) ~~ ( B u. D ) )
8 4 5 6 7 syl3an
 |-  ( ( A ~~ B /\ C ~~ D /\ ( B i^i D ) = (/) ) -> ( B |_| D ) ~~ ( B u. D ) )
9 entr
 |-  ( ( ( A |_| C ) ~~ ( B |_| D ) /\ ( B |_| D ) ~~ ( B u. D ) ) -> ( A |_| C ) ~~ ( B u. D ) )
10 2 8 9 syl2anc
 |-  ( ( A ~~ B /\ C ~~ D /\ ( B i^i D ) = (/) ) -> ( A |_| C ) ~~ ( B u. D ) )