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

Definition df-suc 4400
Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 6532). 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 4469), so that the successor of any ordinal class is still an ordinal class (ordsuc 4607), 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 4396 . 2  class  suc  A
31csn 3642 . . 3  class  { A }
41, 3cun 3152 . 2  class  ( A  u.  { A }
)
52, 4wceq 1625 1  wff  suc  A  =  ( A  u.  { A } )
Colors of variables: wff set class
This definition is referenced by:  suceq  4459  elsuci  4460  elsucg  4461  elsuc2g  4462  nfsuc  4465  suc0  4468  sucprc  4469  unisuc  4470  sssucid  4471  iunsuc  4476  trsuc2OLD  4479  orddif  4488  sucexb  4602  suceloni  4606  onuninsuci  4633  tfrlem10  6405  tfrlem16  6411  df2o3  6494  oarec  6562  limensuci  7039  infensuc  7041  phplem1  7042  sucdom2  7059  sucxpdom  7074  isinf  7078  pssnn  7083  dif1enOLD  7092  dif1en  7093  fiint  7135  pwfi  7153  dffi3  7186  sucprcreg  7315  cantnfp1lem3  7384  ranksuc  7539  pm54.43  7635  dif1card  7640  fseqenlem1  7653  cda1en  7803  ackbij1lem1  7848  ackbij1lem2  7849  ackbij1lem5  7852  ackbij1lem14  7861  cfsuc  7885  fin23lem26  7953  axdc3lem4  8081  unsnen  8177  wunsuc  8341  fzennn  11032  hashp1i  11371  dfon2lem3  24143  dfon2lem7  24147  brsuccf  24482  onsucsuccmpi  24884  onint1  24890  pwfi2f1o  27271  sucidALTVD  28719  sucidALT  28720  sucidVD  28721  bnj927  28873  bnj98  28972  bnj543  28998  bnj970  29052
  Copyright terms: Public domain W3C validator