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 6191
Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 8147). 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 6260), so that the successor of any ordinal class is still an ordinal class (ordsuc 7517), 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 6187 . 2 class suc 𝐴
31csn 4559 . . 3 class {𝐴}
41, 3cun 3933 . 2 class (𝐴 ∪ {𝐴})
52, 4wceq 1528 1 wff suc 𝐴 = (𝐴 ∪ {𝐴})
Colors of variables: wff setvar class
This definition is referenced by:  suceq  6250  elsuci  6251  elsucg  6252  elsuc2g  6253  nfsuc  6256  suc0  6259  sucprc  6260  unisuc  6261  sssucid  6262  iunsuc  6267  orddif  6278  sucexb  7512  suceloni  7516  onuninsuci  7543  omsucne  7586  tfrlem10  8014  tfrlem16  8020  df2o3  8108  oarec  8178  enpr2d  8586  limensuci  8682  infensuc  8684  phplem1  8685  sucdom2  8703  sucxpdom  8716  isinf  8720  pssnn  8725  dif1en  8740  fiint  8784  pwfi  8808  dffi3  8884  sucprcreg  9054  cantnfp1lem3  9132  ranksuc  9283  pm54.43  9418  dif1card  9425  fseqenlem1  9439  dju1en  9586  ackbij1lem1  9631  ackbij1lem2  9632  ackbij1lem5  9635  ackbij1lem14  9644  cfsuc  9668  fin23lem26  9736  axdc3lem4  9864  unsnen  9964  wunsuc  10128  fzennn  13326  hashp1i  13754  bnj927  31940  bnj98  32039  bnj543  32065  bnj970  32119  eqfunressuc  32903  dfon2lem3  32928  dfon2lem7  32932  noextend  33071  nosupbday  33103  nosupbnd1  33112  nosupbnd2lem1  33113  nosupbnd2  33114  brsuccf  33300  onsucsuccmpi  33689  onint1  33695  pwfi2f1o  39576  df3o2  40254  df3o3  40255  grusucd  40446  sucidALTVD  41084  sucidALT  41085  sucidVD  41086
  Copyright terms: Public domain W3C validator