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

Theorem pm54.43 6287
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 6264), so that their means, in our notation, which is the same as by pm54.43lem 6286. 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 6381 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 5407 . . . . . . 7
21elexi 2344 . . . . . 6
32ensn1 5741 . . . . . 6
42, 3ensymi 5730 . . . . 5
5 entr 5731 . . . . 5
64, 5mpan2 651 . . . 4
71onirri 3782 . . . . . . 7
8 disjsn 3118 . . . . . . 7
97, 8mpbir 198 . . . . . 6
10 unen 5755 . . . . . 6
119, 10mpanr2 664 . . . . 5
1211ex 423 . . . 4
136, 12sylan2 457 . . 3
14 df-2o 5401 . . . . 5
15 df-suc 3684 . . . . 5
1614, 15eqtri 1949 . . . 4
1716breq2i 3366 . . 3
1813, 17syl6ibr 217 . 2
19 en1 5744 . . 3
20 en1 5744 . . 3
21 unidm 2774 . . . . . . . . . . . . . 14
22 sneq 3085 . . . . . . . . . . . . . . 15
2322uneq2d 2785 . . . . . . . . . . . . . 14
2421, 23syl5reqr 1976 . . . . . . . . . . . . 13
25 vex 2338 . . . . . . . . . . . . . . 15
2625ensn1 5741 . . . . . . . . . . . . . 14
27 1sdom2 5907 . . . . . . . . . . . . . 14
28 ensdomtr 5795 . . . . . . . . . . . . . 14
2926, 27, 28mp2an 652 . . . . . . . . . . . . 13
3024, 29syl6eqbr 3395 . . . . . . . . . . . 12
31 sdomnen 5701 . . . . . . . . . . . 12
3230, 31syl 14 . . . . . . . . . . 11
3332necon2ai 2090 . . . . . . . . . 10
34 disjsn2 3120 . . . . . . . . . 10
3533, 34syl 14 . . . . . . . . 9
3635a1i 10 . . . . . . . 8
37 uneq12 2780 . . . . . . . . 9
3837breq1d 3368 . . . . . . . 8
39 ineq12 2817 . . . . . . . . 9
4039eqeq1d 1937 . . . . . . . 8
4136, 38, 403imtr4d 258 . . . . . . 7
4241ex 423 . . . . . 6
4342exlimdv 1646 . . . . 5
4443exlimiv 1729 . . . 4
4544imp 418 . . 3
4619, 20, 45syl2anb 462 . 2
4718, 46impbid 181 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   wb 174   wa 360  wex 1346   wceq 1425   wcel 1427   wne 2047   cun 2632   cin 2633  c0 2899  csn 3074   class class class wbr 3358  con0 3678   csuc 3680  c1o 5393  c2o 5394   cen 5678   csdm 5680
This theorem is referenced by:  pr2nelem 6288  pm110.643 6381  isprm2lem 9736
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1342  ax-6 1343  ax-7 1344  ax-gen 1345  ax-8 1429  ax-10 1430  ax-11 1431  ax-12 1432  ax-13 1433  ax-14 1434  ax-17 1441  ax-9 1456  ax-4 1462  ax-16 1640  ax-ext 1911  ax-rep 3444  ax-sep 3454  ax-nul 3463  ax-pow 3499  ax-pr 3523  ax-un 3795
This theorem depends on definitions:  df-bi 175  df-or 361  df-an 362  df-3or 913  df-3an 914  df-tru 1320  df-ex 1347  df-sb 1602  df-eu 1829  df-mo 1830  df-clab 1917  df-cleq 1922  df-clel 1925  df-ne 2049  df-ral 2142  df-rex 2143  df-reu 2144  df-rab 2145  df-v 2337  df-dif 2637  df-un 2639  df-in 2641  df-ss 2643  df-pss 2645  df-nul 2900  df-pw 3063  df-sn 3080  df-pr 3081  df-tp 3082  df-op 3083  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 3649  df-we 3665  df-ord 3681  df-on 3682  df-suc 3684  df-xp 4005  df-rel 4006  df-cnv 4007  df-co 4008  df-dm 4009  df-rn 4010  df-res 4011  df-ima 4012  df-fun 4013  df-fn 4014  df-f 4015  df-f1 4016  df-fo 4017  df-f1o 4018  df-fv 4019  df-1o 5400  df-2o 5401  df-er 5537  df-en 5682  df-dom 5683  df-sdom 5684
Copyright terms: Public domain