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

Theorem pm54.43 6265
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 6242), so that their A e. 1 means, in our notation, A e. {x | (card` x) = 1o} which is the same as A ~~ 1o by pm54.43lem 6264. 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 6359 shows the derivation of 1+1=2 for cardinal numbers from this theorem.

Assertion
Ref Expression
pm54.43 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) <-> (A u. B) ~~ 2o))

Proof of Theorem pm54.43
StepHypRef Expression
1 1on 5384 . . . . . . 7 |- 1o e. On
21elexi 2346 . . . . . 6 |- 1o e. _V
32ensn1 5718 . . . . . 6 |- {1o} ~~ 1o
42, 3ensymi 5707 . . . . 5 |- 1o ~~ {1o}
5 entr 5708 . . . . 5 |- ((B ~~ 1o /\ 1o ~~ {1o}) -> B ~~ {1o})
64, 5mpan2 649 . . . 4 |- (B ~~ 1o -> B ~~ {1o})
71onirri 3778 . . . . . . 7 |- -. 1o e. 1o
8 disjsn 3115 . . . . . . 7 |- ((1o i^i {1o}) = (/) <-> -. 1o e. 1o)
97, 8mpbir 199 . . . . . 6 |- (1o i^i {1o}) = (/)
10 unen 5732 . . . . . 6 |- (((A ~~ 1o /\ B ~~ {1o}) /\ ((A i^i B) = (/) /\ (1o i^i {1o}) = (/))) -> (A u. B) ~~ (1o u. {1o}))
119, 10mpanr2 662 . . . . 5 |- (((A ~~ 1o /\ B ~~ {1o}) /\ (A i^i B) = (/)) -> (A u. B) ~~ (1o u. {1o}))
1211ex 422 . . . 4 |- ((A ~~ 1o /\ B ~~ {1o}) -> ((A i^i B) = (/) -> (A u. B) ~~ (1o u. {1o})))
136, 12sylan2 457 . . 3 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) -> (A u. B) ~~ (1o u. {1o})))
14 df-2o 5378 . . . . 5 |- 2o = suc 1o
15 df-suc 3680 . . . . 5 |- suc 1o = (1o u. {1o})
1614, 15eqtri 1952 . . . 4 |- 2o = (1o u. {1o})
1716breq2i 3362 . . 3 |- ((A u. B) ~~ 2o <-> (A u. B) ~~ (1o u. {1o}))
1813, 17syl6ibr 218 . 2 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) -> (A u. B) ~~ 2o))
19 en1 5721 . . 3 |- (A ~~ 1o <-> E.x A = {x})
20 en1 5721 . . 3 |- (B ~~ 1o <-> E.y B = {y})
21 unidm 2776 . . . . . . . . . . . . . 14 |- ({x} u. {x}) = {x}
22 sneq 3082 . . . . . . . . . . . . . . 15 |- (x = y -> {x} = {y})
2322uneq2d 2787 . . . . . . . . . . . . . 14 |- (x = y -> ({x} u. {x}) = ({x} u. {y}))
2421, 23syl5reqr 1979 . . . . . . . . . . . . 13 |- (x = y -> ({x} u. {y}) = {x})
25 vex 2340 . . . . . . . . . . . . . . 15 |- x e. _V
2625ensn1 5718 . . . . . . . . . . . . . 14 |- {x} ~~ 1o
27 1sdom2 5884 . . . . . . . . . . . . . 14 |- 1o ~< 2o
28 ensdomtr 5772 . . . . . . . . . . . . . 14 |- (({x} ~~ 1o /\ 1o ~< 2o) -> {x} ~< 2o)
2926, 27, 28mp2an 650 . . . . . . . . . . . . 13 |- {x} ~< 2o
3024, 29syl6eqbr 3391 . . . . . . . . . . . 12 |- (x = y -> ({x} u. {y}) ~< 2o)
31 sdomnen 5678 . . . . . . . . . . . 12 |- (({x} u. {y}) ~< 2o -> -. ({x} u. {y}) ~~ 2o)
3230, 31syl 14 . . . . . . . . . . 11 |- (x = y -> -. ({x} u. {y}) ~~ 2o)
3332necon2ai 2093 . . . . . . . . . 10 |- (({x} u. {y}) ~~ 2o -> x =/= y)
34 disjsn2 3116 . . . . . . . . . 10 |- (x =/= y -> ({x} i^i {y}) = (/))
3533, 34syl 14 . . . . . . . . 9 |- (({x} u. {y}) ~~ 2o -> ({x} i^i {y}) = (/))
3635a1i 10 . . . . . . . 8 |- ((A = {x} /\ B = {y}) -> (({x} u. {y}) ~~ 2o -> ({x} i^i {y}) = (/)))
37 uneq12 2782 . . . . . . . . 9 |- ((A = {x} /\ B = {y}) -> (A u. B) = ({x} u. {y}))
3837breq1d 3364 . . . . . . . 8 |- ((A = {x} /\ B = {y}) -> ((A u. B) ~~ 2o <-> ({x} u. {y}) ~~ 2o))
39 ineq12 2819 . . . . . . . . 9 |- ((A = {x} /\ B = {y}) -> (A i^i B) = ({x} i^i {y}))
4039eqeq1d 1940 . . . . . . . 8 |- ((A = {x} /\ B = {y}) -> ((A i^i B) = (/) <-> ({x} i^i {y}) = (/)))
4136, 38, 403imtr4d 259 . . . . . . 7 |- ((A = {x} /\ B = {y}) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
4241ex 422 . . . . . 6 |- (A = {x} -> (B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
4342exlimdv 1649 . . . . 5 |- (A = {x} -> (E.y B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
4443exlimiv 1732 . . . 4 |- (E.x A = {x} -> (E.y B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
4544imp 417 . . 3 |- ((E.x A = {x} /\ E.y B = {y}) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
4619, 20, 45syl2anb 462 . 2 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
4718, 46impbid 181 1 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) <-> (A u. B) ~~ 2o))
Colors of variables: wff set class
Syntax hints:  -. wn 3   -> wi 4   <-> wb 174   /\ wa 357  E.wex 1349   = wceq 1428   e. wcel 1430   =/= wne 2050   u. cun 2634   i^i cin 2635  (/)c0 2900  {csn 3071   class class class wbr 3354  Oncon0 3674  suc csuc 3676  1oc1o 5370  2oc2o 5371   ~~ cen 5655   ~< csdm 5657
This theorem is referenced by:  pr2nelem 6266  pm110.643 6359  isprm2lem 9711
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1345  ax-6 1346  ax-7 1347  ax-gen 1348  ax-8 1432  ax-10 1433  ax-11 1434  ax-12 1435  ax-13 1436  ax-14 1437  ax-17 1444  ax-9 1459  ax-4 1465  ax-16 1643  ax-ext 1914  ax-rep 3440  ax-sep 3450  ax-nul 3459  ax-pow 3495  ax-pr 3519  ax-un 3791
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 916  df-3an 917  df-tru 1323  df-ex 1350  df-sb 1605  df-eu 1832  df-mo 1833  df-clab 1920  df-cleq 1925  df-clel 1928  df-ne 2052  df-ral 2145  df-rex 2146  df-reu 2147  df-rab 2148  df-v 2339  df-dif 2639  df-un 2641  df-in 2643  df-ss 2645  df-pss 2647  df-nul 2901  df-pw 3060  df-sn 3077  df-pr 3078  df-tp 3079  df-op 3080  df-uni 3210  df-br 3355  df-opab 3409  df-tr 3424  df-eprel 3604  df-id 3607  df-po 3612  df-so 3626  df-fr 3645  df-we 3661  df-ord 3677  df-on 3678  df-suc 3680  df-xp 4001  df-rel 4002  df-cnv 4003  df-co 4004  df-dm 4005  df-rn 4006  df-res 4007  df-ima 4008  df-fun 4009  df-fn 4010  df-f 4011  df-f1 4012  df-fo 4013  df-f1o 4014  df-fv 4015  df-1o 5377  df-2o 5378  df-er 5514  df-en 5659  df-dom 5660  df-sdom 5661
Copyright terms: Public domain