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

Metamath Proof Explorer

Theorem endjudisj

Description: Equinumerosity of a disjoint union and a union of two disjoint sets. (Contributed by NM, 5-Apr-2007)

Ref Expression
Assertion endjudisj ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( 𝐴 ∪ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 df-dju ⊢ ( 𝐴 ⊔ 𝐵 ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) )
2 0ex ⊢ ∅ ∈ V
3 xpsnen2g ⊢ ( ( ∅ ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( { ∅ } × 𝐴 ) ≈ 𝐴 )
4 2 3 mpan ⊢ ( 𝐴 ∈ 𝑉 → ( { ∅ } × 𝐴 ) ≈ 𝐴 )
5 1on ⊢ 1o ∈ On
6 xpsnen2g ⊢ ( ( 1o ∈ On ∧ 𝐵 ∈ 𝑊 ) → ( { 1o } × 𝐵 ) ≈ 𝐵 )
7 5 6 mpan ⊢ ( 𝐵 ∈ 𝑊 → ( { 1o } × 𝐵 ) ≈ 𝐵 )
8 4 7 anim12i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( { ∅ } × 𝐴 ) ≈ 𝐴 ∧ ( { 1o } × 𝐵 ) ≈ 𝐵 ) )
9 xp01disjl ⊢ ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × 𝐵 ) ) = ∅
10 9 jctl ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × 𝐵 ) ) = ∅ ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) )
11 unen ⊢ ( ( ( ( { ∅ } × 𝐴 ) ≈ 𝐴 ∧ ( { 1o } × 𝐵 ) ≈ 𝐵 ) ∧ ( ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × 𝐵 ) ) = ∅ ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ) → ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) ) ≈ ( 𝐴 ∪ 𝐵 ) )
12 8 10 11 syl2an ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) ) ≈ ( 𝐴 ∪ 𝐵 ) )
13 12 3impa ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) ) ≈ ( 𝐴 ∪ 𝐵 ) )
14 1 13 eqbrtrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( 𝐴 ∪ 𝐵 ) )