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

Theorem pm54.43 7043
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 7011), so that their means, in our notation, which is the same as by pm54.43lem 7042. 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 7173 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 5910 . . . . . . . 8
21elexi 2509 . . . . . . 7
32ensn1 6309 . . . . . 6
43ensymi 6296 . . . . 5
5 entr 6297 . . . . 5
64, 5mpan2 647 . . . 4
71onirri 4036 . . . . . . 7
8 disjsn 3320 . . . . . . 7
97, 8mpbir 198 . . . . . 6
10 unen 6327 . . . . . 6
119, 10mpanr2 660 . . . . 5
1211ex 419 . . . 4
136, 12sylan2 453 . . 3
14 df-2o 5904 . . . . 5
15 df-suc 3937 . . . . 5
1614, 15eqtri 2110 . . . 4
1716breq2i 3599 . . 3
1813, 17syl6ibr 216 . 2
19 en1 6312 . . 3
20 en1 6312 . . 3
21 unidm 2955 . . . . . . . . . . . . . 14
22 sneq 3279 . . . . . . . . . . . . . . 15
2322uneq2d 2966 . . . . . . . . . . . . . 14
2421, 23syl5reqr 2137 . . . . . . . . . . . . 13
25 vex 2503 . . . . . . . . . . . . . . 15
2625ensn1 6309 . . . . . . . . . . . . . 14
27 1sdom2 6492 . . . . . . . . . . . . . 14
28 ensdomtr 6381 . . . . . . . . . . . . . 14
2926, 27, 28mp2an 648 . . . . . . . . . . . . 13
3024, 29syl6eqbr 3628 . . . . . . . . . . . 12
31 sdomnen 6274 . . . . . . . . . . . 12
3230, 31syl 15 . . . . . . . . . . 11
3332necon2ai 2251 . . . . . . . . . 10
34 disjsn2 3322 . . . . . . . . . 10
3533, 34syl 15 . . . . . . . . 9
3635a1i 10 . . . . . . . 8
37 uneq12 2961 . . . . . . . . 9
3837breq1d 3601 . . . . . . . 8
39 ineq12 3000 . . . . . . . . 9
4039eqeq1d 2098 . . . . . . . 8
4136, 38, 403imtr4d 257 . . . . . . 7
4241ex 419 . . . . . 6
4342exlimdv 1797 . . . . 5
4443exlimiv 1883 . . . 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 1450   wceq 1531   wcel 1533   wne 2207   cun 2808   cin 2809  c0 3085  csn 3268   class class class wbr 3591  con0 3931   csuc 3933  c1o 5896  c2o 5897   cen 6245   csdm 6247
This theorem is referenced by:  pr2nelem  7044  isprm2lem  10995
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1446  ax-6 1447  ax-7 1448  ax-gen 1449  ax-8 1535  ax-11 1536  ax-12 1537  ax-13 1538  ax-14 1539  ax-17 1542  ax-9 1563  ax-10 1591  ax-4 1605  ax-16 1790  ax-ext 2072  ax-sep 3687  ax-nul 3696  ax-pow 3732  ax-pr 3756  ax-un 4049
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 900  df-3an 901  df-tru 1264  df-ex 1451  df-sb 1751  df-eu 1984  df-mo 1985  df-clab 2078  df-cleq 2083  df-clel 2086  df-ne 2209  df-ral 2303  df-rex 2304  df-reu 2305  df-rab 2306  df-v 2502  df-sbc 2669  df-dif 2813  df-un 2815  df-in 2817  df-ss 2821  df-pss 2823  df-nul 3086  df-if 3195  df-pw 3256  df-sn 3274  df-pr 3275  df-tp 3276  df-op 3277  df-uni 3435  df-br 3592  df-opab 3645  df-tr 3660  df-eprel 3844  df-id 3848  df-po 3853  df-so 3854  df-fr 3891  df-we 3893  df-ord 3934  df-on 3935  df-lim 3936  df-suc 3937  df-om 4216  df-xp 4263  df-rel 4264  df-cnv 4265  df-co 4266  df-dm 4267  df-rn 4268  df-res 4269  df-ima 4270  df-fun 4271  df-fn 4272  df-f 4273  df-f1 4274  df-fo 4275  df-f1o 4276  df-fv 4277  df-1o 5903  df-2o 5904  df-er 6076  df-en 6249  df-dom 6250  df-sdom 6251
Copyright terms: Public domain