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

Definition df-suc 4530
Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 6713). 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 4599), so that the successor of any ordinal class is still an ordinal class (ordsuc 4736), 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 4526 . 2  class  suc  A
31csn 3759 . . 3  class  { A }
41, 3cun 3263 . 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  4589  elsuci  4590  elsucg  4591  elsuc2g  4592  nfsuc  4595  suc0  4598  sucprc  4599  unisuc  4600  sssucid  4601  iunsuc  4606  orddif  4617  sucexb  4731  suceloni  4735  onuninsuci  4762  tfrlem10  6586  tfrlem16  6592  df2o3  6675  oarec  6743  limensuci  7221  infensuc  7223  phplem1  7224  sucdom2  7241  sucxpdom  7256  isinf  7260  pssnn  7265  dif1enOLD  7278  dif1en  7279  fiint  7321  pwfi  7339  dffi3  7373  sucprcreg  7502  cantnfp1lem3  7571  ranksuc  7726  pm54.43  7822  dif1card  7827  fseqenlem1  7840  cda1en  7990  ackbij1lem1  8035  ackbij1lem2  8036  ackbij1lem5  8039  ackbij1lem14  8048  cfsuc  8072  fin23lem26  8140  axdc3lem4  8268  unsnen  8363  wunsuc  8527  fzennn  11236  hashp1i  11601  dfon2lem3  25167  dfon2lem7  25171  brsuccf  25506  onsucsuccmpi  25909  onint1  25915  pwfi2f1o  26931  sucidALTVD  28325  sucidALT  28326  sucidVD  28327  bnj927  28479  bnj98  28578  bnj543  28604  bnj970  28658
  Copyright terms: Public domain W3C validator