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

Definition df-suc 5767
Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 7656). Definition 7.22 of [TakeutiZaring] p. 41, who use "+ 1" to denote this function. Ordinal natural numbers defined using this successor function and 0 as the empty set are also called von Neumann ordinals; 0 is the empty set {}, 1 is {0, {0}}, 2 is {1, {1}}, and so on. 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 5838), so that the successor of any ordinal class is still an ordinal class (ordsuc 7056), 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 𝐴 = (𝐴 ∪ {𝐴})

Detailed syntax breakdown of Definition df-suc
StepHypRef Expression
1 cA . . 3 class 𝐴
21csuc 5763 . 2 class suc 𝐴
31csn 4210 . . 3 class {𝐴}
41, 3cun 3605 . 2 class (𝐴 ∪ {𝐴})
52, 4wceq 1523 1 wff suc 𝐴 = (𝐴 ∪ {𝐴})
Colors of variables: wff setvar class
This definition is referenced by:  suceq  5828  elsuci  5829  elsucg  5830  elsuc2g  5831  nfsuc  5834  suc0  5837  sucprc  5838  unisuc  5839  sssucid  5840  iunsuc  5845  orddif  5858  sucexb  7051  suceloni  7055  onuninsuci  7082  tfrlem10  7528  tfrlem16  7534  df2o3  7618  oarec  7687  limensuci  8177  infensuc  8179  phplem1  8180  sucdom2  8197  sucxpdom  8210  isinf  8214  pssnn  8219  dif1en  8234  fiint  8278  pwfi  8302  dffi3  8378  sucprcreg  8544  cantnfp1lem3  8615  ranksuc  8766  pm54.43  8864  dif1card  8871  fseqenlem1  8885  cda1en  9035  ackbij1lem1  9080  ackbij1lem2  9081  ackbij1lem5  9084  ackbij1lem14  9093  cfsuc  9117  fin23lem26  9185  axdc3lem4  9313  unsnen  9413  wunsuc  9577  fzennn  12807  hashp1i  13229  bnj927  30965  bnj98  31063  bnj543  31089  bnj970  31143  eqfunressuc  31786  dfon2lem3  31814  dfon2lem7  31818  noextend  31944  nosupbday  31976  nosupbnd1  31985  nosupbnd2lem1  31986  nosupbnd2  31987  brsuccf  32173  onsucsuccmpi  32567  onint1  32573  pwfi2f1o  37983  df3o2  38639  df3o3  38640  sucidALTVD  39420  sucidALT  39421  sucidVD  39422
  Copyright terms: Public domain W3C validator