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

Definition df-suc 4547
Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 6734). 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 4616), so that the successor of any ordinal class is still an ordinal class (ordsuc 4753), 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 4543 . 2  class  suc  A
31csn 3774 . . 3  class  { A }
41, 3cun 3278 . 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  4606  elsuci  4607  elsucg  4608  elsuc2g  4609  nfsuc  4612  suc0  4615  sucprc  4616  unisuc  4617  sssucid  4618  iunsuc  4623  orddif  4634  sucexb  4748  suceloni  4752  onuninsuci  4779  tfrlem10  6607  tfrlem16  6613  df2o3  6696  oarec  6764  limensuci  7242  infensuc  7244  phplem1  7245  sucdom2  7262  sucxpdom  7277  isinf  7281  pssnn  7286  dif1enOLD  7299  dif1en  7300  fiint  7342  pwfi  7360  dffi3  7394  sucprcreg  7523  cantnfp1lem3  7592  ranksuc  7747  pm54.43  7843  dif1card  7848  fseqenlem1  7861  cda1en  8011  ackbij1lem1  8056  ackbij1lem2  8057  ackbij1lem5  8060  ackbij1lem14  8069  cfsuc  8093  fin23lem26  8161  axdc3lem4  8289  unsnen  8384  wunsuc  8548  fzennn  11262  hashp1i  11627  dfon2lem3  25355  dfon2lem7  25359  brsuccf  25694  onsucsuccmpi  26097  onint1  26103  pwfi2f1o  27128  sucidALTVD  28691  sucidALT  28692  sucidVD  28693  bnj927  28845  bnj98  28944  bnj543  28970  bnj970  29024
  Copyright terms: Public domain W3C validator