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 5949
Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 7851). 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 6019), so that the successor of any ordinal class is still an ordinal class (ordsuc 7247), 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 5945 . 2 class suc 𝐴
31csn 4377 . . 3 class {𝐴}
41, 3cun 3774 . 2 class (𝐴 ∪ {𝐴})
52, 4wceq 1637 1 wff suc 𝐴 = (𝐴 ∪ {𝐴})
Colors of variables: wff setvar class
This definition is referenced by:  suceq  6009  elsuci  6010  elsucg  6011  elsuc2g  6012  nfsuc  6015  suc0  6018  sucprc  6019  unisuc  6020  sssucid  6021  iunsuc  6026  orddif  6037  sucexb  7242  suceloni  7246  onuninsuci  7273  tfrlem10  7722  tfrlem16  7728  df2o3  7813  oarec  7882  limensuci  8378  infensuc  8380  phplem1  8381  sucdom2  8398  sucxpdom  8411  isinf  8415  pssnn  8420  dif1en  8435  fiint  8479  pwfi  8503  dffi3  8579  sucprcreg  8748  cantnfp1lem3  8827  ranksuc  8978  pm54.43  9112  dif1card  9119  fseqenlem1  9133  cda1en  9285  ackbij1lem1  9330  ackbij1lem2  9331  ackbij1lem5  9334  ackbij1lem14  9343  cfsuc  9367  fin23lem26  9435  axdc3lem4  9563  unsnen  9663  wunsuc  9827  fzennn  12994  hashp1i  13411  bnj927  31167  bnj98  31265  bnj543  31291  bnj970  31345  eqfunressuc  31987  dfon2lem3  32015  dfon2lem7  32019  noextend  32145  nosupbday  32177  nosupbnd1  32186  nosupbnd2lem1  32187  nosupbnd2  32188  brsuccf  32374  onsucsuccmpi  32764  onint1  32770  pwfi2f1o  38168  df3o2  38823  df3o3  38824  sucidALTVD  39601  sucidALT  39602  sucidVD  39603
  Copyright terms: Public domain W3C validator