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

Definition df-suc 4579
Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 6767). 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 4648), so that the successor of any ordinal class is still an ordinal class (ordsuc 4786), 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 4575 . 2  class  suc  A
31csn 3806 . . 3  class  { A }
41, 3cun 3310 . 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  4638  elsuci  4639  elsucg  4640  elsuc2g  4641  nfsuc  4644  suc0  4647  sucprc  4648  unisuc  4649  sssucid  4650  iunsuc  4655  orddif  4667  sucexb  4781  suceloni  4785  onuninsuci  4812  tfrlem10  6640  tfrlem16  6646  df2o3  6729  oarec  6797  limensuci  7275  infensuc  7277  phplem1  7278  sucdom2  7295  sucxpdom  7310  isinf  7314  pssnn  7319  dif1enOLD  7332  dif1en  7333  fiint  7375  pwfi  7394  dffi3  7428  sucprcreg  7559  cantnfp1lem3  7628  ranksuc  7783  pm54.43  7879  dif1card  7884  fseqenlem1  7897  cda1en  8047  ackbij1lem1  8092  ackbij1lem2  8093  ackbij1lem5  8096  ackbij1lem14  8105  cfsuc  8129  fin23lem26  8197  axdc3lem4  8325  unsnen  8420  wunsuc  8584  fzennn  11299  hashp1i  11664  dfon2lem3  25404  dfon2lem7  25408  brsuccf  25778  onsucsuccmpi  26185  onint1  26191  pwfi2f1o  27228  sucidALTVD  28919  sucidALT  28920  sucidVD  28921  bnj927  29076  bnj98  29175  bnj543  29201  bnj970  29255
  Copyright terms: Public domain W3C validator