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

Definition df-suc 4398
Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 6530). 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 affect on a proper class (sucprc 4467), so that the successor of any ordinal class is still an ordinal class (ordsuc 4605), 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 4394 . 2  class  suc  A
31csn 3640 . . 3  class  { A }
41, 3cun 3150 . 2  class  ( A  u.  { A }
)
52, 4wceq 1623 1  wff  suc  A  =  ( A  u.  { A } )
Colors of variables: wff set class
This definition is referenced by:  suceq  4457  elsuci  4458  elsucg  4459  elsuc2g  4460  nfsuc  4463  suc0  4466  sucprc  4467  unisuc  4468  sssucid  4469  iunsuc  4474  trsuc2OLD  4477  orddif  4486  sucexb  4600  suceloni  4604  onuninsuci  4631  tfrlem10  6403  tfrlem16  6409  df2o3  6492  oarec  6560  limensuci  7037  infensuc  7039  phplem1  7040  sucdom2  7057  sucxpdom  7072  isinf  7076  pssnn  7081  dif1enOLD  7090  dif1en  7091  fiint  7133  pwfi  7151  dffi3  7184  sucprcreg  7313  cantnfp1lem3  7382  ranksuc  7537  pm54.43  7633  dif1card  7638  fseqenlem1  7651  cda1en  7801  ackbij1lem1  7846  ackbij1lem2  7847  ackbij1lem5  7850  ackbij1lem14  7859  cfsuc  7883  fin23lem26  7951  axdc3lem4  8079  unsnen  8175  wunsuc  8339  fzennn  11030  hashp1i  11369  dfon2lem3  24141  dfon2lem7  24145  brsuccf  24480  onsucsuccmpi  24882  onint1  24888  pwfi2f1o  27260  sucidALTVD  28646  sucidALT  28647  sucidVD  28648  bnj927  28800  bnj98  28899  bnj543  28925  bnj970  28979
  Copyright terms: Public domain W3C validator