Theorem addccom 4406

Description: Cardinal sum commutes. Theorem X.1.9 of [Rosser] p. 276. (Contributed by SF, 15-Jan-2015.)

Assertion

Ref	Expression
addccom	⊢ (A +c B) = (B +c A)

Proof of Theorem addccom

Dummy variables x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		incom 3448	. . . . . . 7 ⊢ (y ∩ z) = (z ∩ y)
2	1	eqeq1i 2360	. . . . . 6 ⊢ ((y ∩ z) = ∅ ↔ (z ∩ y) = ∅)
3		uncom 3408	. . . . . . 7 ⊢ (y ∪ z) = (z ∪ y)
4	3	eqeq2i 2363	. . . . . 6 ⊢ (x = (y ∪ z) ↔ x = (z ∪ y))
5	2, 4	anbi12i 678	. . . . 5 ⊢ (((y ∩ z) = ∅ ∧ x = (y ∪ z)) ↔ ((z ∩ y) = ∅ ∧ x = (z ∪ y)))
6	5	2rexbii 2641	. . . 4 ⊢ (∃y ∈ A ∃z ∈ B ((y ∩ z) = ∅ ∧ x = (y ∪ z)) ↔ ∃y ∈ A ∃z ∈ B ((z ∩ y) = ∅ ∧ x = (z ∪ y)))
7		rexcom 2772	. . . 4 ⊢ (∃y ∈ A ∃z ∈ B ((z ∩ y) = ∅ ∧ x = (z ∪ y)) ↔ ∃z ∈ B ∃y ∈ A ((z ∩ y) = ∅ ∧ x = (z ∪ y)))
8	6, 7	bitri 240	. . 3 ⊢ (∃y ∈ A ∃z ∈ B ((y ∩ z) = ∅ ∧ x = (y ∪ z)) ↔ ∃z ∈ B ∃y ∈ A ((z ∩ y) = ∅ ∧ x = (z ∪ y)))
9	8	abbii 2465	. 2 ⊢ {x ∣ ∃y ∈ A ∃z ∈ B ((y ∩ z) = ∅ ∧ x = (y ∪ z))} = {x ∣ ∃z ∈ B ∃y ∈ A ((z ∩ y) = ∅ ∧ x = (z ∪ y))}
10		df-addc 4378	. 2 ⊢ (A +c B) = {x ∣ ∃y ∈ A ∃z ∈ B ((y ∩ z) = ∅ ∧ x = (y ∪ z))}
11		df-addc 4378	. 2 ⊢ (B +c A) = {x ∣ ∃z ∈ B ∃y ∈ A ((z ∩ y) = ∅ ∧ x = (z ∪ y))}
12	9, 10, 11	3eqtr4i 2383	1 ⊢ (A +c B) = (B +c A)

Syntax hints:   ∧ wa 358   = wceq 1642  {cab 2339  ∃wrex 2615   ∪ cun 3207   ∩ cin 3208  ∅c0 3550   +_c cplc 4375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-rex 2620  df-v 2861  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-addc 4378

This theorem is referenced by:  addcid2  4407  1cnnc  4408  addc32  4416  nncaddccl  4419  addcnnul  4453  ltfintr  4459  tfinltfinlem1  4500  oddtfin  4518  addccan1  4560  leaddc2  6215  nc0suc  6217  nmembers1lem3  6270  nchoicelem1  6289  nchoicelem7  6295  nchoicelem14  6302  nchoicelem17  6305