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 ) )