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	⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ) → ( 𝐴 ⊔ 𝐶 ) ≈ ( 𝐵 ⊔ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2		relen	⊢ Rel ≈
3	2	brrelex1i	⊢ ( 𝐴 ≈ 𝐵 → 𝐴 ∈ V )
4		xpsnen2g	⊢ ( ( ∅ ∈ V ∧ 𝐴 ∈ V ) → ( { ∅ } × 𝐴 ) ≈ 𝐴 )
5	1 3 4	sylancr	⊢ ( 𝐴 ≈ 𝐵 → ( { ∅ } × 𝐴 ) ≈ 𝐴 )
6	2	brrelex2i	⊢ ( 𝐴 ≈ 𝐵 → 𝐵 ∈ V )
7		xpsnen2g	⊢ ( ( ∅ ∈ V ∧ 𝐵 ∈ V ) → ( { ∅ } × 𝐵 ) ≈ 𝐵 )
8	1 6 7	sylancr	⊢ ( 𝐴 ≈ 𝐵 → ( { ∅ } × 𝐵 ) ≈ 𝐵 )
9	8	ensymd	⊢ ( 𝐴 ≈ 𝐵 → 𝐵 ≈ ( { ∅ } × 𝐵 ) )
10		entr	⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ≈ ( { ∅ } × 𝐵 ) ) → 𝐴 ≈ ( { ∅ } × 𝐵 ) )
11	9 10	mpdan	⊢ ( 𝐴 ≈ 𝐵 → 𝐴 ≈ ( { ∅ } × 𝐵 ) )
12		entr	⊢ ( ( ( { ∅ } × 𝐴 ) ≈ 𝐴 ∧ 𝐴 ≈ ( { ∅ } × 𝐵 ) ) → ( { ∅ } × 𝐴 ) ≈ ( { ∅ } × 𝐵 ) )
13	5 11 12	syl2anc	⊢ ( 𝐴 ≈ 𝐵 → ( { ∅ } × 𝐴 ) ≈ ( { ∅ } × 𝐵 ) )
14		1on	⊢ 1o ∈ On
15	2	brrelex1i	⊢ ( 𝐶 ≈ 𝐷 → 𝐶 ∈ V )
16		xpsnen2g	⊢ ( ( 1o ∈ On ∧ 𝐶 ∈ V ) → ( { 1o } × 𝐶 ) ≈ 𝐶 )
17	14 15 16	sylancr	⊢ ( 𝐶 ≈ 𝐷 → ( { 1o } × 𝐶 ) ≈ 𝐶 )
18	2	brrelex2i	⊢ ( 𝐶 ≈ 𝐷 → 𝐷 ∈ V )
19		xpsnen2g	⊢ ( ( 1o ∈ On ∧ 𝐷 ∈ V ) → ( { 1o } × 𝐷 ) ≈ 𝐷 )
20	14 18 19	sylancr	⊢ ( 𝐶 ≈ 𝐷 → ( { 1o } × 𝐷 ) ≈ 𝐷 )
21	20	ensymd	⊢ ( 𝐶 ≈ 𝐷 → 𝐷 ≈ ( { 1o } × 𝐷 ) )
22		entr	⊢ ( ( 𝐶 ≈ 𝐷 ∧ 𝐷 ≈ ( { 1o } × 𝐷 ) ) → 𝐶 ≈ ( { 1o } × 𝐷 ) )
23	21 22	mpdan	⊢ ( 𝐶 ≈ 𝐷 → 𝐶 ≈ ( { 1o } × 𝐷 ) )
24		entr	⊢ ( ( ( { 1o } × 𝐶 ) ≈ 𝐶 ∧ 𝐶 ≈ ( { 1o } × 𝐷 ) ) → ( { 1o } × 𝐶 ) ≈ ( { 1o } × 𝐷 ) )
25	17 23 24	syl2anc	⊢ ( 𝐶 ≈ 𝐷 → ( { 1o } × 𝐶 ) ≈ ( { 1o } × 𝐷 ) )
26		xp01disjl	⊢ ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × 𝐶 ) ) = ∅
27		xp01disjl	⊢ ( ( { ∅ } × 𝐵 ) ∩ ( { 1o } × 𝐷 ) ) = ∅
28		unen	⊢ ( ( ( ( { ∅ } × 𝐴 ) ≈ ( { ∅ } × 𝐵 ) ∧ ( { 1o } × 𝐶 ) ≈ ( { 1o } × 𝐷 ) ) ∧ ( ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × 𝐶 ) ) = ∅ ∧ ( ( { ∅ } × 𝐵 ) ∩ ( { 1o } × 𝐷 ) ) = ∅ ) ) → ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐶 ) ) ≈ ( ( { ∅ } × 𝐵 ) ∪ ( { 1o } × 𝐷 ) ) )
29	26 27 28	mpanr12	⊢ ( ( ( { ∅ } × 𝐴 ) ≈ ( { ∅ } × 𝐵 ) ∧ ( { 1o } × 𝐶 ) ≈ ( { 1o } × 𝐷 ) ) → ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐶 ) ) ≈ ( ( { ∅ } × 𝐵 ) ∪ ( { 1o } × 𝐷 ) ) )
30	13 25 29	syl2an	⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ) → ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐶 ) ) ≈ ( ( { ∅ } × 𝐵 ) ∪ ( { 1o } × 𝐷 ) ) )
31		df-dju	⊢ ( 𝐴 ⊔ 𝐶 ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐶 ) )
32		df-dju	⊢ ( 𝐵 ⊔ 𝐷 ) = ( ( { ∅ } × 𝐵 ) ∪ ( { 1o } × 𝐷 ) )
33	30 31 32	3brtr4g	⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ) → ( 𝐴 ⊔ 𝐶 ) ≈ ( 𝐵 ⊔ 𝐷 ) )