This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

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