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

Theorem pm54.43 6427
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 6403), so that their means, in our notation, which is the same as by pm54.43lem 6426. 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 6521 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 5512 . . . . . . 7
21elexi 2333 . . . . . 6
32ensn1 5859 . . . . . 6
42, 3ensymi 5848 . . . . 5
5 entr 5849 . . . . 5
64, 5mpan2 647 . . . 4
71onirri 3796 . . . . . . 7
8 disjsn 3125 . . . . . . 7
97, 8mpbir 198 . . . . . 6
10 unen 5875 . . . . . 6
119, 10mpanr2 660 . . . . 5
1211ex 419 . . . 4
136, 12sylan2 453 . . 3
14 df-2o 5506 . . . . 5
15 df-suc 3697 . . . . 5
1614, 15eqtri 1938 . . . 4
1716breq2i 3378 . . 3
1813, 17syl6ibr 216 . 2
19 en1 5862 . . 3
20 en1 5862 . . 3
21 unidm 2776 . . . . . . . . . . . . . 14
22 sneq 3090 . . . . . . . . . . . . . . 15
2322uneq2d 2787 . . . . . . . . . . . . . 14
2421, 23syl5reqr 1965 . . . . . . . . . . . . 13
25 vex 2327 . . . . . . . . . . . . . . 15
2625ensn1 5859 . . . . . . . . . . . . . 14
27 1sdom2 6033 . . . . . . . . . . . . . 14
28 ensdomtr 5916 . . . . . . . . . . . . . 14
2926, 27, 28mp2an 648 . . . . . . . . . . . . 13
3024, 29syl6eqbr 3407 . . . . . . . . . . . 12
31 sdomnen 5819 . . . . . . . . . . . 12
3230, 31syl 15 . . . . . . . . . . 11
3332necon2ai 2079 . . . . . . . . . 10
34 disjsn2 3127 . . . . . . . . . 10
3533, 34syl 15 . . . . . . . . 9
3635a1i 10 . . . . . . . 8
37 uneq12 2782 . . . . . . . . 9
3837breq1d 3380 . . . . . . . 8
39 ineq12 2819 . . . . . . . . 9
4039eqeq1d 1926 . . . . . . . 8
4136, 38, 403imtr4d 257 . . . . . . 7
4241ex 419 . . . . . 6
4342exlimdv 1635 . . . . 5
4443exlimiv 1718 . . . 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 1335   wceq 1414   wcel 1416   wne 2035   cun 2632   cin 2633  c0 2902  csn 3079   class class class wbr 3370  con0 3691   csuc 3693  c1o 5498  c2o 5499   cen 5796   csdm 5798
This theorem is referenced by:  pr2nelem 6428  pm110.643 6521  isprm2lem 9922
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1331  ax-6 1332  ax-7 1333  ax-gen 1334  ax-8 1418  ax-10 1419  ax-11 1420  ax-12 1421  ax-13 1422  ax-14 1423  ax-17 1430  ax-9 1445  ax-4 1451  ax-16 1629  ax-ext 1900  ax-rep 3456  ax-sep 3466  ax-nul 3475  ax-pow 3511  ax-pr 3535  ax-un 3809
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 900  df-3an 901  df-tru 1309  df-ex 1336  df-sb 1591  df-eu 1818  df-mo 1819  df-clab 1906  df-cleq 1911  df-clel 1914  df-ne 2037  df-ral 2131  df-rex 2132  df-reu 2133  df-rab 2134  df-v 2326  df-dif 2637  df-un 2639  df-in 2641  df-ss 2645  df-pss 2647  df-nul 2903  df-pw 3068  df-sn 3085  df-pr 3086  df-tp 3087  df-op 3088  df-uni 3224  df-br 3371  df-opab 3425  df-tr 3440  df-eprel 3620  df-id 3623  df-po 3628  df-so 3642  df-fr 3662  df-we 3678  df-ord 3694  df-on 3695  df-suc 3697  df-xp 4021  df-rel 4022  df-cnv 4023  df-co 4024  df-dm 4025  df-rn 4026  df-res 4027  df-ima 4028  df-fun 4029  df-fn 4030  df-f 4031  df-f1 4032  df-fo 4033  df-f1o 4034  df-fv 4035  df-1o 5505  df-2o 5506  df-er 5643  df-en 5800  df-dom 5801  df-sdom 5802
Copyright terms: Public domain