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

Theorem pm54.43 6281
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 6258), 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 6280. 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 6384 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 5400 . . . . . . 7 |- 1o e. On
21elexi 2367 . . . . . 6 |- 1o e. _V
32ensn1 5734 . . . . . 6 |- {1o} ~~ 1o
42, 3ensymi 5723 . . . . 5 |- 1o ~~ {1o}
5 entr 5724 . . . . 5 |- ((B ~~ 1o /\ 1o ~~ {1o}) -> B ~~ {1o})
64, 5mpan2 669 . . . 4 |- (B ~~ 1o -> B ~~ {1o})
71onirri 3795 . . . . . . 7 |- -. 1o e. 1o
8 disjsn 3134 . . . . . . 7 |- ((1o i^i {1o}) = (/) <-> -. 1o e. 1o)
97, 8mpbir 213 . . . . . 6 |- (1o i^i {1o}) = (/)
10 unen 5748 . . . . . 6 |- (((A ~~ 1o /\ B ~~ {1o}) /\ ((A i^i B) = (/) /\ (1o i^i {1o}) = (/))) -> (A u. B) ~~ (1o u. {1o}))
119, 10mpanr2 682 . . . . 5 |- (((A ~~ 1o /\ B ~~ {1o}) /\ (A i^i B) = (/)) -> (A u. B) ~~ (1o u. {1o}))
1211ex 442 . . . 4 |- ((A ~~ 1o /\ B ~~ {1o}) -> ((A i^i B) = (/) -> (A u. B) ~~ (1o u. {1o})))
136, 12sylan2 477 . . 3 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) -> (A u. B) ~~ (1o u. {1o})))
14 df-2o 5394 . . . . 5 |- 2o = suc 1o
15 df-suc 3697 . . . . 5 |- suc 1o = (1o u. {1o})
1614, 15eqtri 1973 . . . 4 |- 2o = (1o u. {1o})
1716breq2i 3381 . . 3 |- ((A u. B) ~~ 2o <-> (A u. B) ~~ (1o u. {1o}))
1813, 17syl6ibr 232 . 2 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) -> (A u. B) ~~ 2o))
19 en1 5737 . . 3 |- (A ~~ 1o <-> E.x A = {x})
20 en1 5737 . . 3 |- (B ~~ 1o <-> E.y B = {y})
21 unidm 2797 . . . . . . . . . . . . . 14 |- ({x} u. {x}) = {x}
22 sneq 3101 . . . . . . . . . . . . . . 15 |- (x = y -> {x} = {y})
2322uneq2d 2808 . . . . . . . . . . . . . 14 |- (x = y -> ({x} u. {x}) = ({x} u. {y}))
2421, 23syl5reqr 2000 . . . . . . . . . . . . 13 |- (x = y -> ({x} u. {y}) = {x})
25 vex 2361 . . . . . . . . . . . . . . 15 |- x e. _V
2625ensn1 5734 . . . . . . . . . . . . . 14 |- {x} ~~ 1o
27 1sdom2 5900 . . . . . . . . . . . . . 14 |- 1o ~< 2o
28 ensdomtr 5788 . . . . . . . . . . . . . 14 |- (({x} ~~ 1o /\ 1o ~< 2o) -> {x} ~< 2o)
2926, 27, 28mp2an 670 . . . . . . . . . . . . 13 |- {x} ~< 2o
3024, 29syl6eqbr 3410 . . . . . . . . . . . 12 |- (x = y -> ({x} u. {y}) ~< 2o)
31 sdomnen 5694 . . . . . . . . . . . 12 |- (({x} u. {y}) ~< 2o -> -. ({x} u. {y}) ~~ 2o)
3230, 31syl 14 . . . . . . . . . . 11 |- (x = y -> -. ({x} u. {y}) ~~ 2o)
3332necon2ai 2114 . . . . . . . . . 10 |- (({x} u. {y}) ~~ 2o -> x =/= y)
34 disjsn2 3135 . . . . . . . . . 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 2803 . . . . . . . . 9 |- ((A = {x} /\ B = {y}) -> (A u. B) = ({x} u. {y}))
3837breq1d 3383 . . . . . . . 8 |- ((A = {x} /\ B = {y}) -> ((A u. B) ~~ 2o <-> ({x} u. {y}) ~~ 2o))
39 ineq12 2840 . . . . . . . . 9 |- ((A = {x} /\ B = {y}) -> (A i^i B) = ({x} i^i {y}))
4039eqeq1d 1961 . . . . . . . 8 |- ((A = {x} /\ B = {y}) -> ((A i^i B) = (/) <-> ({x} i^i {y}) = (/)))
4136, 38, 403imtr4d 273 . . . . . . 7 |- ((A = {x} /\ B = {y}) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
4241ex 442 . . . . . 6 |- (A = {x} -> (B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
4342exlimdv 1670 . . . . 5 |- (A = {x} -> (E.y B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
4443exlimiv 1753 . . . 4 |- (E.x A = {x} -> (E.y B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
4544imp 437 . . 3 |- ((E.x A = {x} /\ E.y B = {y}) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
4619, 20, 45syl2anb 482 . 2 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
4718, 46impbid 191 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 184   /\ wa 377  E.wex 1371   = wceq 1449   e. wcel 1451   =/= wne 2071   u. cun 2655   i^i cin 2656  (/)c0 2921  {csn 3092   class class class wbr 3373  Oncon0 3691  suc csuc 3693  1oc1o 5386  2oc2o 5387   ~~ cen 5671   ~< csdm 5673
This theorem is referenced by:  pr2nelem 6282  pm110.643 6384  isprm2lem 9667
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1367  ax-6 1368  ax-7 1369  ax-gen 1370  ax-8 1453  ax-10 1454  ax-11 1455  ax-12 1456  ax-13 1457  ax-14 1458  ax-17 1465  ax-9 1480  ax-4 1486  ax-16 1664  ax-ext 1935  ax-rep 3459  ax-sep 3469  ax-nul 3478  ax-pow 3514  ax-pr 3538  ax-un 3808
This theorem depends on definitions:  df-bi 185  df-or 378  df-an 379  df-3or 938  df-3an 939  df-tru 1345  df-ex 1372  df-sb 1626  df-eu 1853  df-mo 1854  df-clab 1941  df-cleq 1946  df-clel 1949  df-ne 2073  df-ral 2166  df-rex 2167  df-reu 2168  df-rab 2169  df-v 2360  df-dif 2660  df-un 2662  df-in 2664  df-ss 2666  df-pss 2668  df-nul 2922  df-pw 3081  df-sn 3096  df-pr 3097  df-tp 3099  df-op 3100  df-uni 3229  df-br 3374  df-opab 3428  df-tr 3443  df-eprel 3621  df-id 3624  df-po 3629  df-so 3643  df-fr 3662  df-we 3678  df-ord 3694  df-on 3695  df-suc 3697  df-xp 4018  df-rel 4019  df-cnv 4020  df-co 4021  df-dm 4022  df-rn 4023  df-res 4024  df-ima 4025  df-fun 4026  df-fn 4027  df-f 4028  df-f1 4029  df-fo 4030  df-f1o 4031  df-fv 4032  df-1o 5393  df-2o 5394  df-er 5530  df-en 5675  df-dom 5676  df-sdom 5677
Copyright terms: Public domain