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

Definition df-suc 4873
Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 7173). 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 4942), so that the successor of any ordinal class is still an ordinal class (ordsuc 6622), 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 4869 . 2  class  suc  A
31csn 4016 . . 3  class  { A }
41, 3cun 3459 . 2  class  ( A  u.  { A }
)
52, 4wceq 1398 1  wff  suc  A  =  ( A  u.  { A } )
Colors of variables: wff setvar class
This definition is referenced by:  suceq  4932  elsuci  4933  elsucg  4934  elsuc2g  4935  nfsuc  4938  suc0  4941  sucprc  4942  unisuc  4943  sssucid  4944  iunsuc  4949  orddif  4960  sucexb  6617  suceloni  6621  onuninsuci  6648  tfrlem10  7048  tfrlem16  7054  df2o3  7135  oarec  7203  limensuci  7686  infensuc  7688  phplem1  7689  sucdom2  7707  sucxpdom  7722  isinf  7726  pssnn  7731  dif1en  7745  fiint  7789  pwfi  7807  dffi3  7883  sucprcreg  8017  cantnfp1lem3  8090  cantnfp1lem3OLD  8116  ranksuc  8274  pm54.43  8372  dif1card  8379  fseqenlem1  8396  cda1en  8546  ackbij1lem1  8591  ackbij1lem2  8592  ackbij1lem5  8595  ackbij1lem14  8604  cfsuc  8628  fin23lem26  8696  axdc3lem4  8824  unsnen  8919  wunsuc  9084  fzennn  12060  hashp1i  12452  dfon2lem3  29457  dfon2lem7  29461  brsuccf  29819  onsucsuccmpi  30136  onint1  30142  pwfi2f1o  31283  pwfi2f1oOLD  31284  sucidALTVD  34071  sucidALT  34072  sucidVD  34073  bnj927  34228  bnj98  34326  bnj543  34352  bnj970  34406
  Copyright terms: Public domain W3C validator