MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm110.643 Structured version   Unicode version

Theorem pm110.643 8488
Description: 1+1=2 for cardinal number addition, derived from pm54.43 8312 as promised. Theorem *110.643 of Principia Mathematica, vol. II, p. 86, which adds the remark, "The above proposition is occasionally useful." Whitehead and Russell define cardinal addition on collections of all sets equinumerous to 1 and 2 (which for us are proper classes unless we restrict them as in karden 8244), but after applying definitions, our theorem is equivalent. The comment for cdaval 8481 explains why we use  ~~ instead of =. See pm110.643ALT 8489 for a shorter proof that doesn't use pm54.43 8312. (Contributed by NM, 5-Apr-2007.) (Proof modification is discouraged.)
Assertion
Ref Expression
pm110.643  |-  ( 1o 
+c  1o )  ~~  2o

Proof of Theorem pm110.643
StepHypRef Expression
1 1on 7073 . . 3  |-  1o  e.  On
2 cdaval 8481 . . 3  |-  ( ( 1o  e.  On  /\  1o  e.  On )  -> 
( 1o  +c  1o )  =  ( ( 1o  X.  { (/) } )  u.  ( 1o  X.  { 1o } ) ) )
31, 1, 2mp2an 670 . 2  |-  ( 1o 
+c  1o )  =  ( ( 1o  X.  { (/) } )  u.  ( 1o  X.  { 1o } ) )
4 xp01disj 7082 . . 3  |-  ( ( 1o  X.  { (/) } )  i^i  ( 1o 
X.  { 1o }
) )  =  (/)
51elexi 3057 . . . . 5  |-  1o  e.  _V
6 0ex 4510 . . . . 5  |-  (/)  e.  _V
75, 6xpsnen 7538 . . . 4  |-  ( 1o 
X.  { (/) } ) 
~~  1o
85, 5xpsnen 7538 . . . 4  |-  ( 1o 
X.  { 1o }
)  ~~  1o
9 pm54.43 8312 . . . 4  |-  ( ( ( 1o  X.  { (/)
} )  ~~  1o  /\  ( 1o  X.  { 1o } )  ~~  1o )  ->  ( ( ( 1o  X.  { (/) } )  i^i  ( 1o 
X.  { 1o }
) )  =  (/)  <->  (
( 1o  X.  { (/)
} )  u.  ( 1o  X.  { 1o }
) )  ~~  2o ) )
107, 8, 9mp2an 670 . . 3  |-  ( ( ( 1o  X.  { (/)
} )  i^i  ( 1o  X.  { 1o }
) )  =  (/)  <->  (
( 1o  X.  { (/)
} )  u.  ( 1o  X.  { 1o }
) )  ~~  2o )
114, 10mpbi 208 . 2  |-  ( ( 1o  X.  { (/) } )  u.  ( 1o 
X.  { 1o }
) )  ~~  2o
123, 11eqbrtri 4399 1  |-  ( 1o 
+c  1o )  ~~  2o
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1399    e. wcel 1836    u. cun 3400    i^i cin 3401   (/)c0 3724   {csn 3957   class class class wbr 4380   Oncon0 4805    X. cxp 4924  (class class class)co 6214   1oc1o 7059   2oc2o 7060    ~~ cen 7450    +c ccda 8478
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-sep 4501  ax-nul 4509  ax-pow 4556  ax-pr 4614  ax-un 6509
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-ral 2747  df-rex 2748  df-reu 2749  df-rab 2751  df-v 3049  df-sbc 3266  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-pss 3418  df-nul 3725  df-if 3871  df-pw 3942  df-sn 3958  df-pr 3960  df-tp 3962  df-op 3964  df-uni 4177  df-int 4213  df-br 4381  df-opab 4439  df-mpt 4440  df-tr 4474  df-eprel 4718  df-id 4722  df-po 4727  df-so 4728  df-fr 4765  df-we 4767  df-ord 4808  df-on 4809  df-lim 4810  df-suc 4811  df-xp 4932  df-rel 4933  df-cnv 4934  df-co 4935  df-dm 4936  df-rn 4937  df-res 4938  df-ima 4939  df-iota 5473  df-fun 5511  df-fn 5512  df-f 5513  df-f1 5514  df-fo 5515  df-f1o 5516  df-fv 5517  df-ov 6217  df-oprab 6218  df-mpt2 6219  df-om 6618  df-1o 7066  df-2o 7067  df-er 7247  df-en 7454  df-dom 7455  df-sdom 7456  df-cda 8479
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator