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

Theorem pm54.43 6510
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 6483), so that their means, in our notation, which is the same as by pm54.43lem 6509. 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 6608 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 5579 . . . . . . . 8
21elexi 2336 . . . . . . 7
32ensn1 5924 . . . . . 6
43ensymi 5913 . . . . 5
5 entr 5914 . . . . 5
64, 5mpan2 647 . . . 4
71onirri 3823 . . . . . . 7
8 disjsn 3138 . . . . . . 7
97, 8mpbir 198 . . . . . 6
10 unen 5942 . . . . . 6
119, 10mpanr2 660 . . . . 5
1211ex 419 . . . 4
136, 12sylan2 453 . . 3
14 df-2o 5573 . . . . 5
15 df-suc 3724 . . . . 5
1614, 15eqtri 1938 . . . 4
1716breq2i 3404 . . 3
1813, 17syl6ibr 216 . 2
19 en1 5927 . . 3
20 en1 5927 . . 3
21 unidm 2781 . . . . . . . . . . . . . 14
22 sneq 3097 . . . . . . . . . . . . . . 15
2322uneq2d 2792 . . . . . . . . . . . . . 14
2421, 23syl5reqr 1965 . . . . . . . . . . . . 13
25 vex 2330 . . . . . . . . . . . . . . 15
2625ensn1 5924 . . . . . . . . . . . . . 14
27 1sdom2 6100 . . . . . . . . . . . . . 14
28 ensdomtr 5990 . . . . . . . . . . . . . 14
2926, 27, 28mp2an 648 . . . . . . . . . . . . 13
3024, 29syl6eqbr 3433 . . . . . . . . . . . 12
31 sdomnen 5893 . . . . . . . . . . . 12
3230, 31syl 15 . . . . . . . . . . 11
3332necon2ai 2079 . . . . . . . . . 10
34 disjsn2 3140 . . . . . . . . . 10
3533, 34syl 15 . . . . . . . . 9
3635a1i 10 . . . . . . . 8
37 uneq12 2787 . . . . . . . . 9
3837breq1d 3406 . . . . . . . 8
39 ineq12 2824 . . . . . . . . 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 2635   cin 2636  c0 2907  csn 3086   class class class wbr 3396  con0 3718   csuc 3720  c1o 5565  c2o 5566   cen 5865   csdm 5867
This theorem is referenced by:  pr2nelem 6511  isprm2lem 10171
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 3481  ax-sep 3491  ax-nul 3500  ax-pow 3536  ax-pr 3560  ax-un 3836
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 2329  df-sbc 2496  df-dif 2640  df-un 2642  df-in 2644  df-ss 2648  df-pss 2650  df-nul 2908  df-if 3015  df-pw 3075  df-sn 3092  df-pr 3093  df-tp 3094  df-op 3095  df-uni 3247  df-br 3397  df-opab 3450  df-tr 3465  df-eprel 3646  df-id 3650  df-po 3655  df-so 3669  df-fr 3689  df-we 3705  df-ord 3721  df-on 3722  df-lim 3723  df-suc 3724  df-om 4001  df-xp 4048  df-rel 4049  df-cnv 4050  df-co 4051  df-dm 4052  df-rn 4053  df-res 4054  df-ima 4055  df-fun 4056  df-fn 4057  df-f 4058  df-f1 4059  df-fo 4060  df-f1o 4061  df-fv 4062  df-1o 5572  df-2o 5573  df-er 5710  df-en 5869  df-dom 5870  df-sdom 5871
Copyright terms: Public domain