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

Definition df-suc 5439
Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 7232). 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 5508), so that the successor of any ordinal class is still an ordinal class (ordsuc 6646), 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 5435 . 2  class  suc  A
31csn 3993 . . 3  class  { A }
41, 3cun 3431 . 2  class  ( A  u.  { A }
)
52, 4wceq 1437 1  wff  suc  A  =  ( A  u.  { A } )
Colors of variables: wff setvar class
This definition is referenced by:  suceq  5498  elsuci  5499  elsucg  5500  elsuc2g  5501  nfsuc  5504  suc0  5507  sucprc  5508  unisuc  5509  sssucid  5510  iunsuc  5515  orddif  5526  sucexb  6641  suceloni  6645  onuninsuci  6672  tfrlem10  7104  tfrlem16  7110  df2o3  7194  oarec  7262  limensuci  7745  infensuc  7747  phplem1  7748  sucdom2  7765  sucxpdom  7778  isinf  7782  pssnn  7787  dif1en  7801  fiint  7845  pwfi  7866  dffi3  7942  sucprcreg  8105  cantnfp1lem3  8175  ranksuc  8326  pm54.43  8424  dif1card  8431  fseqenlem1  8444  cda1en  8594  ackbij1lem1  8639  ackbij1lem2  8640  ackbij1lem5  8643  ackbij1lem14  8652  cfsuc  8676  fin23lem26  8744  axdc3lem4  8872  unsnen  8967  wunsuc  9131  fzennn  12167  hashp1i  12566  bnj927  29365  bnj98  29463  bnj543  29489  bnj970  29543  dfon2lem3  30215  dfon2lem7  30219  brsuccf  30490  onsucsuccmpi  30885  onint1  30891  pwfi2f1o  35664  sucidALTVD  36911  sucidALT  36912  sucidVD  36913
  Copyright terms: Public domain W3C validator