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 5631
Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 7475). 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 5702), so that the successor of any ordinal class is still an ordinal class (ordsuc 6883), 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 5627 . 2 class suc 𝐴
31csn 4124 . . 3 class {𝐴}
41, 3cun 3537 . 2 class (𝐴 ∪ {𝐴})
52, 4wceq 1474 1 wff suc 𝐴 = (𝐴 ∪ {𝐴})
Colors of variables: wff setvar class
This definition is referenced by:  suceq  5692  elsuci  5693  elsucg  5694  elsuc2g  5695  nfsuc  5698  suc0  5701  sucprc  5702  unisuc  5703  sssucid  5704  iunsuc  5709  orddif  5722  sucexb  6878  suceloni  6882  onuninsuci  6909  tfrlem10  7347  tfrlem16  7353  df2o3  7437  oarec  7506  limensuci  7998  infensuc  8000  phplem1  8001  sucdom2  8018  sucxpdom  8031  isinf  8035  pssnn  8040  dif1en  8055  fiint  8099  pwfi  8121  dffi3  8197  sucprcreg  8366  cantnfp1lem3  8437  ranksuc  8588  pm54.43  8686  dif1card  8693  fseqenlem1  8707  cda1en  8857  ackbij1lem1  8902  ackbij1lem2  8903  ackbij1lem5  8906  ackbij1lem14  8915  cfsuc  8939  fin23lem26  9007  axdc3lem4  9135  unsnen  9231  wunsuc  9395  fzennn  12586  hashp1i  13006  bnj927  29886  bnj98  29984  bnj543  30010  bnj970  30064  dfon2lem3  30727  dfon2lem7  30731  brsuccf  31011  onsucsuccmpi  31405  onint1  31411  pwfi2f1o  36467  df3o2  37125  df3o3  37126  sucidALTVD  37911  sucidALT  37912  sucidVD  37913
  Copyright terms: Public domain W3C validator