MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-suc Unicode version

Definition df-suc 4551
Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 6738). Definition 7.22 of [TakeutiZaring] p. 41, who use "+ 1" to denote this function. Our definition is a generalization to classes. Although it is not conventional to use it with proper classes, it has no effect on a proper class (sucprc 4620), so that the successor of any ordinal class is still an ordinal class (ordsuc 4757), simplifying certain proofs. Some authors denote the successor operation with a prime (apostrophe-like) symbol, such as Definition 6 of [Suppes] p. 134 and the definition of successor in [Mendelson] p. 246 (who uses the symbol "Suc" as a predicate to mean "is a successor ordinal"). The definition of successor of [Enderton] p. 68 denotes the operation with a plus-sign superscript. (Contributed by NM, 30-Aug-1993.)
Assertion
Ref Expression
df-suc  |-  suc  A  =  ( A  u.  { A } )

Detailed syntax breakdown of Definition df-suc
StepHypRef Expression
1 cA . . 3  class  A
21csuc 4547 . 2  class  suc  A
31csn 3778 . . 3  class  { A }
41, 3cun 3282 . 2  class  ( A  u.  { A }
)
52, 4wceq 1649 1  wff  suc  A  =  ( A  u.  { A } )
Colors of variables: wff set class
This definition is referenced by:  suceq  4610  elsuci  4611  elsucg  4612  elsuc2g  4613  nfsuc  4616  suc0  4619  sucprc  4620  unisuc  4621  sssucid  4622  iunsuc  4627  orddif  4638  sucexb  4752  suceloni  4756  onuninsuci  4783  tfrlem10  6611  tfrlem16  6617  df2o3  6700  oarec  6768  limensuci  7246  infensuc  7248  phplem1  7249  sucdom2  7266  sucxpdom  7281  isinf  7285  pssnn  7290  dif1enOLD  7303  dif1en  7304  fiint  7346  pwfi  7364  dffi3  7398  sucprcreg  7527  cantnfp1lem3  7596  ranksuc  7751  pm54.43  7847  dif1card  7852  fseqenlem1  7865  cda1en  8015  ackbij1lem1  8060  ackbij1lem2  8061  ackbij1lem5  8064  ackbij1lem14  8073  cfsuc  8097  fin23lem26  8165  axdc3lem4  8293  unsnen  8388  wunsuc  8552  fzennn  11266  hashp1i  11631  dfon2lem3  25359  dfon2lem7  25363  brsuccf  25698  onsucsuccmpi  26101  onint1  26107  pwfi2f1o  27132  sucidALTVD  28695  sucidALT  28696  sucidVD  28697  bnj927  28849  bnj98  28948  bnj543  28974  bnj970  29028
  Copyright terms: Public domain W3C validator