New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > addcass | Unicode version |
Description: Cardinal addition is associative. Theorem X.1.11, corollary 1 of [Rosser] p. 277. (Contributed by SF, 17-Jan-2015.) |
Ref | Expression |
---|---|
addcass |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ancom 437 | . . . . . . . . . . 11 | |
2 | 1 | anbi2i 675 | . . . . . . . . . 10 |
3 | an12 772 | . . . . . . . . . 10 | |
4 | 2, 3 | bitri 240 | . . . . . . . . 9 |
5 | indir 3503 | . . . . . . . . . . . 12 | |
6 | 5 | eqeq1i 2360 | . . . . . . . . . . 11 |
7 | un00 3586 | . . . . . . . . . . 11 | |
8 | 6, 7 | bitr4i 243 | . . . . . . . . . 10 |
9 | 8 | anbi2i 675 | . . . . . . . . 9 |
10 | indi 3501 | . . . . . . . . . . . 12 | |
11 | 10 | eqeq1i 2360 | . . . . . . . . . . 11 |
12 | un00 3586 | . . . . . . . . . . 11 | |
13 | 11, 12 | bitr4i 243 | . . . . . . . . . 10 |
14 | 13 | anbi2i 675 | . . . . . . . . 9 |
15 | 4, 9, 14 | 3bitr4i 268 | . . . . . . . 8 |
16 | unass 3420 | . . . . . . . . 9 | |
17 | 16 | eqeq2i 2363 | . . . . . . . 8 |
18 | 15, 17 | anbi12i 678 | . . . . . . 7 |
19 | anass 630 | . . . . . . 7 | |
20 | anass 630 | . . . . . . 7 | |
21 | 18, 19, 20 | 3bitr3i 266 | . . . . . 6 |
22 | anass 630 | . . . . . . . . 9 | |
23 | an12 772 | . . . . . . . . 9 | |
24 | 22, 23 | bitri 240 | . . . . . . . 8 |
25 | 24 | exbii 1582 | . . . . . . 7 |
26 | vex 2862 | . . . . . . . . 9 | |
27 | vex 2862 | . . . . . . . . 9 | |
28 | 26, 27 | unex 4106 | . . . . . . . 8 |
29 | ineq1 3450 | . . . . . . . . . . 11 | |
30 | 29 | eqeq1d 2361 | . . . . . . . . . 10 |
31 | uneq1 3411 | . . . . . . . . . . 11 | |
32 | 31 | eqeq2d 2364 | . . . . . . . . . 10 |
33 | 30, 32 | anbi12d 691 | . . . . . . . . 9 |
34 | 33 | anbi2d 684 | . . . . . . . 8 |
35 | 28, 34 | ceqsexv 2894 | . . . . . . 7 |
36 | 25, 35 | bitri 240 | . . . . . 6 |
37 | anass 630 | . . . . . . . . 9 | |
38 | an12 772 | . . . . . . . . 9 | |
39 | 37, 38 | bitri 240 | . . . . . . . 8 |
40 | 39 | exbii 1582 | . . . . . . 7 |
41 | vex 2862 | . . . . . . . . 9 | |
42 | 27, 41 | unex 4106 | . . . . . . . 8 |
43 | ineq2 3451 | . . . . . . . . . . 11 | |
44 | 43 | eqeq1d 2361 | . . . . . . . . . 10 |
45 | uneq2 3412 | . . . . . . . . . . 11 | |
46 | 45 | eqeq2d 2364 | . . . . . . . . . 10 |
47 | 44, 46 | anbi12d 691 | . . . . . . . . 9 |
48 | 47 | anbi2d 684 | . . . . . . . 8 |
49 | 42, 48 | ceqsexv 2894 | . . . . . . 7 |
50 | 40, 49 | bitri 240 | . . . . . 6 |
51 | 21, 36, 50 | 3bitr4i 268 | . . . . 5 |
52 | 51 | rexbii 2639 | . . . 4 |
53 | 52 | 2rexbii 2641 | . . 3 |
54 | eladdc 4398 | . . . 4 | |
55 | df-rex 2620 | . . . . 5 | |
56 | rexcom4 2878 | . . . . . 6 | |
57 | rexcom4 2878 | . . . . . . . . . 10 | |
58 | r19.42v 2765 | . . . . . . . . . . 11 | |
59 | 58 | exbii 1582 | . . . . . . . . . 10 |
60 | 57, 59 | bitri 240 | . . . . . . . . 9 |
61 | 60 | rexbii 2639 | . . . . . . . 8 |
62 | rexcom4 2878 | . . . . . . . 8 | |
63 | 61, 62 | bitri 240 | . . . . . . 7 |
64 | 63 | rexbii 2639 | . . . . . 6 |
65 | r19.41v 2764 | . . . . . . . 8 | |
66 | r19.41v 2764 | . . . . . . . . 9 | |
67 | 66 | rexbii 2639 | . . . . . . . 8 |
68 | eladdc 4398 | . . . . . . . . 9 | |
69 | 68 | anbi1i 676 | . . . . . . . 8 |
70 | 65, 67, 69 | 3bitr4ri 269 | . . . . . . 7 |
71 | 70 | exbii 1582 | . . . . . 6 |
72 | 56, 64, 71 | 3bitr4ri 269 | . . . . 5 |
73 | 55, 72 | bitri 240 | . . . 4 |
74 | 54, 73 | bitri 240 | . . 3 |
75 | eladdc 4398 | . . . 4 | |
76 | df-rex 2620 | . . . . . 6 | |
77 | rexcom4 2878 | . . . . . . 7 | |
78 | rexcom4 2878 | . . . . . . . 8 | |
79 | 78 | rexbii 2639 | . . . . . . 7 |
80 | r19.41v 2764 | . . . . . . . . 9 | |
81 | r19.41v 2764 | . . . . . . . . . 10 | |
82 | 81 | rexbii 2639 | . . . . . . . . 9 |
83 | eladdc 4398 | . . . . . . . . . 10 | |
84 | 83 | anbi1i 676 | . . . . . . . . 9 |
85 | 80, 82, 84 | 3bitr4ri 269 | . . . . . . . 8 |
86 | 85 | exbii 1582 | . . . . . . 7 |
87 | 77, 79, 86 | 3bitr4ri 269 | . . . . . 6 |
88 | 76, 87 | bitri 240 | . . . . 5 |
89 | 88 | rexbii 2639 | . . . 4 |
90 | 75, 89 | bitri 240 | . . 3 |
91 | 53, 74, 90 | 3bitr4i 268 | . 2 |
92 | 91 | eqriv 2350 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wa 358 wex 1541 wceq 1642 wcel 1710 wrex 2615 cun 3207 cin 3208 c0 3550 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 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 |