| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Theorem *54.43 of [WhiteheadRussell] p. 360. "From
this proposition it
will follow, when arithmetical addition has been defined, that
1+1=2."
See http://en.wikipedia.org/wiki/Principia_Mathematica#Quotations.
This theorem states that two sets of cardinality 1 are disjoint iff
their union has cardinality 2.
Whitehead and Russell define 1 as the collection of all sets with
cardinality 1 (i.e. all singletons; see card1 4979), so that their
Theorem pm110.643 5072 shows the derivation of 1+1=2 for cardinal numbers from this theorem. |
| Ref | Expression |
|---|---|
| pm54.43 |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 1on 4272 |
. . . . . . . 8
| |
| 2 | 1 | onirri 3075 |
. . . . . . 7
|
| 3 | disjsn 2501 |
. . . . . . 7
| |
| 4 | 2, 3 | mpbir 188 |
. . . . . 6
|
| 5 | unen 4573 |
. . . . . 6
| |
| 6 | 4, 5 | mpanr2 713 |
. . . . 5
|
| 7 | 6 | ex 371 |
. . . 4
|
| 8 | 1 | elisseti 1863 |
. . . . . 6
|
| 9 | 8 | ensn1 4563 |
. . . . . 6
|
| 10 | 8, 9 | ensymi 4552 |
. . . . 5
|
| 11 | entr 4553 |
. . . . 5
| |
| 12 | 10, 11 | mpan2 699 |
. . . 4
|
| 13 | 7, 12 | sylan2 453 |
. . 3
|
| 14 | df-2o 4268 |
. . . . 5
| |
| 15 | df-suc 2980 |
. . . . 5
| |
| 16 | 14, 15 | eqtri 1537 |
. . . 4
|
| 17 | 16 | breq2i 2699 |
. . 3
|
| 18 | 13, 17 | syl6ibr 211 |
. 2
|
| 19 | sneq 2474 |
. . . . . . . . . . . . . . 15
| |
| 20 | 19 | uneq2d 2235 |
. . . . . . . . . . . . . 14
|
| 21 | unidm 2226 |
. . . . . . . . . . . . . 14
| |
| 22 | 20, 21 | syl5reqr 1564 |
. . . . . . . . . . . . 13
|
| 23 | visset 1858 |
. . . . . . . . . . . . . . 15
| |
| 24 | 23 | ensn1 4563 |
. . . . . . . . . . . . . 14
|
| 25 | 1sdom2 4670 |
. . . . . . . . . . . . . 14
| |
| 26 | ensdomtr 4614 |
. . . . . . . . . . . . . 14
| |
| 27 | 24, 25, 26 | mp2an 700 |
. . . . . . . . . . . . 13
|
| 28 | 22, 27 | syl6eqbr 2724 |
. . . . . . . . . . . 12
|
| 29 | sdomnen 4526 |
. . . . . . . . . . . 12
| |
| 30 | 28, 29 | syl 10 |
. . . . . . . . . . 11
|
| 31 | 30 | necon2ai 1653 |
. . . . . . . . . 10
|
| 32 | disjsn2 2502 |
. . . . . . . . . 10
| |
| 33 | 31, 32 | syl 10 |
. . . . . . . . 9
|
| 34 | 33 | a1i 8 |
. . . . . . . 8
|
| 35 | uneq12 2230 |
. . . . . . . . 9
| |
| 36 | 35 | breq1d 2701 |
. . . . . . . 8
|
| 37 | ineq12 2263 |
. . . . . . . . 9
| |
| 38 | 37 | eqeq1d 1525 |
. . . . . . . 8
|
| 39 | 34, 36, 38 | 3imtr4d 545 |
. . . . . . 7
|
| 40 | 39 | ex 371 |
. . . . . 6
|
| 41 | 40 | 19.23adv 1250 |
. . . . 5
|
| 42 | 41 | 19.23aiv 1332 |
. . . 4
|
| 43 | 42 | imp 348 |
. . 3
|
| 44 | en1 4565 |
. . 3
| |
| 45 | en1 4565 |
. . 3
| |
| 46 | 43, 44, 45 | syl2anb 457 |
. 2
|
| 47 | 18, 46 | impbid 518 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: pm110.643 5072 unpde2eg2 11010 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 997 ax-gen 998 ax-8 999 ax-9 1000 ax-10 1001 ax-11 1002 ax-12 1003 ax-13 1004 ax-14 1005 ax-17 1006 ax-4 1008 ax-5o 1010 ax-6o 1013 ax-9o 1158 ax-10o 1176 ax-16 1246 ax-11o 1254 ax-ext 1499 ax-rep 2766 ax-sep 2776 ax-nul 2783 ax-pow 2817 ax-pr 2854 ax-un 3088 |
| This theorem depends on definitions: df-bi 145 df-or 222 df-an 223 df-3or 781 df-3an 782 df-ex 1016 df-sb 1208 df-eu 1420 df-mo 1421 df-clab 1505 df-cleq 1510 df-clel 1513 df-ne 1629 df-ral 1694 df-rex 1695 df-reu 1696 df-rab 1697 df-v 1857 df-dif 2100 df-un 2101 df-in 2102 df-ss 2104 df-nul 2332 df-pw 2458 df-sn 2469 df-pr 2470 df-tp 2472 df-op 2473 df-uni 2569 df-br 2692 df-opab 2740 df-tr 2754 df-eprel 2909 df-id 2912 df-po 2917 df-so 2928 df-fr 2946 df-we 2961 df-ord 2977 df-on 2978 df-suc 2980 df-xp 3264 df-rel 3265 df-cnv 3266 df-co 3267 df-dm 3268 df-rn 3269 df-res 3270 df-ima 3271 df-fun 3272 df-fn 3273 df-f 3274 df-f1 3275 df-fo 3276 df-f1o 3277 df-fv 3278 df-1o 4267 df-2o 4268 df-er 4399 df-en 4507 df-dom 4508 df-sdom 4509 |