New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  addcass GIF version

 Description: Cardinal addition is associative. Theorem X.1.11, corollary 1 of [Rosser] p. 277. (Contributed by SF, 17-Jan-2015.)
Assertion
Ref Expression
addcass ((A +c B) +c C) = (A +c (B +c C))

Dummy variables a b c d e x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ancom 437 . . . . . . . . . . 11 (((ac) = (bc) = ) ↔ ((bc) = (ac) = ))
21anbi2i 675 . . . . . . . . . 10 (((ab) = ((ac) = (bc) = )) ↔ ((ab) = ((bc) = (ac) = )))
3 an12 772 . . . . . . . . . 10 (((ab) = ((bc) = (ac) = )) ↔ ((bc) = ((ab) = (ac) = )))
42, 3bitri 240 . . . . . . . . 9 (((ab) = ((ac) = (bc) = )) ↔ ((bc) = ((ab) = (ac) = )))
5 indir 3503 . . . . . . . . . . . 12 ((ab) ∩ c) = ((ac) ∪ (bc))
65eqeq1i 2360 . . . . . . . . . . 11 (((ab) ∩ c) = ↔ ((ac) ∪ (bc)) = )
7 un00 3586 . . . . . . . . . . 11 (((ac) = (bc) = ) ↔ ((ac) ∪ (bc)) = )
86, 7bitr4i 243 . . . . . . . . . 10 (((ab) ∩ c) = ↔ ((ac) = (bc) = ))
98anbi2i 675 . . . . . . . . 9 (((ab) = ((ab) ∩ c) = ) ↔ ((ab) = ((ac) = (bc) = )))
10 indi 3501 . . . . . . . . . . . 12 (a ∩ (bc)) = ((ab) ∪ (ac))
1110eqeq1i 2360 . . . . . . . . . . 11 ((a ∩ (bc)) = ↔ ((ab) ∪ (ac)) = )
12 un00 3586 . . . . . . . . . . 11 (((ab) = (ac) = ) ↔ ((ab) ∪ (ac)) = )
1311, 12bitr4i 243 . . . . . . . . . 10 ((a ∩ (bc)) = ↔ ((ab) = (ac) = ))
1413anbi2i 675 . . . . . . . . 9 (((bc) = (a ∩ (bc)) = ) ↔ ((bc) = ((ab) = (ac) = )))
154, 9, 143bitr4i 268 . . . . . . . 8 (((ab) = ((ab) ∩ c) = ) ↔ ((bc) = (a ∩ (bc)) = ))
16 unass 3420 . . . . . . . . 9 ((ab) ∪ c) = (a ∪ (bc))
1716eqeq2i 2363 . . . . . . . 8 (x = ((ab) ∪ c) ↔ x = (a ∪ (bc)))
1815, 17anbi12i 678 . . . . . . 7 ((((ab) = ((ab) ∩ c) = ) x = ((ab) ∪ c)) ↔ (((bc) = (a ∩ (bc)) = ) x = (a ∪ (bc))))
19 anass 630 . . . . . . 7 ((((ab) = ((ab) ∩ c) = ) x = ((ab) ∪ c)) ↔ ((ab) = (((ab) ∩ c) = x = ((ab) ∪ c))))
20 anass 630 . . . . . . 7 ((((bc) = (a ∩ (bc)) = ) x = (a ∪ (bc))) ↔ ((bc) = ((a ∩ (bc)) = x = (a ∪ (bc)))))
2118, 19, 203bitr3i 266 . . . . . 6 (((ab) = (((ab) ∩ c) = x = ((ab) ∪ c))) ↔ ((bc) = ((a ∩ (bc)) = x = (a ∪ (bc)))))
22 anass 630 . . . . . . . . 9 ((((ab) = d = (ab)) ((dc) = x = (dc))) ↔ ((ab) = (d = (ab) ((dc) = x = (dc)))))
23 an12 772 . . . . . . . . 9 (((ab) = (d = (ab) ((dc) = x = (dc)))) ↔ (d = (ab) ((ab) = ((dc) = x = (dc)))))
2422, 23bitri 240 . . . . . . . 8 ((((ab) = d = (ab)) ((dc) = x = (dc))) ↔ (d = (ab) ((ab) = ((dc) = x = (dc)))))
2524exbii 1582 . . . . . . 7 (d(((ab) = d = (ab)) ((dc) = x = (dc))) ↔ d(d = (ab) ((ab) = ((dc) = x = (dc)))))
26 vex 2862 . . . . . . . . 9 a V
27 vex 2862 . . . . . . . . 9 b V
2826, 27unex 4106 . . . . . . . 8 (ab) V
29 ineq1 3450 . . . . . . . . . . 11 (d = (ab) → (dc) = ((ab) ∩ c))
3029eqeq1d 2361 . . . . . . . . . 10 (d = (ab) → ((dc) = ↔ ((ab) ∩ c) = ))
31 uneq1 3411 . . . . . . . . . . 11 (d = (ab) → (dc) = ((ab) ∪ c))
3231eqeq2d 2364 . . . . . . . . . 10 (d = (ab) → (x = (dc) ↔ x = ((ab) ∪ c)))
3330, 32anbi12d 691 . . . . . . . . 9 (d = (ab) → (((dc) = x = (dc)) ↔ (((ab) ∩ c) = x = ((ab) ∪ c))))
3433anbi2d 684 . . . . . . . 8 (d = (ab) → (((ab) = ((dc) = x = (dc))) ↔ ((ab) = (((ab) ∩ c) = x = ((ab) ∪ c)))))
3528, 34ceqsexv 2894 . . . . . . 7 (d(d = (ab) ((ab) = ((dc) = x = (dc)))) ↔ ((ab) = (((ab) ∩ c) = x = ((ab) ∪ c))))
3625, 35bitri 240 . . . . . 6 (d(((ab) = d = (ab)) ((dc) = x = (dc))) ↔ ((ab) = (((ab) ∩ c) = x = ((ab) ∪ c))))
37 anass 630 . . . . . . . . 9 ((((bc) = e = (bc)) ((ae) = x = (ae))) ↔ ((bc) = (e = (bc) ((ae) = x = (ae)))))
38 an12 772 . . . . . . . . 9 (((bc) = (e = (bc) ((ae) = x = (ae)))) ↔ (e = (bc) ((bc) = ((ae) = x = (ae)))))
3937, 38bitri 240 . . . . . . . 8 ((((bc) = e = (bc)) ((ae) = x = (ae))) ↔ (e = (bc) ((bc) = ((ae) = x = (ae)))))
4039exbii 1582 . . . . . . 7 (e(((bc) = e = (bc)) ((ae) = x = (ae))) ↔ e(e = (bc) ((bc) = ((ae) = x = (ae)))))
41 vex 2862 . . . . . . . . 9 c V
4227, 41unex 4106 . . . . . . . 8 (bc) V
43 ineq2 3451 . . . . . . . . . . 11 (e = (bc) → (ae) = (a ∩ (bc)))
4443eqeq1d 2361 . . . . . . . . . 10 (e = (bc) → ((ae) = ↔ (a ∩ (bc)) = ))
45 uneq2 3412 . . . . . . . . . . 11 (e = (bc) → (ae) = (a ∪ (bc)))
4645eqeq2d 2364 . . . . . . . . . 10 (e = (bc) → (x = (ae) ↔ x = (a ∪ (bc))))
4744, 46anbi12d 691 . . . . . . . . 9 (e = (bc) → (((ae) = x = (ae)) ↔ ((a ∩ (bc)) = x = (a ∪ (bc)))))
4847anbi2d 684 . . . . . . . 8 (e = (bc) → (((bc) = ((ae) = x = (ae))) ↔ ((bc) = ((a ∩ (bc)) = x = (a ∪ (bc))))))
4942, 48ceqsexv 2894 . . . . . . 7 (e(e = (bc) ((bc) = ((ae) = x = (ae)))) ↔ ((bc) = ((a ∩ (bc)) = x = (a ∪ (bc)))))
5040, 49bitri 240 . . . . . 6 (e(((bc) = e = (bc)) ((ae) = x = (ae))) ↔ ((bc) = ((a ∩ (bc)) = x = (a ∪ (bc)))))
5121, 36, 503bitr4i 268 . . . . 5 (d(((ab) = d = (ab)) ((dc) = x = (dc))) ↔ e(((bc) = e = (bc)) ((ae) = x = (ae))))
5251rexbii 2639 . . . 4 (c C d(((ab) = d = (ab)) ((dc) = x = (dc))) ↔ c C e(((bc) = e = (bc)) ((ae) = x = (ae))))
53522rexbii 2641 . . 3 (a A b B c C d(((ab) = d = (ab)) ((dc) = x = (dc))) ↔ a A b B c C e(((bc) = e = (bc)) ((ae) = x = (ae))))
54 eladdc 4398 . . . 4 (x ((A +c B) +c C) ↔ d (A +c B)c C ((dc) = x = (dc)))
55 df-rex 2620 . . . . 5 (d (A +c B)c C ((dc) = x = (dc)) ↔ d(d (A +c B) c C ((dc) = x = (dc))))
56 rexcom4 2878 . . . . . 6 (a A db B (((ab) = d = (ab)) c C ((dc) = x = (dc))) ↔ da A b B (((ab) = d = (ab)) c C ((dc) = x = (dc))))
57 rexcom4 2878 . . . . . . . . . 10 (c C d(((ab) = d = (ab)) ((dc) = x = (dc))) ↔ dc C (((ab) = d = (ab)) ((dc) = x = (dc))))
58 r19.42v 2765 . . . . . . . . . . 11 (c C (((ab) = d = (ab)) ((dc) = x = (dc))) ↔ (((ab) = d = (ab)) c C ((dc) = x = (dc))))
5958exbii 1582 . . . . . . . . . 10 (dc C (((ab) = d = (ab)) ((dc) = x = (dc))) ↔ d(((ab) = d = (ab)) c C ((dc) = x = (dc))))
6057, 59bitri 240 . . . . . . . . 9 (c C d(((ab) = d = (ab)) ((dc) = x = (dc))) ↔ d(((ab) = d = (ab)) c C ((dc) = x = (dc))))
6160rexbii 2639 . . . . . . . 8 (b B c C d(((ab) = d = (ab)) ((dc) = x = (dc))) ↔ b B d(((ab) = d = (ab)) c C ((dc) = x = (dc))))
62 rexcom4 2878 . . . . . . . 8 (b B d(((ab) = d = (ab)) c C ((dc) = x = (dc))) ↔ db B (((ab) = d = (ab)) c C ((dc) = x = (dc))))
6361, 62bitri 240 . . . . . . 7 (b B c C d(((ab) = d = (ab)) ((dc) = x = (dc))) ↔ db B (((ab) = d = (ab)) c C ((dc) = x = (dc))))
6463rexbii 2639 . . . . . 6 (a A b B c C d(((ab) = d = (ab)) ((dc) = x = (dc))) ↔ a A db B (((ab) = d = (ab)) c C ((dc) = x = (dc))))
65 r19.41v 2764 . . . . . . . 8 (a A (b B ((ab) = d = (ab)) c C ((dc) = x = (dc))) ↔ (a A b B ((ab) = d = (ab)) c C ((dc) = x = (dc))))
66 r19.41v 2764 . . . . . . . . 9 (b B (((ab) = d = (ab)) c C ((dc) = x = (dc))) ↔ (b B ((ab) = d = (ab)) c C ((dc) = x = (dc))))
6766rexbii 2639 . . . . . . . 8 (a A b B (((ab) = d = (ab)) c C ((dc) = x = (dc))) ↔ a A (b B ((ab) = d = (ab)) c C ((dc) = x = (dc))))
68 eladdc 4398 . . . . . . . . 9 (d (A +c B) ↔ a A b B ((ab) = d = (ab)))
6968anbi1i 676 . . . . . . . 8 ((d (A +c B) c C ((dc) = x = (dc))) ↔ (a A b B ((ab) = d = (ab)) c C ((dc) = x = (dc))))
7065, 67, 693bitr4ri 269 . . . . . . 7 ((d (A +c B) c C ((dc) = x = (dc))) ↔ a A b B (((ab) = d = (ab)) c C ((dc) = x = (dc))))
7170exbii 1582 . . . . . 6 (d(d (A +c B) c C ((dc) = x = (dc))) ↔ da A b B (((ab) = d = (ab)) c C ((dc) = x = (dc))))
7256, 64, 713bitr4ri 269 . . . . 5 (d(d (A +c B) c C ((dc) = x = (dc))) ↔ a A b B c C d(((ab) = d = (ab)) ((dc) = x = (dc))))
7355, 72bitri 240 . . . 4 (d (A +c B)c C ((dc) = x = (dc)) ↔ a A b B c C d(((ab) = d = (ab)) ((dc) = x = (dc))))
7454, 73bitri 240 . . 3 (x ((A +c B) +c C) ↔ a A b B c C d(((ab) = d = (ab)) ((dc) = x = (dc))))
75 eladdc 4398 . . . 4 (x (A +c (B +c C)) ↔ a A e (B +c C)((ae) = x = (ae)))
76 df-rex 2620 . . . . . 6 (e (B +c C)((ae) = x = (ae)) ↔ e(e (B +c C) ((ae) = x = (ae))))
77 rexcom4 2878 . . . . . . 7 (b B ec C (((bc) = e = (bc)) ((ae) = x = (ae))) ↔ eb B c C (((bc) = e = (bc)) ((ae) = x = (ae))))
78 rexcom4 2878 . . . . . . . 8 (c C e(((bc) = e = (bc)) ((ae) = x = (ae))) ↔ ec C (((bc) = e = (bc)) ((ae) = x = (ae))))
7978rexbii 2639 . . . . . . 7 (b B c C e(((bc) = e = (bc)) ((ae) = x = (ae))) ↔ b B ec C (((bc) = e = (bc)) ((ae) = x = (ae))))
80 r19.41v 2764 . . . . . . . . 9 (b B (c C ((bc) = e = (bc)) ((ae) = x = (ae))) ↔ (b B c C ((bc) = e = (bc)) ((ae) = x = (ae))))
81 r19.41v 2764 . . . . . . . . . 10 (c C (((bc) = e = (bc)) ((ae) = x = (ae))) ↔ (c C ((bc) = e = (bc)) ((ae) = x = (ae))))
8281rexbii 2639 . . . . . . . . 9 (b B c C (((bc) = e = (bc)) ((ae) = x = (ae))) ↔ b B (c C ((bc) = e = (bc)) ((ae) = x = (ae))))
83 eladdc 4398 . . . . . . . . . 10 (e (B +c C) ↔ b B c C ((bc) = e = (bc)))
8483anbi1i 676 . . . . . . . . 9 ((e (B +c C) ((ae) = x = (ae))) ↔ (b B c C ((bc) = e = (bc)) ((ae) = x = (ae))))
8580, 82, 843bitr4ri 269 . . . . . . . 8 ((e (B +c C) ((ae) = x = (ae))) ↔ b B c C (((bc) = e = (bc)) ((ae) = x = (ae))))
8685exbii 1582 . . . . . . 7 (e(e (B +c C) ((ae) = x = (ae))) ↔ eb B c C (((bc) = e = (bc)) ((ae) = x = (ae))))
8777, 79, 863bitr4ri 269 . . . . . 6 (e(e (B +c C) ((ae) = x = (ae))) ↔ b B c C e(((bc) = e = (bc)) ((ae) = x = (ae))))
8876, 87bitri 240 . . . . 5 (e (B +c C)((ae) = x = (ae)) ↔ b B c C e(((bc) = e = (bc)) ((ae) = x = (ae))))
8988rexbii 2639 . . . 4 (a A e (B +c C)((ae) = x = (ae)) ↔ a A b B c C e(((bc) = e = (bc)) ((ae) = x = (ae))))
9075, 89bitri 240 . . 3 (x (A +c (B +c C)) ↔ a A b B c C e(((bc) = e = (bc)) ((ae) = x = (ae))))
9153, 74, 903bitr4i 268 . 2 (x ((A +c B) +c C) ↔ x (A +c (B +c C)))
9291eqriv 2350 1 ((A +c B) +c C) = (A +c (B +c C))
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 358  ∃wex 1541   = wceq 1642   ∈ wcel 1710  ∃wrex 2615   ∪ cun 3207   ∩ cin 3208  ∅c0 3550   +c cplc 4375 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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  ax-nin 4078 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-ral 2619  df-rex 2620  df-v 2861  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-ss 3259  df-nul 3551  df-addc 4378 This theorem is referenced by:  addc32  4416  addc4  4417  addc6  4418  nncaddccl  4419  ltfinirr  4457  leltfintr  4458  ltfintr  4459  lefinlteq  4463  ltlefin  4468  sucoddeven  4511  evenodddisj  4516  sfinltfin  4535  lectr  6211  addceq0  6219  nclenn  6249  lecadd2  6266  ncslesuc  6267  nncdiv3  6277  nnc3n3p1  6278  nnc3n3p2  6279  nnc3p1n3p2  6280  nchoicelem1  6289  nchoicelem2  6290
 Copyright terms: Public domain W3C validator