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

Definition df-suc 5646
 Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 7498). 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 5717), so that the successor of any ordinal class is still an ordinal class (ordsuc 6906), 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 5642 . 2 class suc 𝐴
31csn 4125 . . 3 class {𝐴}
41, 3cun 3538 . 2 class (𝐴 ∪ {𝐴})
52, 4wceq 1475 1 wff suc 𝐴 = (𝐴 ∪ {𝐴})
 Colors of variables: wff setvar class This definition is referenced by:  suceq  5707  elsuci  5708  elsucg  5709  elsuc2g  5710  nfsuc  5713  suc0  5716  sucprc  5717  unisuc  5718  sssucid  5719  iunsuc  5724  orddif  5737  sucexb  6901  suceloni  6905  onuninsuci  6932  tfrlem10  7370  tfrlem16  7376  df2o3  7460  oarec  7529  limensuci  8021  infensuc  8023  phplem1  8024  sucdom2  8041  sucxpdom  8054  isinf  8058  pssnn  8063  dif1en  8078  fiint  8122  pwfi  8144  dffi3  8220  sucprcreg  8389  cantnfp1lem3  8460  ranksuc  8611  pm54.43  8709  dif1card  8716  fseqenlem1  8730  cda1en  8880  ackbij1lem1  8925  ackbij1lem2  8926  ackbij1lem5  8929  ackbij1lem14  8938  cfsuc  8962  fin23lem26  9030  axdc3lem4  9158  unsnen  9254  wunsuc  9418  fzennn  12629  hashp1i  13052  bnj927  30093  bnj98  30191  bnj543  30217  bnj970  30271  dfon2lem3  30934  dfon2lem7  30938  brsuccf  31218  onsucsuccmpi  31612  onint1  31618  pwfi2f1o  36684  df3o2  37342  df3o3  37343  sucidALTVD  38128  sucidALT  38129  sucidVD  38130
 Copyright terms: Public domain W3C validator