MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm54.43 Unicode version

Theorem pm54.43 7159
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 7127), 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 7158. 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 7310 shows the derivation of 1+1=2 for cardinal numbers from this theorem. (Contributed by NM, 4-Apr-2007.)

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 5985 . . . . . . . 8  |-  1o  e.  On
21elexi 2521 . . . . . . 7  |-  1o  e.  _V
32ensn1 6406 . . . . . 6  |-  { 1o }  ~~  1o
43ensymi 6393 . . . . 5  |-  1o  ~~  { 1o }
5 entr 6394 . . . . 5  |-  ( ( B  ~~  1o  /\  1o  ~~  { 1o }
)  ->  B  ~~  { 1o } )
64, 5mpan2 647 . . . 4  |-  ( B 
~~  1o  ->  B  ~~  { 1o } )
71onirri 4092 . . . . . . 7  |-  -.  1o  e.  1o
8 disjsn 3347 . . . . . . 7  |-  ( ( 1o  i^i  { 1o } )  =  (/)  <->  -.  1o  e.  1o )
97, 8mpbir 198 . . . . . 6  |-  ( 1o 
i^i  { 1o } )  =  (/)
10 unen 6424 . . . . . 6  |-  ( ( ( A  ~~  1o  /\  B  ~~  { 1o } )  /\  (
( A  i^i  B
)  =  (/)  /\  ( 1o  i^i  { 1o }
)  =  (/) ) )  ->  ( A  u.  B )  ~~  ( 1o  u.  { 1o }
) )
119, 10mpanr2 660 . . . . 5  |-  ( ( ( A  ~~  1o  /\  B  ~~  { 1o } )  /\  ( A  i^i  B )  =  (/) )  ->  ( A  u.  B )  ~~  ( 1o  u.  { 1o } ) )
1211ex 420 . . . 4  |-  ( ( A  ~~  1o  /\  B  ~~  { 1o }
)  ->  ( ( A  i^i  B )  =  (/)  ->  ( A  u.  B )  ~~  ( 1o  u.  { 1o }
) ) )
136, 12sylan2 455 . . 3  |-  ( ( A  ~~  1o  /\  B  ~~  1o )  -> 
( ( A  i^i  B )  =  (/)  ->  ( A  u.  B )  ~~  ( 1o  u.  { 1o } ) ) )
14 df-2o 5979 . . . . 5  |-  2o  =  suc  1o
15 df-suc 3993 . . . . 5  |-  suc  1o  =  ( 1o  u.  { 1o } )
1614, 15eqtri 2120 . . . 4  |-  2o  =  ( 1o  u.  { 1o } )
1716breq2i 3638 . . 3  |-  ( ( A  u.  B ) 
~~  2o  <->  ( A  u.  B )  ~~  ( 1o  u.  { 1o }
) )
1813, 17syl6ibr 216 . 2  |-  ( ( A  ~~  1o  /\  B  ~~  1o )  -> 
( ( A  i^i  B )  =  (/)  ->  ( A  u.  B )  ~~  2o ) )
19 en1 6409 . . 3  |-  ( A 
~~  1o  <->  E. x  A  =  { x } )
20 en1 6409 . . 3  |-  ( B 
~~  1o  <->  E. y  B  =  { y } )
21 unidm 2977 . . . . . . . . . . . . . 14  |-  ( { x }  u.  {
x } )  =  { x }
22 sneq 3305 . . . . . . . . . . . . . . 15  |-  ( x  =  y  ->  { x }  =  { y } )
2322uneq2d 2988 . . . . . . . . . . . . . 14  |-  ( x  =  y  ->  ( { x }  u.  { x } )  =  ( { x }  u.  { y } ) )
2421, 23syl5reqr 2147 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  ( { x }  u.  { y } )  =  { x } )
25 vex 2515 . . . . . . . . . . . . . . 15  |-  x  e. 
_V
2625ensn1 6406 . . . . . . . . . . . . . 14  |-  { x }  ~~  1o
27 1sdom2 6589 . . . . . . . . . . . . . 14  |-  1o  ~<  2o
28 ensdomtr 6478 . . . . . . . . . . . . . 14  |-  ( ( { x }  ~~  1o  /\  1o  ~<  2o )  ->  { x }  ~<  2o )
2926, 27, 28mp2an 648 . . . . . . . . . . . . 13  |-  { x }  ~<  2o
3024, 29syl6eqbr 3667 . . . . . . . . . . . 12  |-  ( x  =  y  ->  ( { x }  u.  { y } )  ~<  2o )
31 sdomnen 6372 . . . . . . . . . . . 12  |-  ( ( { x }  u.  { y } )  ~<  2o  ->  -.  ( {
x }  u.  {
y } )  ~~  2o )
3230, 31syl 15 . . . . . . . . . . 11  |-  ( x  =  y  ->  -.  ( { x }  u.  { y } )  ~~  2o )
3332necon2ai 2263 . . . . . . . . . 10  |-  ( ( { x }  u.  { y } )  ~~  2o  ->  x  =/=  y
)
34 disjsn2 3348 . . . . . . . . . 10  |-  ( x  =/=  y  ->  ( { x }  i^i  { y } )  =  (/) )
3533, 34syl 15 . . . . . . . . 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 2983 . . . . . . . . 9  |-  ( ( A  =  { x }  /\  B  =  {
y } )  -> 
( A  u.  B
)  =  ( { x }  u.  {
y } ) )
3837breq1d 3640 . . . . . . . 8  |-  ( ( A  =  { x }  /\  B  =  {
y } )  -> 
( ( A  u.  B )  ~~  2o  <->  ( { x }  u.  { y } )  ~~  2o ) )
39 ineq12 3022 . . . . . . . . 9  |-  ( ( A  =  { x }  /\  B  =  {
y } )  -> 
( A  i^i  B
)  =  ( { x }  i^i  {
y } ) )
4039eqeq1d 2108 . . . . . . . 8  |-  ( ( A  =  { x }  /\  B  =  {
y } )  -> 
( ( A  i^i  B )  =  (/)  <->  ( {
x }  i^i  {
y } )  =  (/) ) )
4136, 38, 403imtr4d 257 . . . . . . 7  |-  ( ( A  =  { x }  /\  B  =  {
y } )  -> 
( ( A  u.  B )  ~~  2o  ->  ( A  i^i  B
)  =  (/) ) )
4241ex 420 . . . . . 6  |-  ( A  =  { x }  ->  ( B  =  {
y }  ->  (
( A  u.  B
)  ~~  2o  ->  ( A  i^i  B )  =  (/) ) ) )
4342exlimdv 1793 . . . . 5  |-  ( A  =  { x }  ->  ( E. y  B  =  { y }  ->  ( ( A  u.  B )  ~~  2o  ->  ( A  i^i  B )  =  (/) ) ) )
4443exlimiv 1879 . . . 4  |-  ( E. x  A  =  {
x }  ->  ( E. y  B  =  { y }  ->  ( ( A  u.  B
)  ~~  2o  ->  ( A  i^i  B )  =  (/) ) ) )
4544imp 415 . . 3  |-  ( ( E. x  A  =  { x }  /\  E. y  B  =  {
y } )  -> 
( ( A  u.  B )  ~~  2o  ->  ( A  i^i  B
)  =  (/) ) )
4619, 20, 45syl2anb 460 . 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 356   E.wex 1456    = wceq 1531    e. wcel 1533    =/= wne 2218    u. cun 2828    i^i cin 2829   (/)c0 3110   {csn 3294   class class class wbr 3630   Oncon0 3987   suc csuc 3989   1oc1o 5971   2oc2o 5972    ~~ cen 6342    ~< csdm 6344
This theorem is referenced by:  pr2nelem  7160  pm110.643  7310  isprm2lem  11924
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1452  ax-6 1453  ax-7 1454  ax-gen 1455  ax-8 1535  ax-11 1536  ax-13 1537  ax-14 1538  ax-17 1540  ax-12o 1574  ax-10 1588  ax-9 1594  ax-4 1601  ax-16 1787  ax-ext 2082  ax-sep 3745  ax-nul 3753  ax-pow 3789  ax-pr 3813  ax-un 4105
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-3or 901  df-3an 902  df-tru 1265  df-ex 1457  df-sb 1748  df-eu 1970  df-mo 1971  df-clab 2088  df-cleq 2093  df-clel 2096  df-ne 2220  df-ral 2315  df-rex 2316  df-reu 2317  df-rab 2318  df-v 2514  df-sbc 2688  df-dif 2833  df-un 2835  df-in 2837  df-ss 2841  df-pss 2843  df-nul 3111  df-if 3221  df-pw 3282  df-sn 3300  df-pr 3301  df-tp 3302  df-op 3303  df-uni 3469  df-br 3631  df-opab 3685  df-tr 3718  df-eprel 3900  df-id 3904  df-po 3909  df-so 3910  df-fr 3947  df-we 3949  df-ord 3990  df-on 3991  df-lim 3992  df-suc 3993  df-om 4268  df-xp 4314  df-rel 4315  df-cnv 4316  df-co 4317  df-dm 4318  df-rn 4319  df-res 4320  df-ima 4321  df-fun 4322  df-fn 4323  df-f 4324  df-f1 4325  df-fo 4326  df-f1o 4327  df-fv 4328  df-1o 5978  df-2o 5979  df-er 6159  df-en 6346  df-dom 6347  df-sdom 6348
  Copyright terms: Public domain W3C validator