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

Theorem pm54.43 6364
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 6340), so that their means, in our notation, which is the same as by pm54.43lem 6363. 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 6458 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 5468 . . . . . . 7
21elexi 2331 . . . . . 6
32ensn1 5809 . . . . . 6
42, 3ensymi 5798 . . . . 5
5 entr 5799 . . . . 5
64, 5mpan2 646 . . . 4
71onirri 3784 . . . . . . 7
8 disjsn 3117 . . . . . . 7
97, 8mpbir 197 . . . . . 6
10 unen 5825 . . . . . 6
119, 10mpanr2 659 . . . . 5
1211ex 418 . . . 4
136, 12sylan2 452 . . 3
14 df-2o 5462 . . . . 5
15 df-suc 3685 . . . . 5
1614, 15eqtri 1937 . . . 4
1716breq2i 3366 . . 3
1813, 17syl6ibr 215 . 2
19 en1 5812 . . 3
20 en1 5812 . . 3
21 unidm 2772 . . . . . . . . . . . . . 14
22 sneq 3084 . . . . . . . . . . . . . . 15
2322uneq2d 2783 . . . . . . . . . . . . . 14
2421, 23syl5reqr 1964 . . . . . . . . . . . . 13
25 vex 2325 . . . . . . . . . . . . . . 15
2625ensn1 5809 . . . . . . . . . . . . . 14
27 1sdom2 5978 . . . . . . . . . . . . . 14
28 ensdomtr 5866 . . . . . . . . . . . . . 14
2926, 27, 28mp2an 647 . . . . . . . . . . . . 13
3024, 29syl6eqbr 3395 . . . . . . . . . . . 12
31 sdomnen 5769 . . . . . . . . . . . 12
3230, 31syl 14 . . . . . . . . . . 11
3332necon2ai 2077 . . . . . . . . . 10
34 disjsn2 3119 . . . . . . . . . 10
3533, 34syl 14 . . . . . . . . 9
3635a1i 10 . . . . . . . 8
37 uneq12 2778 . . . . . . . . 9
3837breq1d 3368 . . . . . . . 8
39 ineq12 2815 . . . . . . . . 9
4039eqeq1d 1925 . . . . . . . 8
4136, 38, 403imtr4d 256 . . . . . . 7
4241ex 418 . . . . . 6
4342exlimdv 1634 . . . . 5
4443exlimiv 1717 . . . 4
4544imp 413 . . 3
4619, 20, 45syl2anb 457 . 2
4718, 46impbid 180 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   wb 173   wa 356  wex 1334   wceq 1413   wcel 1415   wne 2034   cun 2630   cin 2631  c0 2898  csn 3073   class class class wbr 3358  con0 3679   csuc 3681  c1o 5454  c2o 5455   cen 5746   csdm 5748
This theorem is referenced by:  pr2nelem 6365  pm110.643 6458  isprm2lem 9855
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1330  ax-6 1331  ax-7 1332  ax-gen 1333  ax-8 1417  ax-10 1418  ax-11 1419  ax-12 1420  ax-13 1421  ax-14 1422  ax-17 1429  ax-9 1444  ax-4 1450  ax-16 1628  ax-ext 1899  ax-rep 3444  ax-sep 3454  ax-nul 3463  ax-pow 3499  ax-pr 3523  ax-un 3797
This theorem depends on definitions:  df-bi 174  df-or 357  df-an 358  df-3or 899  df-3an 900  df-tru 1308  df-ex 1335  df-sb 1590  df-eu 1817  df-mo 1818  df-clab 1905  df-cleq 1910  df-clel 1913  df-ne 2036  df-ral 2129  df-rex 2130  df-reu 2131  df-rab 2132  df-v 2324  df-dif 2635  df-un 2637  df-in 2639  df-ss 2641  df-pss 2643  df-nul 2899  df-pw 3062  df-sn 3079  df-pr 3080  df-tp 3081  df-op 3082  df-uni 3214  df-br 3359  df-opab 3413  df-tr 3428  df-eprel 3608  df-id 3611  df-po 3616  df-so 3630  df-fr 3650  df-we 3666  df-ord 3682  df-on 3683  df-suc 3685  df-xp 4009  df-rel 4010  df-cnv 4011  df-co 4012  df-dm 4013  df-rn 4014  df-res 4015  df-ima 4016  df-fun 4017  df-fn 4018  df-f 4019  df-f1 4020  df-fo 4021  df-f1o 4022  df-fv 4023  df-1o 5461  df-2o 5462  df-er 5598  df-en 5750  df-dom 5751  df-sdom 5752
Copyright terms: Public domain