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 6219
Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 8258). 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 6288), so that the successor of any ordinal class is still an ordinal class (ordsuc 7593), 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 6215 . 2 class suc 𝐴
31csn 4541 . . 3 class {𝐴}
41, 3cun 3864 . 2 class (𝐴 ∪ {𝐴})
52, 4wceq 1543 1 wff suc 𝐴 = (𝐴 ∪ {𝐴})
Colors of variables: wff setvar class
This definition is referenced by:  suceq  6278  elsuci  6279  elsucg  6280  elsuc2g  6281  nfsuc  6284  suc0  6287  sucprc  6288  unisuc  6289  sssucid  6290  iunsuc  6295  orddif  6306  sucexb  7588  suceloni  7592  onuninsuci  7619  omsucne  7663  tfrlem10  8123  tfrlem16  8129  df2o3  8217  oarec  8290  enrefnn  8724  enpr2d  8725  sucdom2  8755  limensuci  8822  infensuc  8824  phplem1  8825  pssnn  8846  unfi  8850  sucxpdom  8887  isinf  8891  pssnnOLD  8895  dif1enALT  8907  fiint  8948  pwfiOLD  8971  dffi3  9047  sucprcreg  9217  cantnfp1lem3  9295  ranksuc  9481  pm54.43  9617  dif1card  9624  fseqenlem1  9638  dju1en  9785  ackbij1lem1  9834  ackbij1lem2  9835  ackbij1lem5  9838  ackbij1lem14  9847  cfsuc  9871  fin23lem26  9939  axdc3lem4  10067  unsnen  10167  wunsuc  10331  fzennn  13541  hashp1i  13970  bnj927  32461  bnj98  32560  bnj543  32586  bnj970  32640  eqfunressuc  33455  dfon2lem3  33480  dfon2lem7  33484  on2recsov  33564  noextend  33606  nosupbday  33645  nosupbnd1  33654  nosupbnd2lem1  33655  nosupbnd2  33656  noinfbday  33660  noinfbnd1  33669  noinfbnd2lem1  33670  noinfbnd2  33671  madeoldsuc  33804  brsuccf  33980  onsucsuccmpi  34369  onint1  34375  pwfi2f1o  40624  df3o2  41311  df3o3  41312  grusucd  41521  sucidALTVD  42163  sucidALT  42164  sucidVD  42165
  Copyright terms: Public domain W3C validator