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

Definition df-suc 4397
Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 6525). 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 4466), so that the successor of any ordinal class is still an ordinal class (ordsuc 4604), 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 4393 . 2  class  suc  A
31csn 3641 . . 3  class  { A }
41, 3cun 3151 . 2  class  ( A  u.  { A }
)
52, 4wceq 1624 1  wff  suc  A  =  ( A  u.  { A } )
Colors of variables: wff set class
This definition is referenced by:  suceq  4456  elsuci  4457  elsucg  4458  elsuc2g  4459  nfsuc  4462  suc0  4465  sucprc  4466  unisuc  4467  sssucid  4468  iunsuc  4473  trsuc2OLD  4476  orddif  4485  sucexb  4599  suceloni  4603  onuninsuci  4630  tfrlem10  6398  tfrlem16  6404  df2o3  6487  oarec  6555  limensuci  7032  infensuc  7034  phplem1  7035  sucdom2  7052  sucxpdom  7067  isinf  7071  pssnn  7076  dif1enOLD  7085  dif1en  7086  fiint  7128  pwfi  7146  dffi3  7179  sucprcreg  7308  cantnfp1lem3  7377  ranksuc  7532  pm54.43  7628  dif1card  7633  fseqenlem1  7646  cda1en  7796  ackbij1lem1  7841  ackbij1lem2  7842  ackbij1lem5  7845  ackbij1lem14  7854  cfsuc  7878  fin23lem26  7946  axdc3lem4  8074  unsnen  8170  wunsuc  8334  fzennn  11024  hashp1i  11363  dfon2lem3  23542  dfon2lem7  23546  brsuccf  23887  onsucsuccmpi  24289  onint1  24295  pwfi2f1o  26659  sucidALTVD  27914  sucidALT  27915  sucidVD  27916  bnj927  28067  bnj98  28166  bnj543  28192  bnj970  28246
  Copyright terms: Public domain W3C validator