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

Theorem pm54.43 6288
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 6265), 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 6287. 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 6382 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 5408 . . . . . . 7 |- 1o e. On
21elexi 2352 . . . . . 6 |- 1o e. _V
32ensn1 5742 . . . . . 6 |- {1o} ~~ 1o
42, 3ensymi 5731 . . . . 5 |- 1o ~~ {1o}
5 entr 5732 . . . . 5 |- ((B ~~ 1o /\ 1o ~~ {1o}) -> B ~~ {1o})
64, 5mpan2 655 . . . 4 |- (B ~~ 1o -> B ~~ {1o})
71onirri 3787 . . . . . . 7 |- -. 1o e. 1o
8 disjsn 3123 . . . . . . 7 |- ((1o i^i {1o}) = (/) <-> -. 1o e. 1o)
97, 8mpbir 198 . . . . . 6 |- (1o i^i {1o}) = (/)
10 unen 5756 . . . . . 6 |- (((A ~~ 1o /\ B ~~ {1o}) /\ ((A i^i B) = (/) /\ (1o i^i {1o}) = (/))) -> (A u. B) ~~ (1o u. {1o}))
119, 10mpanr2 668 . . . . 5 |- (((A ~~ 1o /\ B ~~ {1o}) /\ (A i^i B) = (/)) -> (A u. B) ~~ (1o u. {1o}))
1211ex 426 . . . 4 |- ((A ~~ 1o /\ B ~~ {1o}) -> ((A i^i B) = (/) -> (A u. B) ~~ (1o u. {1o})))
136, 12sylan2 461 . . 3 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) -> (A u. B) ~~ (1o u. {1o})))
14 df-2o 5402 . . . . 5 |- 2o = suc 1o
15 df-suc 3689 . . . . 5 |- suc 1o = (1o u. {1o})
1614, 15eqtri 1958 . . . 4 |- 2o = (1o u. {1o})
1716breq2i 3371 . . 3 |- ((A u. B) ~~ 2o <-> (A u. B) ~~ (1o u. {1o}))
1813, 17syl6ibr 217 . 2 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) -> (A u. B) ~~ 2o))
19 en1 5745 . . 3 |- (A ~~ 1o <-> E.x A = {x})
20 en1 5745 . . 3 |- (B ~~ 1o <-> E.y B = {y})
21 unidm 2782 . . . . . . . . . . . . . 14 |- ({x} u. {x}) = {x}
22 sneq 3090 . . . . . . . . . . . . . . 15 |- (x = y -> {x} = {y})
2322uneq2d 2793 . . . . . . . . . . . . . 14 |- (x = y -> ({x} u. {x}) = ({x} u. {y}))
2421, 23syl5reqr 1985 . . . . . . . . . . . . 13 |- (x = y -> ({x} u. {y}) = {x})
25 vex 2346 . . . . . . . . . . . . . . 15 |- x e. _V
2625ensn1 5742 . . . . . . . . . . . . . 14 |- {x} ~~ 1o
27 1sdom2 5908 . . . . . . . . . . . . . 14 |- 1o ~< 2o
28 ensdomtr 5796 . . . . . . . . . . . . . 14 |- (({x} ~~ 1o /\ 1o ~< 2o) -> {x} ~< 2o)
2926, 27, 28mp2an 656 . . . . . . . . . . . . 13 |- {x} ~< 2o
3024, 29syl6eqbr 3400 . . . . . . . . . . . 12 |- (x = y -> ({x} u. {y}) ~< 2o)
31 sdomnen 5702 . . . . . . . . . . . 12 |- (({x} u. {y}) ~< 2o -> -. ({x} u. {y}) ~~ 2o)
3230, 31syl 14 . . . . . . . . . . 11 |- (x = y -> -. ({x} u. {y}) ~~ 2o)
3332necon2ai 2099 . . . . . . . . . 10 |- (({x} u. {y}) ~~ 2o -> x =/= y)
34 disjsn2 3125 . . . . . . . . . 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 2788 . . . . . . . . 9 |- ((A = {x} /\ B = {y}) -> (A u. B) = ({x} u. {y}))
3837breq1d 3373 . . . . . . . 8 |- ((A = {x} /\ B = {y}) -> ((A u. B) ~~ 2o <-> ({x} u. {y}) ~~ 2o))
39 ineq12 2825 . . . . . . . . 9 |- ((A = {x} /\ B = {y}) -> (A i^i B) = ({x} i^i {y}))
4039eqeq1d 1946 . . . . . . . 8 |- ((A = {x} /\ B = {y}) -> ((A i^i B) = (/) <-> ({x} i^i {y}) = (/)))
4136, 38, 403imtr4d 258 . . . . . . 7 |- ((A = {x} /\ B = {y}) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
4241ex 426 . . . . . 6 |- (A = {x} -> (B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
4342exlimdv 1655 . . . . 5 |- (A = {x} -> (E.y B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
4443exlimiv 1738 . . . 4 |- (E.x A = {x} -> (E.y B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
4544imp 421 . . 3 |- ((E.x A = {x} /\ E.y B = {y}) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
4619, 20, 45syl2anb 466 . 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 361  E.wex 1355   = wceq 1434   e. wcel 1436   =/= wne 2056   u. cun 2640   i^i cin 2641  (/)c0 2906  {csn 3079   class class class wbr 3363  Oncon0 3683  suc csuc 3685  1oc1o 5394  2oc2o 5395   ~~ cen 5679   ~< csdm 5681
This theorem is referenced by:  pr2nelem 6289  pm110.643 6382  isprm2lem 9734
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1351  ax-6 1352  ax-7 1353  ax-gen 1354  ax-8 1438  ax-10 1439  ax-11 1440  ax-12 1441  ax-13 1442  ax-14 1443  ax-17 1450  ax-9 1465  ax-4 1471  ax-16 1649  ax-ext 1920  ax-rep 3449  ax-sep 3459  ax-nul 3468  ax-pow 3504  ax-pr 3528  ax-un 3800
This theorem depends on definitions:  df-bi 175  df-or 362  df-an 363  df-3or 922  df-3an 923  df-tru 1329  df-ex 1356  df-sb 1611  df-eu 1838  df-mo 1839  df-clab 1926  df-cleq 1931  df-clel 1934  df-ne 2058  df-ral 2151  df-rex 2152  df-reu 2153  df-rab 2154  df-v 2345  df-dif 2645  df-un 2647  df-in 2649  df-ss 2651  df-pss 2653  df-nul 2907  df-pw 3068  df-sn 3085  df-pr 3086  df-tp 3087  df-op 3088  df-uni 3219  df-br 3364  df-opab 3418  df-tr 3433  df-eprel 3613  df-id 3616  df-po 3621  df-so 3635  df-fr 3654  df-we 3670  df-ord 3686  df-on 3687  df-suc 3689  df-xp 4010  df-rel 4011  df-cnv 4012  df-co 4013  df-dm 4014  df-rn 4015  df-res 4016  df-ima 4017  df-fun 4018  df-fn 4019  df-f 4020  df-f1 4021  df-fo 4022  df-f1o 4023  df-fv 4024  df-1o 5401  df-2o 5402  df-er 5538  df-en 5683  df-dom 5684  df-sdom 5685
Copyright terms: Public domain