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

Theorem pm54.43 6282
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 6259), 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 6281. 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 6385 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 5403 . . . . . . 7 |- 1o e. On
21elexi 2375 . . . . . 6 |- 1o e. _V
32ensn1 5737 . . . . . 6 |- {1o} ~~ 1o
42, 3ensymi 5726 . . . . 5 |- 1o ~~ {1o}
5 entr 5727 . . . . 5 |- ((B ~~ 1o /\ 1o ~~ {1o}) -> B ~~ {1o})
64, 5mpan2 678 . . . 4 |- (B ~~ 1o -> B ~~ {1o})
71onirri 3801 . . . . . . 7 |- -. 1o e. 1o
8 disjsn 3140 . . . . . . 7 |- ((1o i^i {1o}) = (/) <-> -. 1o e. 1o)
97, 8mpbir 218 . . . . . 6 |- (1o i^i {1o}) = (/)
10 unen 5751 . . . . . 6 |- (((A ~~ 1o /\ B ~~ {1o}) /\ ((A i^i B) = (/) /\ (1o i^i {1o}) = (/))) -> (A u. B) ~~ (1o u. {1o}))
119, 10mpanr2 691 . . . . 5 |- (((A ~~ 1o /\ B ~~ {1o}) /\ (A i^i B) = (/)) -> (A u. B) ~~ (1o u. {1o}))
1211ex 448 . . . 4 |- ((A ~~ 1o /\ B ~~ {1o}) -> ((A i^i B) = (/) -> (A u. B) ~~ (1o u. {1o})))
136, 12sylan2 483 . . 3 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) -> (A u. B) ~~ (1o u. {1o})))
14 df-2o 5397 . . . . 5 |- 2o = suc 1o
15 df-suc 3703 . . . . 5 |- suc 1o = (1o u. {1o})
1614, 15eqtri 1981 . . . 4 |- 2o = (1o u. {1o})
1716breq2i 3387 . . 3 |- ((A u. B) ~~ 2o <-> (A u. B) ~~ (1o u. {1o}))
1813, 17syl6ibr 237 . 2 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) -> (A u. B) ~~ 2o))
19 en1 5740 . . 3 |- (A ~~ 1o <-> E.x A = {x})
20 en1 5740 . . 3 |- (B ~~ 1o <-> E.y B = {y})
21 unidm 2803 . . . . . . . . . . . . . 14 |- ({x} u. {x}) = {x}
22 sneq 3107 . . . . . . . . . . . . . . 15 |- (x = y -> {x} = {y})
2322uneq2d 2814 . . . . . . . . . . . . . 14 |- (x = y -> ({x} u. {x}) = ({x} u. {y}))
2421, 23syl5reqr 2008 . . . . . . . . . . . . 13 |- (x = y -> ({x} u. {y}) = {x})
25 vex 2369 . . . . . . . . . . . . . . 15 |- x e. _V
2625ensn1 5737 . . . . . . . . . . . . . 14 |- {x} ~~ 1o
27 1sdom2 5903 . . . . . . . . . . . . . 14 |- 1o ~< 2o
28 ensdomtr 5791 . . . . . . . . . . . . . 14 |- (({x} ~~ 1o /\ 1o ~< 2o) -> {x} ~< 2o)
2926, 27, 28mp2an 679 . . . . . . . . . . . . 13 |- {x} ~< 2o
3024, 29syl6eqbr 3416 . . . . . . . . . . . 12 |- (x = y -> ({x} u. {y}) ~< 2o)
31 sdomnen 5697 . . . . . . . . . . . 12 |- (({x} u. {y}) ~< 2o -> -. ({x} u. {y}) ~~ 2o)
3230, 31syl 14 . . . . . . . . . . 11 |- (x = y -> -. ({x} u. {y}) ~~ 2o)
3332necon2ai 2122 . . . . . . . . . 10 |- (({x} u. {y}) ~~ 2o -> x =/= y)
34 disjsn2 3141 . . . . . . . . . 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 2809 . . . . . . . . 9 |- ((A = {x} /\ B = {y}) -> (A u. B) = ({x} u. {y}))
3837breq1d 3389 . . . . . . . 8 |- ((A = {x} /\ B = {y}) -> ((A u. B) ~~ 2o <-> ({x} u. {y}) ~~ 2o))
39 ineq12 2846 . . . . . . . . 9 |- ((A = {x} /\ B = {y}) -> (A i^i B) = ({x} i^i {y}))
4039eqeq1d 1969 . . . . . . . 8 |- ((A = {x} /\ B = {y}) -> ((A i^i B) = (/) <-> ({x} i^i {y}) = (/)))
4136, 38, 403imtr4d 278 . . . . . . 7 |- ((A = {x} /\ B = {y}) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
4241ex 448 . . . . . 6 |- (A = {x} -> (B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
4342exlimdv 1678 . . . . 5 |- (A = {x} -> (E.y B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
4443exlimiv 1761 . . . 4 |- (E.x A = {x} -> (E.y B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
4544imp 443 . . 3 |- ((E.x A = {x} /\ E.y B = {y}) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
4619, 20, 45syl2anb 488 . 2 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
4718, 46impbid 196 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 189   /\ wa 382  E.wex 1380   = wceq 1457   e. wcel 1459   =/= wne 2079   u. cun 2661   i^i cin 2662  (/)c0 2927  {csn 3098   class class class wbr 3379  Oncon0 3697  suc csuc 3699  1oc1o 5389  2oc2o 5390   ~~ cen 5674   ~< csdm 5676
This theorem is referenced by:  pr2nelem 6283  pm110.643 6385  isprm2lem 9651
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1376  ax-6 1377  ax-7 1378  ax-gen 1379  ax-8 1461  ax-10 1462  ax-11 1463  ax-12 1464  ax-13 1465  ax-14 1466  ax-17 1473  ax-9 1488  ax-4 1494  ax-16 1672  ax-ext 1943  ax-rep 3465  ax-sep 3475  ax-nul 3484  ax-pow 3520  ax-pr 3544  ax-un 3814
This theorem depends on definitions:  df-bi 190  df-or 383  df-an 384  df-3or 947  df-3an 948  df-tru 1354  df-ex 1381  df-sb 1634  df-eu 1861  df-mo 1862  df-clab 1949  df-cleq 1954  df-clel 1957  df-ne 2081  df-ral 2174  df-rex 2175  df-reu 2176  df-rab 2177  df-v 2368  df-dif 2666  df-un 2668  df-in 2670  df-ss 2672  df-pss 2674  df-nul 2928  df-pw 3087  df-sn 3102  df-pr 3103  df-tp 3105  df-op 3106  df-uni 3235  df-br 3380  df-opab 3434  df-tr 3449  df-eprel 3627  df-id 3630  df-po 3635  df-so 3649  df-fr 3668  df-we 3684  df-ord 3700  df-on 3701  df-suc 3703  df-xp 4022  df-rel 4023  df-cnv 4024  df-co 4025  df-dm 4026  df-rn 4027  df-res 4028  df-ima 4029  df-fun 4030  df-fn 4031  df-f 4032  df-f1 4033  df-fo 4034  df-f1o 4035  df-fv 4036  df-1o 5396  df-2o 5397  df-er 5533  df-en 5678  df-dom 5679  df-sdom 5680
Copyright terms: Public domain