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

Definition df-suc 4335
Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 6463). 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 affect on a proper class (sucprc 4404), so that the successor of any ordinal class is still an ordinal class (ordsuc 4542), 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 4331 . 2  class  suc  A
31csn 3581 . . 3  class  { A }
41, 3cun 3092 . 2  class  ( A  u.  { A }
)
52, 4wceq 1619 1  wff  suc  A  =  ( A  u.  { A } )
Colors of variables: wff set class
This definition is referenced by:  suceq  4394  elsuci  4395  elsucg  4396  elsuc2g  4397  nfsuc  4400  suc0  4403  sucprc  4404  unisuc  4405  sssucid  4406  iunsuc  4411  trsuc2OLD  4414  orddif  4423  sucexb  4537  suceloni  4541  onuninsuci  4568  tfrlem10  6336  tfrlem16  6342  df2o3  6425  oarec  6493  limensuci  6970  infensuc  6972  phplem1  6973  sucdom2  6990  sucxpdom  7005  isinf  7009  pssnn  7014  dif1enOLD  7023  dif1en  7024  fiint  7066  pwfi  7084  dffi3  7117  sucprcreg  7246  cantnfp1lem3  7315  ranksuc  7470  pm54.43  7566  dif1card  7571  fseqenlem1  7584  cda1en  7734  ackbij1lem1  7779  ackbij1lem2  7780  ackbij1lem5  7783  ackbij1lem14  7792  cfsuc  7816  fin23lem26  7884  axdc3lem4  8012  unsnen  8108  wunsuc  8272  fzennn  10961  hashp1i  11299  dfon2lem3  23475  dfon2lem7  23479  brsuccf  23820  onsucsuccmpi  24222  onint1  24228  pwfi2f1o  26592  sucidALTVD  27659  sucidALT  27660  sucidVD  27661  bnj927  27812  bnj98  27911  bnj543  27937  bnj970  27991
  Copyright terms: Public domain W3C validator