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

Metamath Proof Explorer

Theorem djucomen

Description: Commutative law for cardinal addition. Exercise 4.56(c) of Mendelson p. 258. (Contributed by NM, 24-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion djucomen ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( 𝐵 ⊔ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 1oex ⊢ 1o ∈ V
2 xpsnen2g ⊢ ( ( 1o ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( { 1o } × 𝐴 ) ≈ 𝐴 )
3 1 2 mpan ⊢ ( 𝐴 ∈ 𝑉 → ( { 1o } × 𝐴 ) ≈ 𝐴 )
4 0ex ⊢ ∅ ∈ V
5 xpsnen2g ⊢ ( ( ∅ ∈ V ∧ 𝐵 ∈ 𝑊 ) → ( { ∅ } × 𝐵 ) ≈ 𝐵 )
6 4 5 mpan ⊢ ( 𝐵 ∈ 𝑊 → ( { ∅ } × 𝐵 ) ≈ 𝐵 )
7 ensym ⊢ ( ( { 1o } × 𝐴 ) ≈ 𝐴 → 𝐴 ≈ ( { 1o } × 𝐴 ) )
8 ensym ⊢ ( ( { ∅ } × 𝐵 ) ≈ 𝐵 → 𝐵 ≈ ( { ∅ } × 𝐵 ) )
9 incom ⊢ ( ( { 1o } × 𝐴 ) ∩ ( { ∅ } × 𝐵 ) ) = ( ( { ∅ } × 𝐵 ) ∩ ( { 1o } × 𝐴 ) )
10 xp01disjl ⊢ ( ( { ∅ } × 𝐵 ) ∩ ( { 1o } × 𝐴 ) ) = ∅
11 9 10 eqtri ⊢ ( ( { 1o } × 𝐴 ) ∩ ( { ∅ } × 𝐵 ) ) = ∅
12 djuenun ⊢ ( ( 𝐴 ≈ ( { 1o } × 𝐴 ) ∧ 𝐵 ≈ ( { ∅ } × 𝐵 ) ∧ ( ( { 1o } × 𝐴 ) ∩ ( { ∅ } × 𝐵 ) ) = ∅ ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( ( { 1o } × 𝐴 ) ∪ ( { ∅ } × 𝐵 ) ) )
13 11 12 mp3an3 ⊢ ( ( 𝐴 ≈ ( { 1o } × 𝐴 ) ∧ 𝐵 ≈ ( { ∅ } × 𝐵 ) ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( ( { 1o } × 𝐴 ) ∪ ( { ∅ } × 𝐵 ) ) )
14 7 8 13 syl2an ⊢ ( ( ( { 1o } × 𝐴 ) ≈ 𝐴 ∧ ( { ∅ } × 𝐵 ) ≈ 𝐵 ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( ( { 1o } × 𝐴 ) ∪ ( { ∅ } × 𝐵 ) ) )
15 3 6 14 syl2an ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( ( { 1o } × 𝐴 ) ∪ ( { ∅ } × 𝐵 ) ) )
16 df-dju ⊢ ( 𝐵 ⊔ 𝐴 ) = ( ( { ∅ } × 𝐵 ) ∪ ( { 1o } × 𝐴 ) )
17 16 equncomi ⊢ ( 𝐵 ⊔ 𝐴 ) = ( ( { 1o } × 𝐴 ) ∪ ( { ∅ } × 𝐵 ) )
18 15 17 breqtrrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( 𝐵 ⊔ 𝐴 ) )