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

Definition df-suc 4622
Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 6811). 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 4691), so that the successor of any ordinal class is still an ordinal class (ordsuc 4829), 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 4618 . 2  class  suc  A
31csn 3843 . . 3  class  { A }
41, 3cun 3307 . 2  class  ( A  u.  { A }
)
52, 4wceq 1654 1  wff  suc  A  =  ( A  u.  { A } )
Colors of variables: wff set class
This definition is referenced by:  suceq  4681  elsuci  4682  elsucg  4683  elsuc2g  4684  nfsuc  4687  suc0  4690  sucprc  4691  unisuc  4692  sssucid  4693  iunsuc  4698  orddif  4710  sucexb  4824  suceloni  4828  onuninsuci  4855  tfrlem10  6684  tfrlem16  6690  df2o3  6773  oarec  6841  limensuci  7319  infensuc  7321  phplem1  7322  sucdom2  7339  sucxpdom  7354  isinf  7358  pssnn  7363  dif1enOLD  7376  dif1en  7377  fiint  7419  pwfi  7438  dffi3  7472  sucprcreg  7603  cantnfp1lem3  7672  ranksuc  7827  pm54.43  7925  dif1card  7930  fseqenlem1  7943  cda1en  8093  ackbij1lem1  8138  ackbij1lem2  8139  ackbij1lem5  8142  ackbij1lem14  8151  cfsuc  8175  fin23lem26  8243  axdc3lem4  8371  unsnen  8466  wunsuc  8630  fzennn  11345  hashp1i  11710  dfon2lem3  25447  dfon2lem7  25451  brsuccf  25821  onsucsuccmpi  26228  onint1  26234  pwfi2f1o  27349  sucidALTVD  29156  sucidALT  29157  sucidVD  29158  bnj927  29313  bnj98  29412  bnj543  29438  bnj970  29492
  Copyright terms: Public domain W3C validator