| 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), so that their Theorem pm110.643 4846 shows the derivation of 1+1=2 for cardinal numbers from this theorem. |
| Ref | Expression |
|---|---|
| pm54.43 |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 1on 4076 |
. . . . . . . 8
| |
| 2 | 1 | onirr 3060 |
. . . . . . 7
|
| 3 | disjsn 2412 |
. . . . . . 7
| |
| 4 | 2, 3 | mpbir 190 |
. . . . . 6
|
| 5 | unen 4368 |
. . . . . 6
| |
| 6 | 4, 5 | mpanr2 707 |
. . . . 5
|
| 7 | 6 | ex 373 |
. . . 4
|
| 8 | 1 | elisseti 1793 |
. . . . . 6
|
| 9 | 8 | ensn1 4359 |
. . . . . 6
|
| 10 | 8, 9 | ensymi 4348 |
. . . . 5
|
| 11 | entrt 4349 |
. . . . 5
| |
| 12 | 10, 11 | mpan2 693 |
. . . 4
|
| 13 | 7, 12 | sylan2 451 |
. . 3
|
| 14 | df-2o 4072 |
. . . . 5
| |
| 15 | df-suc 2917 |
. . . . 5
| |
| 16 | 14, 15 | eqtr 1471 |
. . . 4
|
| 17 | 16 | breq2i 2595 |
. . 3
|
| 18 | 13, 17 | syl6ibr 213 |
. 2
|
| 19 | sneq 2388 |
. . . . . . . . . . . . . . 15
| |
| 20 | 19 | uneq2d 2155 |
. . . . . . . . . . . . . 14
|
| 21 | unidm 2146 |
. . . . . . . . . . . . . 14
| |
| 22 | 20, 21 | syl5reqr 1498 |
. . . . . . . . . . . . 13
|
| 23 | visset 1788 |
. . . . . . . . . . . . . . 15
| |
| 24 | 23 | ensn1 4359 |
. . . . . . . . . . . . . 14
|
| 25 | 1sdom2 4457 |
. . . . . . . . . . . . . 14
| |
| 26 | ensdomtr 4405 |
. . . . . . . . . . . . . 14
| |
| 27 | 24, 25, 26 | mp2an 694 |
. . . . . . . . . . . . 13
|
| 28 | 22, 27 | syl6eqbr 2620 |
. . . . . . . . . . . 12
|
| 29 | sdomnen 4322 |
. . . . . . . . . . . 12
| |
| 30 | 28, 29 | syl 10 |
. . . . . . . . . . 11
|
| 31 | 30 | necon2ai 1587 |
. . . . . . . . . 10
|
| 32 | disjsn2 2413 |
. . . . . . . . . 10
| |
| 33 | 31, 32 | syl 10 |
. . . . . . . . 9
|
| 34 | 33 | a1i 8 |
. . . . . . . 8
|
| 35 | uneq12 2150 |
. . . . . . . . 9
| |
| 36 | 35 | breq1d 2597 |
. . . . . . . 8
|
| 37 | ineq12 2183 |
. . . . . . . . 9
| |
| 38 | 37 | eqeq1d 1459 |
. . . . . . . 8
|
| 39 | 34, 36, 38 | 3imtr4d 541 |
. . . . . . 7
|
| 40 | 39 | ex 373 |
. . . . . 6
|
| 41 | 40 | 19.23adv 1198 |
. . . . 5
|
| 42 | 41 | 19.23aiv 1277 |
. . . 4
|
| 43 | 42 | imp 350 |
. . 3
|
| 44 | en1 4361 |
. . 3
| |
| 45 | en1 4361 |
. . 3
| |
| 46 | 43, 44, 45 | syl2anb 455 |
. 2
|
| 47 | 18, 46 | impbid 514 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: pm110.643 4846 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-4 951 ax-5 952 ax-6 953 ax-7 954 ax-gen 955 ax-8 1101 ax-9 1102 ax-10 1103 ax-12 1104 ax-13 1107 ax-14 1108 ax-11 1180 ax-17 1190 ax-16 1194 ax-11o 1202 ax-ext 1436 ax-rep 2661 ax-sep 2671 ax-nul 2678 ax-pow 2710 ax-pr 2747 ax-un 2830 |
| This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 773 df-3an 774 df-ex 957 df-sb 1155 df-eu 1359 df-mo 1360 df-clab 1441 df-cleq 1446 df-clel 1449 df-ne 1563 df-ral 1625 df-rex 1626 df-reu 1627 df-rab 1628 df-v 1787 df-dif 2020 df-un 2021 df-in 2022 df-ss 2024 df-nul 2252 df-pw 2373 df-sn 2383 df-pr 2384 df-tp 2386 df-op 2387 df-uni 2472 df-br 2588 df-opab 2635 df-tr 2649 df-eprel 2794 df-id 2797 df-po 2804 df-so 2814 df-fr 2880 df-we 2897 df-ord 2914 df-on 2915 df-suc 2917 df-xp 3147 df-rel 3148 df-cnv 3149 df-co 3150 df-dm 3151 df-rn 3152 df-res 3153 df-ima 3154 df-fun 3155 df-fn 3156 df-f 3157 df-f1 3158 df-fo 3159 df-f1o 3160 df-fv 3161 df-1o 4071 df-2o 4072 df-er 4199 df-en 4305 df-dom 4306 df-sdom 4307 |