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

Definition df-suc 4414
Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 6546). Definition 7.22 of [TakeutiZaring] p. 41, who use "+ 1" to denote this function. 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 4483), so that the successor of any ordinal class is still an ordinal class (ordsuc 4621), 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  A  =  ( A  u.  { A } )

Detailed syntax breakdown of Definition df-suc
StepHypRef Expression
1 cA . . 3  class  A
21csuc 4410 . 2  class  suc  A
31csn 3653 . . 3  class  { A }
41, 3cun 3163 . 2  class  ( A  u.  { A }
)
52, 4wceq 1632 1  wff  suc  A  =  ( A  u.  { A } )
Colors of variables: wff set class
This definition is referenced by:  suceq  4473  elsuci  4474  elsucg  4475  elsuc2g  4476  nfsuc  4479  suc0  4482  sucprc  4483  unisuc  4484  sssucid  4485  iunsuc  4490  trsuc2OLD  4493  orddif  4502  sucexb  4616  suceloni  4620  onuninsuci  4647  tfrlem10  6419  tfrlem16  6425  df2o3  6508  oarec  6576  limensuci  7053  infensuc  7055  phplem1  7056  sucdom2  7073  sucxpdom  7088  isinf  7092  pssnn  7097  dif1enOLD  7106  dif1en  7107  fiint  7149  pwfi  7167  dffi3  7200  sucprcreg  7329  cantnfp1lem3  7398  ranksuc  7553  pm54.43  7649  dif1card  7654  fseqenlem1  7667  cda1en  7817  ackbij1lem1  7862  ackbij1lem2  7863  ackbij1lem5  7866  ackbij1lem14  7875  cfsuc  7899  fin23lem26  7967  axdc3lem4  8095  unsnen  8191  wunsuc  8355  fzennn  11046  hashp1i  11385  dfon2lem3  24212  dfon2lem7  24216  brsuccf  24551  onsucsuccmpi  24954  onint1  24960  pwfi2f1o  27363  sucidALTVD  28962  sucidALT  28963  sucidVD  28964  bnj927  29116  bnj98  29215  bnj543  29241  bnj970  29295
  Copyright terms: Public domain W3C validator