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

Theorem pm54.43 7095
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 7063), 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 7094. 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 7246 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 5933 . . . . . . . 8  |-  1o  e.  On
21elexi 2501 . . . . . . 7  |-  1o  e.  _V
32ensn1 6349 . . . . . 6  |-  { 1o }  ~~  1o
43ensymi 6336 . . . . 5  |-  1o  ~~  { 1o }
5 entr 6337 . . . . 5  |-  ( ( B  ~~  1o  /\  1o  ~~ 
{ 1o } )  ->  B  ~~  { 1o } )
64, 5mpan2 648 . . . 4  |-  ( B  ~~  1o  ->  B  ~~  { 1o } )
71onirri 4062 . . . . . . 7  |-  -.  1o  e.  1o
8 disjsn 3324 . . . . . . 7  |-  ( ( 1o  i^i  { 1o }
)  =  (/)  <->  -.  1o  e.  1o )
97, 8mpbir 198 . . . . . 6  |-  ( 1o  i^i  { 1o } )  =  (/)
10 unen 6367 . . . . . 6  |-  ( (
( A  ~~  1o  /\  B  ~~  { 1o } )  /\  (
( A  i^i  B
)  =  (/)  /\  ( 1o  i^i  { 1o }
)  =  (/) ) )  ->  ( A  u.  B )  ~~  ( 1o  u.  { 1o }
) )
119, 10mpanr2 661 . . . . 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 454 . . 3  |-  ( ( A  ~~  1o  /\  B  ~~  1o )  ->  (
( A  i^i  B
)  =  (/)  ->  ( A  u.  B )  ~~  ( 1o  u.  { 1o } ) ) )
14 df-2o 5927 . . . . 5  |-  2o  =  suc  1o
15 df-suc 3963 . . . . 5  |-  suc  1o  =  ( 1o  u.  { 1o } )
1614, 15eqtri 2102 . . . 4  |-  2o  =  ( 1o  u.  { 1o } )
1716breq2i 3608 . . 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 6352 . . 3  |-  ( A  ~~  1o  <->  E. x  A  =  { x } )
20 en1 6352 . . 3  |-  ( B  ~~  1o  <->  E. y  B  =  { y } )
21 unidm 2957 . . . . . . . . . . . . . 14  |-  ( {
x }  u.  {
x } )  =  { x }
22 sneq 3283 . . . . . . . . . . . . . . 15  |-  ( x  =  y  ->  { x }  =  { y } )
2322uneq2d 2968 . . . . . . . . . . . . . 14  |-  ( x  =  y  ->  ( { x }  u.  {
x } )  =  ( { x }  u.  { y } ) )
2421, 23syl5reqr 2129 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  ( { x }  u.  {
y } )  =  { x } )
25 vex 2495 . . . . . . . . . . . . . . 15  |-  x  e.  _V
2625ensn1 6349 . . . . . . . . . . . . . 14  |-  { x }  ~~  1o
27 1sdom2 6532 . . . . . . . . . . . . . 14  |-  1o  ~<  2o
28 ensdomtr 6421 . . . . . . . . . . . . . 14  |-  ( ( { x }  ~~  1o  /\  1o  ~<  2o )  ->  { x }  ~<  2o )
2926, 27, 28mp2an 649 . . . . . . . . . . . . 13  |-  { x }  ~<  2o
3024, 29syl6eqbr 3637 . . . . . . . . . . . 12  |-  ( x  =  y  ->  ( { x }  u.  {
y } )  ~<  2o )
31 sdomnen 6315 . . . . . . . . . . . 12  |-  ( ( { x }  u.  { y } )  ~<  2o  ->  -.  ( {
x }  u.  {
y } )  ~~  2o )
3230, 31syl 15 . . . . . . . . . . 11  |-  ( x  =  y  ->  -.  ( { x }  u.  { y } )  ~~  2o )
3332necon2ai 2243 . . . . . . . . . 10  |-  ( ( { x }  u.  { y } )  ~~  2o  ->  x  =/=  y
)
34 disjsn2 3326 . . . . . . . . . 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 2963 . . . . . . . . 9  |-  ( ( A  =  { x }  /\  B  =  {
y } )  -> 
( A  u.  B
)  =  ( { x }  u.  {
y } ) )
3837breq1d 3610 . . . . . . . 8  |-  ( ( A  =  { x }  /\  B  =  {
y } )  -> 
( ( A  u.  B )  ~~  2o  <->  ( { x }  u.  { y } )  ~~  2o ) )
39 ineq12 3002 . . . . . . . . 9  |-  ( ( A  =  { x }  /\  B  =  {
y } )  -> 
( A  i^i  B
)  =  ( { x }  i^i  {
y } ) )
4039eqeq1d 2090 . . . . . . . 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 1799 . . . . 5  |-  ( A  =  { x }  ->  ( E. y  B  =  { y }  ->  ( ( A  u.  B
)  ~~  2o  ->  ( A  i^i  B )  =  (/) ) ) )
4443exlimiv 1885 . . . 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 459 . 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 357   E.wex 1455    = wceq 1536    e. wcel 1538    =/= wne 2199    u. cun 2808    i^i cin 2809   (/)c0 3088   {csn 3272   class class class wbr 3600   Oncon0 3957   suc csuc 3959   1oc1o 5919   2oc2o 5920    ~~ cen 6285    ~< csdm 6287
This theorem is referenced by:  pr2nelem  7096  pm110.643  7246  isprm2lem  11251
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1451  ax-6 1452  ax-7 1453  ax-gen 1454  ax-8 1540  ax-11 1541  ax-13 1542  ax-14 1543  ax-17 1545  ax-12o 1578  ax-10 1592  ax-9 1598  ax-4 1606  ax-16 1793  ax-ext 2064  ax-sep 3715  ax-nul 3723  ax-pow 3759  ax-pr 3783  ax-un 4075
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 904  df-3an 905  df-tru 1268  df-ex 1456  df-sb 1754  df-eu 1976  df-mo 1977  df-clab 2070  df-cleq 2075  df-clel 2078  df-ne 2201  df-ral 2295  df-rex 2296  df-reu 2297  df-rab 2298  df-v 2494  df-sbc 2668  df-dif 2813  df-un 2815  df-in 2817  df-ss 2821  df-pss 2823  df-nul 3089  df-if 3199  df-pw 3260  df-sn 3278  df-pr 3279  df-tp 3280  df-op 3281  df-uni 3439  df-br 3601  df-opab 3655  df-tr 3688  df-eprel 3870  df-id 3874  df-po 3879  df-so 3880  df-fr 3917  df-we 3919  df-ord 3960  df-on 3961  df-lim 3962  df-suc 3963  df-om 4243  df-xp 4289  df-rel 4290  df-cnv 4291  df-co 4292  df-dm 4293  df-rn 4294  df-res 4295  df-ima 4296  df-fun 4297  df-fn 4298  df-f 4299  df-f1 4300  df-fo 4301  df-f1o 4302  df-fv 4303  df-1o 5926  df-2o 5927  df-er 6102  df-en 6289  df-dom 6290  df-sdom 6291
Copyright terms: Public domain