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

Theorem pm54.43 6389
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 6366), 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 6388. 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 6493 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 5507 . . . . . . 7 |- 1o e. On
21elisseti 2509 . . . . . 6 |- 1o e. _V
32ensn1 5812 . . . . . 6 |- {1o} ~~ 1o
42, 3ensymi 5801 . . . . 5 |- 1o ~~ {1o}
5 entr 5802 . . . . 5 |- ((B ~~ 1o /\ 1o ~~ {1o}) -> B ~~ {1o})
64, 5mpan2 755 . . . 4 |- (B ~~ 1o -> B ~~ {1o})
71onirri 3934 . . . . . . 7 |- -. 1o e. 1o
8 disjsn 3275 . . . . . . 7 |- ((1o i^i {1o}) = (/) <-> -. 1o e. 1o)
97, 8mpbir 238 . . . . . 6 |- (1o i^i {1o}) = (/)
10 unen 5827 . . . . . 6 |- (((A ~~ 1o /\ B ~~ {1o}) /\ ((A i^i B) = (/) /\ (1o i^i {1o}) = (/))) -> (A u. B) ~~ (1o u. {1o}))
119, 10mpanr2 770 . . . . 5 |- (((A ~~ 1o /\ B ~~ {1o}) /\ (A i^i B) = (/)) -> (A u. B) ~~ (1o u. {1o}))
1211ex 485 . . . 4 |- ((A ~~ 1o /\ B ~~ {1o}) -> ((A i^i B) = (/) -> (A u. B) ~~ (1o u. {1o})))
136, 12sylan2 526 . . 3 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) -> (A u. B) ~~ (1o u. {1o})))
14 df-2o 5501 . . . . 5 |- 2o = suc 1o
15 df-suc 3835 . . . . 5 |- suc 1o = (1o u. {1o})
1614, 15eqtri 2112 . . . 4 |- 2o = (1o u. {1o})
1716breq2i 3517 . . 3 |- ((A u. B) ~~ 2o <-> (A u. B) ~~ (1o u. {1o}))
1813, 17syl6ibr 263 . 2 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) -> (A u. B) ~~ 2o))
19 en1 5815 . . 3 |- (A ~~ 1o <-> E.x A = {x})
20 en1 5815 . . 3 |- (B ~~ 1o <-> E.y B = {y})
21 unidm 2940 . . . . . . . . . . . . . 14 |- ({x} u. {x}) = {x}
22 sneq 3242 . . . . . . . . . . . . . . 15 |- (x = y -> {x} = {y})
2322uneq2d 2951 . . . . . . . . . . . . . 14 |- (x = y -> ({x} u. {x}) = ({x} u. {y}))
2421, 23syl5reqr 2142 . . . . . . . . . . . . 13 |- (x = y -> ({x} u. {y}) = {x})
25 visset 2502 . . . . . . . . . . . . . . 15 |- x e. _V
2625ensn1 5812 . . . . . . . . . . . . . 14 |- {x} ~~ 1o
27 1sdom2 5981 . . . . . . . . . . . . . 14 |- 1o ~< 2o
28 ensdomtr 5866 . . . . . . . . . . . . . 14 |- (({x} ~~ 1o /\ 1o ~< 2o) -> {x} ~< 2o)
2926, 27, 28mp2an 756 . . . . . . . . . . . . 13 |- {x} ~< 2o
3024, 29syl6eqbr 3550 . . . . . . . . . . . 12 |- (x = y -> ({x} u. {y}) ~< 2o)
31 sdomnen 5771 . . . . . . . . . . . 12 |- (({x} u. {y}) ~< 2o -> -. ({x} u. {y}) ~~ 2o)
3230, 31syl 13 . . . . . . . . . . 11 |- (x = y -> -. ({x} u. {y}) ~~ 2o)
3332necon2ai 2262 . . . . . . . . . 10 |- (({x} u. {y}) ~~ 2o -> x =/= y)
34 disjsn2 3276 . . . . . . . . . 10 |- (x =/= y -> ({x} i^i {y}) = (/))
3533, 34syl 13 . . . . . . . . 9 |- (({x} u. {y}) ~~ 2o -> ({x} i^i {y}) = (/))
3635a1i 9 . . . . . . . 8 |- ((A = {x} /\ B = {y}) -> (({x} u. {y}) ~~ 2o -> ({x} i^i {y}) = (/)))
37 uneq12 2946 . . . . . . . . 9 |- ((A = {x} /\ B = {y}) -> (A u. B) = ({x} u. {y}))
3837breq1d 3519 . . . . . . . 8 |- ((A = {x} /\ B = {y}) -> ((A u. B) ~~ 2o <-> ({x} u. {y}) ~~ 2o))
39 ineq12 2983 . . . . . . . . 9 |- ((A = {x} /\ B = {y}) -> (A i^i B) = ({x} i^i {y}))
4039eqeq1d 2100 . . . . . . . 8 |- ((A = {x} /\ B = {y}) -> ((A i^i B) = (/) <-> ({x} i^i {y}) = (/)))
4136, 38, 403imtr4d 310 . . . . . . 7 |- ((A = {x} /\ B = {y}) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
4241ex 485 . . . . . 6 |- (A = {x} -> (B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
4342exlimdv 1809 . . . . 5 |- (A = {x} -> (E.y B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
4443exlimiv 1892 . . . 4 |- (E.x A = {x} -> (E.y B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
4544imp 480 . . 3 |- ((E.x A = {x} /\ E.y B = {y}) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
4619, 20, 45syl2anb 531 . 2 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
4718, 46impbid 216 1 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) <-> (A u. B) ~~ 2o))
Colors of variables: wff set class
Syntax hints:  -. wn 2   -> wi 3   <-> wb 209   /\ wa 418  E.wex 1520   = wceq 1592   e. wcel 1594   =/= wne 2218   u. cun 2799   i^i cin 2800  (/)c0 3065  {csn 3233   class class class wbr 3509  Oncon0 3829  suc csuc 3831  1oc1o 5493  2oc2o 5494   ~~ cen 5748   ~< csdm 5750
This theorem is referenced by:  pr2nelem 6390  pm110.643 6493  isprm2lem 9898
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1516  ax-6 1517  ax-7 1518  ax-gen 1519  ax-8 1596  ax-10 1597  ax-11 1598  ax-12 1599  ax-13 1600  ax-14 1601  ax-17 1608  ax-9 1620  ax-4 1626  ax-16 1803  ax-ext 2074  ax-rep 3599  ax-sep 3609  ax-nul 3619  ax-pow 3655  ax-pr 3679  ax-un 3947
This theorem depends on definitions:  df-bi 210  df-or 419  df-an 420  df-3or 1038  df-3an 1039  df-ex 1521  df-sb 1765  df-eu 1992  df-mo 1993  df-clab 2080  df-cleq 2085  df-clel 2088  df-ne 2220  df-ral 2314  df-rex 2315  df-reu 2316  df-rab 2317  df-v 2501  df-dif 2804  df-un 2806  df-in 2808  df-ss 2810  df-pss 2812  df-nul 3066  df-pw 3222  df-sn 3237  df-pr 3238  df-tp 3240  df-op 3241  df-uni 3365  df-br 3510  df-opab 3568  df-tr 3583  df-eprel 3762  df-id 3765  df-po 3770  df-so 3782  df-fr 3800  df-we 3816  df-ord 3832  df-on 3833  df-suc 3835  df-xp 4151  df-rel 4152  df-cnv 4153  df-co 4154  df-dm 4155  df-rn 4156  df-res 4157  df-ima 4158  df-fun 4159  df-fn 4160  df-f 4161  df-f1 4162  df-fo 4163  df-f1o 4164  df-fv 4165  df-1o 5500  df-2o 5501  df-er 5637  df-en 5752  df-dom 5753  df-sdom 5754
Copyright terms: Public domain