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

Theorem pm54.43 6468
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 6442), so that their means, in our notation, which is the same as by pm54.43lem 6467. 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 6562 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 5542 . . . . . . 7
21elexi 2335 . . . . . 6
32ensn1 5889 . . . . . 6
42, 3ensymi 5878 . . . . 5
5 entr 5879 . . . . 5
64, 5mpan2 647 . . . 4
71onirri 3810 . . . . . . 7
8 disjsn 3129 . . . . . . 7
97, 8mpbir 198 . . . . . 6
10 unen 5908 . . . . . 6
119, 10mpanr2 660 . . . . 5
1211ex 419 . . . 4
136, 12sylan2 453 . . 3
14 df-2o 5536 . . . . 5
15 df-suc 3711 . . . . 5
1614, 15eqtri 1938 . . . 4
1716breq2i 3391 . . 3
1813, 17syl6ibr 216 . 2
19 en1 5892 . . 3
20 en1 5892 . . 3
21 unidm 2778 . . . . . . . . . . . . . 14
22 sneq 3094 . . . . . . . . . . . . . . 15
2322uneq2d 2789 . . . . . . . . . . . . . 14
2421, 23syl5reqr 1965 . . . . . . . . . . . . 13
25 vex 2329 . . . . . . . . . . . . . . 15
2625ensn1 5889 . . . . . . . . . . . . . 14
27 1sdom2 6069 . . . . . . . . . . . . . 14
28 ensdomtr 5951 . . . . . . . . . . . . . 14
2926, 27, 28mp2an 648 . . . . . . . . . . . . 13
3024, 29syl6eqbr 3420 . . . . . . . . . . . 12
31 sdomnen 5849 . . . . . . . . . . . 12
3230, 31syl 15 . . . . . . . . . . 11
3332necon2ai 2079 . . . . . . . . . 10
34 disjsn2 3131 . . . . . . . . . 10
3533, 34syl 15 . . . . . . . . 9
3635a1i 10 . . . . . . . 8
37 uneq12 2784 . . . . . . . . 9
3837breq1d 3393 . . . . . . . 8
39 ineq12 2821 . . . . . . . . 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 2634   cin 2635  c0 2904  csn 3083   class class class wbr 3383  con0 3705   csuc 3707  c1o 5528  c2o 5529   cen 5826   csdm 5828
This theorem is referenced by:  pr2nelem 6469  pm110.643 6562  isprm2lem 10020
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 3469  ax-sep 3479  ax-nul 3488  ax-pow 3524  ax-pr 3548  ax-un 3823
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 2328  df-dif 2639  df-un 2641  df-in 2643  df-ss 2647  df-pss 2649  df-nul 2905  df-pw 3072  df-sn 3089  df-pr 3090  df-tp 3091  df-op 3092  df-uni 3234  df-br 3384  df-opab 3438  df-tr 3453  df-eprel 3634  df-id 3637  df-po 3642  df-so 3656  df-fr 3676  df-we 3692  df-ord 3708  df-on 3709  df-suc 3711  df-xp 4035  df-rel 4036  df-cnv 4037  df-co 4038  df-dm 4039  df-rn 4040  df-res 4041  df-ima 4042  df-fun 4043  df-fn 4044  df-f 4045  df-f1 4046  df-fo 4047  df-f1o 4048  df-fv 4049  df-1o 5535  df-2o 5536  df-er 5673  df-en 5830  df-dom 5831  df-sdom 5832
Copyright terms: Public domain