HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem pm54.43 6884
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 6852), so that their means, in our notation, which is the same as by pm54.43lem 6883. We do not have several of their earlier lemmas available (which would otherwise be unused by our different approach to arithmetic), so our proof is longer. (It is also longer because we must show every detail.)

Theorem pm110.643 7014 shows the derivation of 1+1=2 for cardinal numbers from this theorem.

Assertion
Ref Expression
pm54.43

Proof of Theorem pm54.43
StepHypRef Expression
1 1on 5805 . . . . . . . 8
21elexi 2449 . . . . . . 7
32ensn1 6177 . . . . . 6
43ensymi 6165 . . . . 5
5 entr 6166 . . . . 5
64, 5mpan2 647 . . . 4
71onirri 3960 . . . . . . 7
8 disjsn 3260 . . . . . . 7
97, 8mpbir 198 . . . . . 6
10 unen 6195 . . . . . 6
119, 10mpanr2 660 . . . . 5
1211ex 419 . . . 4
136, 12sylan2 453 . . 3
14 df-2o 5799 . . . . 5
15 df-suc 3861 . . . . 5
1614, 15eqtri 2050 . . . 4
1716breq2i 3539 . . 3
1813, 17syl6ibr 216 . 2
19 en1 6180 . . 3
20 en1 6180 . . 3
21 unidm 2895 . . . . . . . . . . . . . 14
22 sneq 3219 . . . . . . . . . . . . . . 15
2322uneq2d 2906 . . . . . . . . . . . . . 14
2421, 23syl5reqr 2077 . . . . . . . . . . . . 13
25 vex 2443 . . . . . . . . . . . . . . 15
2625ensn1 6177 . . . . . . . . . . . . . 14
27 1sdom2 6362 . . . . . . . . . . . . . 14
28 ensdomtr 6247 . . . . . . . . . . . . . 14
2926, 27, 28mp2an 648 . . . . . . . . . . . . 13
3024, 29syl6eqbr 3568 . . . . . . . . . . . 12
31 sdomnen 6145 . . . . . . . . . . . 12
3230, 31syl 15 . . . . . . . . . . 11
3332necon2ai 2191 . . . . . . . . . 10
34 disjsn2 3262 . . . . . . . . . 10
3533, 34syl 15 . . . . . . . . 9
3635a1i 10 . . . . . . . 8
37 uneq12 2901 . . . . . . . . 9
3837breq1d 3541 . . . . . . . 8
39 ineq12 2940 . . . . . . . . 9
4039eqeq1d 2038 . . . . . . . 8
4136, 38, 403imtr4d 257 . . . . . . 7
4241ex 419 . . . . . 6
4342exlimdv 1747 . . . . 5
4443exlimiv 1830 . . . 4
4544imp 414 . . 3
4619, 20, 45syl2anb 458 . 2
4718, 46impbid 181 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   wb 174   wa 357  wex 1447   wceq 1526   wcel 1528   wne 2147   cun 2748   cin 2749  c0 3025  csn 3208   class class class wbr 3531  con0 3855   csuc 3857  c1o 5791  c2o 5792   cen 6117   csdm 6119
This theorem is referenced by:  pr2nelem 6885  isprm2lem 10829
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1443  ax-6 1444  ax-7 1445  ax-gen 1446  ax-8 1530  ax-10 1531  ax-11 1532  ax-12 1533  ax-13 1534  ax-14 1535  ax-17 1542  ax-9 1557  ax-4 1563  ax-16 1741  ax-ext 2012  ax-rep 3616  ax-sep 3626  ax-nul 3635  ax-pow 3671  ax-pr 3695  ax-un 3973
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 900  df-3an 901  df-tru 1261  df-ex 1448  df-sb 1703  df-eu 1930  df-mo 1931  df-clab 2018  df-cleq 2023  df-clel 2026  df-ne 2149  df-ral 2243  df-rex 2244  df-reu 2245  df-rab 2246  df-v 2442  df-sbc 2609  df-dif 2753  df-un 2755  df-in 2757  df-ss 2761  df-pss 2763  df-nul 3026  df-if 3135  df-pw 3196  df-sn 3214  df-pr 3215  df-tp 3216  df-op 3217  df-uni 3375  df-br 3532  df-opab 3585  df-tr 3600  df-eprel 3783  df-id 3787  df-po 3792  df-so 3806  df-fr 3826  df-we 3842  df-ord 3858  df-on 3859  df-lim 3860  df-suc 3861  df-om 4139  df-xp 4186  df-rel 4187  df-cnv 4188  df-co 4189  df-dm 4190  df-rn 4191  df-res 4192  df-ima 4193  df-fun 4194  df-fn 4195  df-f 4196  df-f1 4197  df-fo 4198  df-f1o 4199  df-fv 4200  df-1o 5798  df-2o 5799  df-er 5952  df-en 6121  df-dom 6122  df-sdom 6123
Copyright terms: Public domain