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

Definition df-suc 4574
Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 6761). 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 4643), so that the successor of any ordinal class is still an ordinal class (ordsuc 4780), 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 4570 . 2  class  suc  A
31csn 3801 . . 3  class  { A }
41, 3cun 3305 . 2  class  ( A  u.  { A }
)
52, 4wceq 1652 1  wff  suc  A  =  ( A  u.  { A } )
Colors of variables: wff set class
This definition is referenced by:  suceq  4633  elsuci  4634  elsucg  4635  elsuc2g  4636  nfsuc  4639  suc0  4642  sucprc  4643  unisuc  4644  sssucid  4645  iunsuc  4650  orddif  4661  sucexb  4775  suceloni  4779  onuninsuci  4806  tfrlem10  6634  tfrlem16  6640  df2o3  6723  oarec  6791  limensuci  7269  infensuc  7271  phplem1  7272  sucdom2  7289  sucxpdom  7304  isinf  7308  pssnn  7313  dif1enOLD  7326  dif1en  7327  fiint  7369  pwfi  7388  dffi3  7422  sucprcreg  7551  cantnfp1lem3  7620  ranksuc  7775  pm54.43  7871  dif1card  7876  fseqenlem1  7889  cda1en  8039  ackbij1lem1  8084  ackbij1lem2  8085  ackbij1lem5  8088  ackbij1lem14  8097  cfsuc  8121  fin23lem26  8189  axdc3lem4  8317  unsnen  8412  wunsuc  8576  fzennn  11290  hashp1i  11655  dfon2lem3  25391  dfon2lem7  25395  brsuccf  25731  onsucsuccmpi  26136  onint1  26142  pwfi2f1o  27170  sucidALTVD  28734  sucidALT  28735  sucidVD  28736  bnj927  28891  bnj98  28990  bnj543  29016  bnj970  29070
  Copyright terms: Public domain W3C validator