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 6391
Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 8567). Definition 7.22 of [TakeutiZaring] p. 41, who use "+ 1" to denote this function. Definition 1.4 of [Schloeder] p. 1, similarly. 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 6461), so that the successor of any ordinal class is still an ordinal class (ordsuc 7832), 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 6387 . 2 class suc 𝐴
31csn 4630 . . 3 class {𝐴}
41, 3cun 3960 . 2 class (𝐴 ∪ {𝐴})
52, 4wceq 1536 1 wff suc 𝐴 = (𝐴 ∪ {𝐴})
Colors of variables: wff setvar class
This definition is referenced by:  suceq  6451  elsuci  6452  elsucg  6453  elsuc2g  6454  nfsuc  6457  suc0  6460  sucprc  6461  unisucs  6462  sssucid  6465  iunsuc  6470  orddif  6481  eqfunressuc  7380  sucexb  7823  ordsuci  7827  sucexeloniOLD  7829  suceloniOLD  7831  onuninsuci  7860  omsucne  7905  tfrlem10  8425  tfrlem16  8431  df2o3  8512  oarec  8598  on2recsov  8704  naddsuc2  8737  enrefnn  9085  enpr2dOLD  9088  sucdom2OLD  9120  limensuci  9191  infensuc  9193  pssnn  9206  unfi  9209  sucdom2  9240  phplem1OLD  9251  sucxpdom  9288  isinf  9293  isinfOLD  9294  dif1ennnALT  9308  fiint  9363  fiintOLD  9364  dffi3  9468  sucprcreg  9638  cantnfp1lem3  9717  ranksuc  9902  pm54.43  10038  dif1card  10047  fseqenlem1  10061  dju1en  10209  ackbij1lem1  10256  ackbij1lem2  10257  ackbij1lem5  10260  ackbij1lem14  10269  cfsuc  10294  fin23lem26  10362  axdc3lem4  10490  unsnen  10590  wunsuc  10754  fzennn  14005  hashp1i  14438  noextend  27725  nosupbday  27764  nosupbnd1  27773  nosupbnd2lem1  27774  nosupbnd2  27775  noinfbday  27779  noinfbnd1  27788  noinfbnd2lem1  27789  noinfbnd2  27790  madeoldsuc  27937  bnj927  34761  bnj98  34859  bnj543  34885  bnj970  34939  dfon2lem3  35766  dfon2lem7  35770  brsuccf  35922  onsucsuccmpi  36425  onint1  36431  sucdifsn  38219  ressucdifsn  38225  disjsuc  38740  pwfi2f1o  43084  df3o2  43302  df3o3  43303  omcl3g  43323  oa1un  43435  grusucd  44225  sucidALTVD  44867  sucidALT  44868  sucidVD  44869
  Copyright terms: Public domain W3C validator