| 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 6123), so that their
Theorem pm110.643 6243 shows the derivation of 1+1=2 for cardinal numbers from this theorem. |
| Ref | Expression |
|---|---|
| pm54.43 |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 1on 5349 |
. . . . . . 7
| |
| 2 | 1 | elisseti 2548 |
. . . . . 6
|
| 3 | 2 | ensn1 5644 |
. . . . . 6
|
| 4 | 2, 3 | ensymi 5633 |
. . . . 5
|
| 5 | entr 5634 |
. . . . 5
| |
| 6 | 4, 5 | mpan2 679 |
. . . 4
|
| 7 | 1 | onirri 3916 |
. . . . . . 7
|
| 8 | disjsn 3280 |
. . . . . . 7
| |
| 9 | 7, 8 | mpbir 273 |
. . . . . 6
|
| 10 | unen 5657 |
. . . . . 6
| |
| 11 | 9, 10 | mpanr2 697 |
. . . . 5
|
| 12 | 11 | ex 398 |
. . . 4
|
| 13 | 6, 12 | sylan2 600 |
. . 3
|
| 14 | df-2o 5345 |
. . . . 5
| |
| 15 | df-suc 3817 |
. . . . 5
| |
| 16 | 14, 15 | eqtri 2161 |
. . . 4
|
| 17 | 16 | breq2i 3515 |
. . 3
|
| 18 | 13, 17 | syl6ibr 262 |
. 2
|
| 19 | en1 5646 |
. . 3
| |
| 20 | en1 5646 |
. . 3
| |
| 21 | unidm 2962 |
. . . . . . . . . . . . . 14
| |
| 22 | sneq 3247 |
. . . . . . . . . . . . . . 15
| |
| 23 | 22 | uneq2d 2973 |
. . . . . . . . . . . . . 14
|
| 24 | 21, 23 | syl5reqr 2191 |
. . . . . . . . . . . . 13
|
| 25 | visset 2541 |
. . . . . . . . . . . . . . 15
| |
| 26 | 25 | ensn1 5644 |
. . . . . . . . . . . . . 14
|
| 27 | 1sdom2 5814 |
. . . . . . . . . . . . . 14
| |
| 28 | ensdomtr 5700 |
. . . . . . . . . . . . . 14
| |
| 29 | 26, 27, 28 | mp2an 681 |
. . . . . . . . . . . . 13
|
| 30 | 24, 29 | syl6eqbr 3548 |
. . . . . . . . . . . 12
|
| 31 | sdomnen 5607 |
. . . . . . . . . . . 12
| |
| 32 | 30, 31 | syl 13 |
. . . . . . . . . . 11
|
| 33 | 32 | necon2ai 2310 |
. . . . . . . . . 10
|
| 34 | disjsn2 3281 |
. . . . . . . . . 10
| |
| 35 | 33, 34 | syl 13 |
. . . . . . . . 9
|
| 36 | 35 | a1i 8 |
. . . . . . . 8
|
| 37 | uneq12 2968 |
. . . . . . . . 9
| |
| 38 | 37 | breq1d 3517 |
. . . . . . . 8
|
| 39 | ineq12 3004 |
. . . . . . . . 9
| |
| 40 | 39 | eqeq1d 2149 |
. . . . . . . 8
|
| 41 | 36, 38, 40 | 3imtr4d 330 |
. . . . . . 7
|
| 42 | 41 | ex 398 |
. . . . . 6
|
| 43 | 42 | 19.23adv 1860 |
. . . . 5
|
| 44 | 43 | 19.23aiv 1943 |
. . . 4
|
| 45 | 44 | imp 393 |
. . 3
|
| 46 | 19, 20, 45 | syl2anb 604 |
. 2
|
| 47 | 18, 46 | impbid 235 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: pm110.643 6243 isprm2lem 9368 unpde2eg2 15118 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1592 ax-gen 1593 ax-8 1594 ax-9 1595 ax-10 1596 ax-11 1597 ax-12 1598 ax-13 1599 ax-14 1600 ax-17 1605 ax-4 1608 ax-5o 1610 ax-6o 1613 ax-9o 1763 ax-10o 1781 ax-16 1854 ax-11o 1864 ax-ext 2123 ax-rep 3596 ax-sep 3606 ax-nul 3613 ax-pow 3649 ax-pr 3687 ax-un 3929 |
| This theorem depends on definitions: df-bi 220 df-or 338 df-an 339 df-3or 1103 df-3an 1104 df-ex 1616 df-sb 1816 df-eu 2041 df-mo 2042 df-clab 2129 df-cleq 2134 df-clel 2137 df-ne 2268 df-ral 2359 df-rex 2360 df-reu 2361 df-rab 2362 df-v 2540 df-dif 2830 df-un 2832 df-in 2834 df-ss 2836 df-pss 2838 df-nul 3083 df-pw 3229 df-sn 3242 df-pr 3243 df-tp 3245 df-op 3246 df-uni 3367 df-br 3508 df-opab 3566 df-tr 3580 df-eprel 3744 df-id 3747 df-po 3752 df-so 3764 df-fr 3782 df-we 3798 df-ord 3814 df-on 3815 df-suc 3817 df-xp 4133 df-rel 4134 df-cnv 4135 df-co 4136 df-dm 4137 df-rn 4138 df-res 4139 df-ima 4140 df-fun 4141 df-fn 4142 df-f 4143 df-f1 4144 df-fo 4145 df-f1o 4146 df-fv 4147 df-1o 5344 df-2o 5345 df-er 5479 df-en 5588 df-dom 5589 df-sdom 5590 |