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

Definition df-suc 4370
Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 6498). 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 4439), so that the successor of any ordinal class is still an ordinal class (ordsuc 4577), 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 4366 . 2  class  suc  A
31csn 3614 . . 3  class  { A }
41, 3cun 3125 . 2  class  ( A  u.  { A }
)
52, 4wceq 1619 1  wff  suc  A  =  ( A  u.  { A } )
Colors of variables: wff set class
This definition is referenced by:  suceq  4429  elsuci  4430  elsucg  4431  elsuc2g  4432  nfsuc  4435  suc0  4438  sucprc  4439  unisuc  4440  sssucid  4441  iunsuc  4446  trsuc2OLD  4449  orddif  4458  sucexb  4572  suceloni  4576  onuninsuci  4603  tfrlem10  6371  tfrlem16  6377  df2o3  6460  oarec  6528  limensuci  7005  infensuc  7007  phplem1  7008  sucdom2  7025  sucxpdom  7040  isinf  7044  pssnn  7049  dif1enOLD  7058  dif1en  7059  fiint  7101  pwfi  7119  dffi3  7152  sucprcreg  7281  cantnfp1lem3  7350  ranksuc  7505  pm54.43  7601  dif1card  7606  fseqenlem1  7619  cda1en  7769  ackbij1lem1  7814  ackbij1lem2  7815  ackbij1lem5  7818  ackbij1lem14  7827  cfsuc  7851  fin23lem26  7919  axdc3lem4  8047  unsnen  8143  wunsuc  8307  fzennn  10996  hashp1i  11334  dfon2lem3  23510  dfon2lem7  23514  brsuccf  23855  onsucsuccmpi  24257  onint1  24263  pwfi2f1o  26627  sucidALTVD  27696  sucidALT  27697  sucidVD  27698  bnj927  27849  bnj98  27948  bnj543  27974  bnj970  28028
  Copyright terms: Public domain W3C validator