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 6368
Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 8528). 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 6438), so that the successor of any ordinal class is still an ordinal class (ordsuc 7798), 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 6364 . 2 class suc 𝐴
31csn 4628 . . 3 class {𝐴}
41, 3cun 3946 . 2 class (𝐴 ∪ {𝐴})
52, 4wceq 1542 1 wff suc 𝐴 = (𝐴 ∪ {𝐴})
Colors of variables: wff setvar class
This definition is referenced by:  suceq  6428  elsuci  6429  elsucg  6430  elsuc2g  6431  nfsuc  6434  suc0  6437  sucprc  6438  unisucs  6439  sssucid  6442  iunsuc  6447  orddif  6458  eqfunressuc  7355  sucexb  7789  ordsuci  7793  sucexeloniOLD  7795  suceloniOLD  7797  onuninsuci  7826  omsucne  7871  tfrlem10  8384  tfrlem16  8390  df2o3  8471  oarec  8559  on2recsov  8664  enrefnn  9044  enpr2dOLD  9047  sucdom2OLD  9079  limensuci  9150  infensuc  9152  pssnn  9165  unfi  9169  sucdom2  9203  phplem1OLD  9214  sucxpdom  9252  isinf  9257  isinfOLD  9258  pssnnOLD  9262  dif1ennnALT  9274  fiint  9321  pwfiOLD  9344  dffi3  9423  sucprcreg  9593  cantnfp1lem3  9672  ranksuc  9857  pm54.43  9993  dif1card  10002  fseqenlem1  10016  dju1en  10163  ackbij1lem1  10212  ackbij1lem2  10213  ackbij1lem5  10216  ackbij1lem14  10225  cfsuc  10249  fin23lem26  10317  axdc3lem4  10445  unsnen  10545  wunsuc  10709  fzennn  13930  hashp1i  14360  noextend  27159  nosupbday  27198  nosupbnd1  27207  nosupbnd2lem1  27208  nosupbnd2  27209  noinfbday  27213  noinfbnd1  27222  noinfbnd2lem1  27223  noinfbnd2  27224  madeoldsuc  27369  bnj927  33769  bnj98  33867  bnj543  33893  bnj970  33947  dfon2lem3  34746  dfon2lem7  34750  brsuccf  34902  onsucsuccmpi  35317  onint1  35323  sucdifsn  37094  ressucdifsn  37100  disjsuc  37618  pwfi2f1o  41824  df3o2  42049  df3o3  42050  omcl3g  42070  naddsuc2  42129  oa1un  42183  grusucd  42975  sucidALTVD  43617  sucidALT  43618  sucidVD  43619
  Copyright terms: Public domain W3C validator