Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-suc Structured version   Visualization version   GIF version

Definition df-suc 6165
 Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 8141). 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 6234), so that the successor of any ordinal class is still an ordinal class (ordsuc 7511), 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 6161 . 2 class suc 𝐴
31csn 4525 . . 3 class {𝐴}
41, 3cun 3879 . 2 class (𝐴 ∪ {𝐴})
52, 4wceq 1538 1 wff suc 𝐴 = (𝐴 ∪ {𝐴})
 Colors of variables: wff setvar class This definition is referenced by:  suceq  6224  elsuci  6225  elsucg  6226  elsuc2g  6227  nfsuc  6230  suc0  6233  sucprc  6234  unisuc  6235  sssucid  6236  iunsuc  6241  orddif  6252  sucexb  7506  suceloni  7510  onuninsuci  7537  omsucne  7580  tfrlem10  8008  tfrlem16  8014  df2o3  8102  oarec  8173  enpr2d  8582  sucdom2  8612  limensuci  8679  infensuc  8681  phplem1  8682  sucxpdom  8713  isinf  8717  pssnn  8722  dif1en  8737  fiint  8781  pwfi  8805  dffi3  8881  sucprcreg  9051  cantnfp1lem3  9129  ranksuc  9280  pm54.43  9416  dif1card  9423  fseqenlem1  9437  dju1en  9584  ackbij1lem1  9633  ackbij1lem2  9634  ackbij1lem5  9637  ackbij1lem14  9646  cfsuc  9670  fin23lem26  9738  axdc3lem4  9866  unsnen  9966  wunsuc  10130  fzennn  13333  hashp1i  13762  bnj927  32162  bnj98  32261  bnj543  32287  bnj970  32341  eqfunressuc  33130  dfon2lem3  33155  dfon2lem7  33159  noextend  33298  nosupbday  33330  nosupbnd1  33339  nosupbnd2lem1  33340  nosupbnd2  33341  brsuccf  33527  onsucsuccmpi  33916  onint1  33922  pwfi2f1o  40055  df3o2  40742  df3o3  40743  grusucd  40953  sucidALTVD  41591  sucidALT  41592  sucidVD  41593
 Copyright terms: Public domain W3C validator