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 6390
Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 8569). 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 6460), so that the successor of any ordinal class is still an ordinal class (ordsuc 7833), 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 6386 . 2 class suc 𝐴
31csn 4626 . . 3 class {𝐴}
41, 3cun 3949 . 2 class (𝐴 ∪ {𝐴})
52, 4wceq 1540 1 wff suc 𝐴 = (𝐴 ∪ {𝐴})
Colors of variables: wff setvar class
This definition is referenced by:  suceq  6450  elsuci  6451  elsucg  6452  elsuc2g  6453  nfsuc  6456  suc0  6459  sucprc  6460  unisucs  6461  sssucid  6464  iunsuc  6469  orddif  6480  eqfunressuc  7381  sucexb  7824  ordsuci  7828  sucexeloniOLD  7830  suceloniOLD  7832  onuninsuci  7861  omsucne  7906  tfrlem10  8427  tfrlem16  8433  df2o3  8514  oarec  8600  on2recsov  8706  naddsuc2  8739  enrefnn  9087  enpr2dOLD  9090  sucdom2OLD  9122  limensuci  9193  infensuc  9195  pssnn  9208  unfi  9211  sucdom2  9243  phplem1OLD  9254  sucxpdom  9291  isinf  9296  isinfOLD  9297  dif1ennnALT  9311  fiint  9366  fiintOLD  9367  dffi3  9471  sucprcreg  9641  cantnfp1lem3  9720  ranksuc  9905  pm54.43  10041  dif1card  10050  fseqenlem1  10064  dju1en  10212  ackbij1lem1  10259  ackbij1lem2  10260  ackbij1lem5  10263  ackbij1lem14  10272  cfsuc  10297  fin23lem26  10365  axdc3lem4  10493  unsnen  10593  wunsuc  10757  fzennn  14009  hashp1i  14442  noextend  27711  nosupbday  27750  nosupbnd1  27759  nosupbnd2lem1  27760  nosupbnd2  27761  noinfbday  27765  noinfbnd1  27774  noinfbnd2lem1  27775  noinfbnd2  27776  madeoldsuc  27923  bnj927  34783  bnj98  34881  bnj543  34907  bnj970  34961  dfon2lem3  35786  dfon2lem7  35790  brsuccf  35942  onsucsuccmpi  36444  onint1  36450  sucdifsn  38240  ressucdifsn  38246  disjsuc  38760  pwfi2f1o  43108  df3o2  43326  df3o3  43327  omcl3g  43347  oa1un  43459  grusucd  44249  sucidALTVD  44890  sucidALT  44891  sucidVD  44892
  Copyright terms: Public domain W3C validator