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

Theorem pm54.43 6249
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 6226), 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 6248. 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 6352 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 5370 . . . . . . 7 |- 1o e. On
21elexi 2374 . . . . . 6 |- 1o e. _V
32ensn1 5704 . . . . . 6 |- {1o} ~~ 1o
42, 3ensymi 5693 . . . . 5 |- 1o ~~ {1o}
5 entr 5694 . . . . 5 |- ((B ~~ 1o /\ 1o ~~ {1o}) -> B ~~ {1o})
64, 5mpan2 678 . . . 4 |- (B ~~ 1o -> B ~~ {1o})
71onirri 3800 . . . . . . 7 |- -. 1o e. 1o
8 disjsn 3139 . . . . . . 7 |- ((1o i^i {1o}) = (/) <-> -. 1o e. 1o)
97, 8mpbir 218 . . . . . 6 |- (1o i^i {1o}) = (/)
10 unen 5718 . . . . . 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 5364 . . . . 5 |- 2o = suc 1o
15 df-suc 3702 . . . . 5 |- suc 1o = (1o u. {1o})
1614, 15eqtri 1980 . . . 4 |- 2o = (1o u. {1o})
1716breq2i 3386 . . 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 5707 . . 3 |- (A ~~ 1o <-> E.x A = {x})
20 en1 5707 . . 3 |- (B ~~ 1o <-> E.y B = {y})
21 unidm 2802 . . . . . . . . . . . . . 14 |- ({x} u. {x}) = {x}
22 sneq 3106 . . . . . . . . . . . . . . 15 |- (x = y -> {x} = {y})
2322uneq2d 2813 . . . . . . . . . . . . . 14 |- (x = y -> ({x} u. {x}) = ({x} u. {y}))
2421, 23syl5reqr 2007 . . . . . . . . . . . . 13 |- (x = y -> ({x} u. {y}) = {x})
25 vex 2368 . . . . . . . . . . . . . . 15 |- x e. _V
2625ensn1 5704 . . . . . . . . . . . . . 14 |- {x} ~~ 1o
27 1sdom2 5870 . . . . . . . . . . . . . 14 |- 1o ~< 2o
28 ensdomtr 5758 . . . . . . . . . . . . . 14 |- (({x} ~~ 1o /\ 1o ~< 2o) -> {x} ~< 2o)
2926, 27, 28mp2an 679 . . . . . . . . . . . . 13 |- {x} ~< 2o
3024, 29syl6eqbr 3415 . . . . . . . . . . . 12 |- (x = y -> ({x} u. {y}) ~< 2o)
31 sdomnen 5664 . . . . . . . . . . . 12 |- (({x} u. {y}) ~< 2o -> -. ({x} u. {y}) ~~ 2o)
3230, 31syl 14 . . . . . . . . . . 11 |- (x = y -> -. ({x} u. {y}) ~~ 2o)
3332necon2ai 2121 . . . . . . . . . 10 |- (({x} u. {y}) ~~ 2o -> x =/= y)
34 disjsn2 3140 . . . . . . . . . 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 2808 . . . . . . . . 9 |- ((A = {x} /\ B = {y}) -> (A u. B) = ({x} u. {y}))
3837breq1d 3388 . . . . . . . 8 |- ((A = {x} /\ B = {y}) -> ((A u. B) ~~ 2o <-> ({x} u. {y}) ~~ 2o))
39 ineq12 2845 . . . . . . . . 9 |- ((A = {x} /\ B = {y}) -> (A i^i B) = ({x} i^i {y}))
4039eqeq1d 1968 . . . . . . . 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 1677 . . . . 5 |- (A = {x} -> (E.y B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
4443exlimiv 1760 . . . 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 2078   u. cun 2660   i^i cin 2661  (/)c0 2926  {csn 3097   class class class wbr 3378  Oncon0 3696  suc csuc 3698  1oc1o 5356  2oc2o 5357   ~~ cen 5641   ~< csdm 5643
This theorem is referenced by:  pr2nelem 6250  pm110.643 6352  isprm2lem 9643
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 1671  ax-ext 1942  ax-rep 3464  ax-sep 3474  ax-nul 3483  ax-pow 3519  ax-pr 3543  ax-un 3813
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 1633  df-eu 1860  df-mo 1861  df-clab 1948  df-cleq 1953  df-clel 1956  df-ne 2080  df-ral 2173  df-rex 2174  df-reu 2175  df-rab 2176  df-v 2367  df-dif 2665  df-un 2667  df-in 2669  df-ss 2671  df-pss 2673  df-nul 2927  df-pw 3086  df-sn 3101  df-pr 3102  df-tp 3104  df-op 3105  df-uni 3234  df-br 3379  df-opab 3433  df-tr 3448  df-eprel 3626  df-id 3629  df-po 3634  df-so 3648  df-fr 3667  df-we 3683  df-ord 3699  df-on 3700  df-suc 3702  df-xp 4016  df-rel 4017  df-cnv 4018  df-co 4019  df-dm 4020  df-rn 4021  df-res 4022  df-ima 4023  df-fun 4024  df-fn 4025  df-f 4026  df-f1 4027  df-fo 4028  df-f1o 4029  df-fv 4030  df-1o 5363  df-2o 5364  df-er 5500  df-en 5645  df-dom 5646  df-sdom 5647
Copyright terms: Public domain