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 ⊢ A ∈ V ∧ B ∈ W → A ⊔︀ B ≈ B ⊔︀ A

Proof

Step Hyp Ref Expression
1 1oex ⊢ 1 𝑜 ∈ V
2 xpsnen2g ⊢ 1 𝑜 ∈ V ∧ A ∈ V → 1 𝑜 × A ≈ A
3 1 2 mpan ⊢ A ∈ V → 1 𝑜 × A ≈ A
4 0ex ⊢ ∅ ∈ V
5 xpsnen2g ⊢ ∅ ∈ V ∧ B ∈ W → ∅ × B ≈ B
6 4 5 mpan ⊢ B ∈ W → ∅ × B ≈ B
7 ensym ⊢ 1 𝑜 × A ≈ A → A ≈ 1 𝑜 × A
8 ensym ⊢ ∅ × B ≈ B → B ≈ ∅ × B
9 incom ⊢ 1 𝑜 × A ∩ ∅ × B = ∅ × B ∩ 1 𝑜 × A
10 xp01disjl ⊢ ∅ × B ∩ 1 𝑜 × A = ∅
11 9 10 eqtri ⊢ 1 𝑜 × A ∩ ∅ × B = ∅
12 djuenun ⊢ A ≈ 1 𝑜 × A ∧ B ≈ ∅ × B ∧ 1 𝑜 × A ∩ ∅ × B = ∅ → A ⊔︀ B ≈ 1 𝑜 × A ∪ ∅ × B
13 11 12 mp3an3 ⊢ A ≈ 1 𝑜 × A ∧ B ≈ ∅ × B → A ⊔︀ B ≈ 1 𝑜 × A ∪ ∅ × B
14 7 8 13 syl2an ⊢ 1 𝑜 × A ≈ A ∧ ∅ × B ≈ B → A ⊔︀ B ≈ 1 𝑜 × A ∪ ∅ × B
15 3 6 14 syl2an ⊢ A ∈ V ∧ B ∈ W → A ⊔︀ B ≈ 1 𝑜 × A ∪ ∅ × B
16 df-dju ⊢ B ⊔︀ A = ∅ × B ∪ 1 𝑜 × A
17 16 equncomi ⊢ B ⊔︀ A = 1 𝑜 × A ∪ ∅ × B
18 15 17 breqtrrdi ⊢ A ∈ V ∧ B ∈ W → A ⊔︀ B ≈ B ⊔︀ A