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

Definition df-suc 4884
Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 7178). 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 4953), so that the successor of any ordinal class is still an ordinal class (ordsuc 6627), 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 4880 . 2  class  suc  A
31csn 4027 . . 3  class  { A }
41, 3cun 3474 . 2  class  ( A  u.  { A }
)
52, 4wceq 1379 1  wff  suc  A  =  ( A  u.  { A } )
Colors of variables: wff setvar class
This definition is referenced by:  suceq  4943  elsuci  4944  elsucg  4945  elsuc2g  4946  nfsuc  4949  suc0  4952  sucprc  4953  unisuc  4954  sssucid  4955  iunsuc  4960  orddif  4971  sucexb  6622  suceloni  6626  onuninsuci  6653  tfrlem10  7053  tfrlem16  7059  df2o3  7140  oarec  7208  limensuci  7690  infensuc  7692  phplem1  7693  sucdom2  7711  sucxpdom  7726  isinf  7730  pssnn  7735  dif1enOLD  7748  dif1en  7749  fiint  7793  pwfi  7811  dffi3  7887  sucprcreg  8021  sucprcregOLD  8022  cantnfp1lem3  8095  cantnfp1lem3OLD  8121  ranksuc  8279  pm54.43  8377  dif1card  8384  fseqenlem1  8401  cda1en  8551  ackbij1lem1  8596  ackbij1lem2  8597  ackbij1lem5  8600  ackbij1lem14  8609  cfsuc  8633  fin23lem26  8701  axdc3lem4  8829  unsnen  8924  wunsuc  9091  fzennn  12042  hashp1i  12430  dfon2lem3  28794  dfon2lem7  28798  brsuccf  29168  onsucsuccmpi  29485  onint1  29491  pwfi2f1o  30648  sucidALTVD  32750  sucidALT  32751  sucidVD  32752  bnj927  32906  bnj98  33004  bnj543  33030  bnj970  33084
  Copyright terms: Public domain W3C validator