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

Definition df-suc 4871
Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 7180). 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 4940), so that the successor of any ordinal class is still an ordinal class (ordsuc 6631), 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 4867 . 2  class  suc  A
31csn 4011 . . 3  class  { A }
41, 3cun 3457 . 2  class  ( A  u.  { A }
)
52, 4wceq 1381 1  wff  suc  A  =  ( A  u.  { A } )
Colors of variables: wff setvar class
This definition is referenced by:  suceq  4930  elsuci  4931  elsucg  4932  elsuc2g  4933  nfsuc  4936  suc0  4939  sucprc  4940  unisuc  4941  sssucid  4942  iunsuc  4947  orddif  4958  sucexb  6626  suceloni  6630  onuninsuci  6657  tfrlem10  7055  tfrlem16  7061  df2o3  7142  oarec  7210  limensuci  7692  infensuc  7694  phplem1  7695  sucdom2  7713  sucxpdom  7728  isinf  7732  pssnn  7737  dif1enOLD  7751  dif1en  7752  fiint  7796  pwfi  7814  dffi3  7890  sucprcreg  8025  sucprcregOLD  8026  cantnfp1lem3  8099  cantnfp1lem3OLD  8125  ranksuc  8283  pm54.43  8381  dif1card  8388  fseqenlem1  8405  cda1en  8555  ackbij1lem1  8600  ackbij1lem2  8601  ackbij1lem5  8604  ackbij1lem14  8613  cfsuc  8637  fin23lem26  8705  axdc3lem4  8833  unsnen  8928  wunsuc  9095  fzennn  12054  hashp1i  12444  dfon2lem3  29189  dfon2lem7  29193  brsuccf  29563  onsucsuccmpi  29880  onint1  29886  pwfi2f1o  31016  sucidALTVD  33398  sucidALT  33399  sucidVD  33400  bnj927  33555  bnj98  33653  bnj543  33679  bnj970  33733
  Copyright terms: Public domain W3C validator