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

Definition df-suc 4587
Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 6775). 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 4656), so that the successor of any ordinal class is still an ordinal class (ordsuc 4794), 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 4583 . 2  class  suc  A
31csn 3814 . . 3  class  { A }
41, 3cun 3318 . 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  4646  elsuci  4647  elsucg  4648  elsuc2g  4649  nfsuc  4652  suc0  4655  sucprc  4656  unisuc  4657  sssucid  4658  iunsuc  4663  orddif  4675  sucexb  4789  suceloni  4793  onuninsuci  4820  tfrlem10  6648  tfrlem16  6654  df2o3  6737  oarec  6805  limensuci  7283  infensuc  7285  phplem1  7286  sucdom2  7303  sucxpdom  7318  isinf  7322  pssnn  7327  dif1enOLD  7340  dif1en  7341  fiint  7383  pwfi  7402  dffi3  7436  sucprcreg  7567  cantnfp1lem3  7636  ranksuc  7791  pm54.43  7887  dif1card  7892  fseqenlem1  7905  cda1en  8055  ackbij1lem1  8100  ackbij1lem2  8101  ackbij1lem5  8104  ackbij1lem14  8113  cfsuc  8137  fin23lem26  8205  axdc3lem4  8333  unsnen  8428  wunsuc  8592  fzennn  11307  hashp1i  11672  dfon2lem3  25412  dfon2lem7  25416  brsuccf  25786  onsucsuccmpi  26193  onint1  26199  pwfi2f1o  27237  sucidALTVD  28982  sucidALT  28983  sucidVD  28984  bnj927  29139  bnj98  29238  bnj543  29264  bnj970  29318
  Copyright terms: Public domain W3C validator