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

Definition df-suc 4696
 Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 6932). 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 4765), so that the successor of any ordinal class is still an ordinal class (ordsuc 6395), 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

Detailed syntax breakdown of Definition df-suc
StepHypRef Expression
1 cA . . 3
21csuc 4692 . 2
31csn 3853 . . 3
41, 3cun 3303 . 2
52, 4wceq 1687 1
 Colors of variables: wff setvar class This definition is referenced by:  suceq  4755  elsuci  4756  elsucg  4757  elsuc2g  4758  nfsuc  4761  suc0  4764  sucprc  4765  unisuc  4766  sssucid  4767  iunsuc  4772  orddif  4783  sucexb  6390  suceloni  6394  onuninsuci  6421  tfrlem10  6805  tfrlem16  6811  df2o3  6894  oarec  6962  limensuci  7446  infensuc  7448  phplem1  7449  sucdom2  7466  sucxpdom  7481  isinf  7485  pssnn  7490  dif1enOLD  7503  dif1en  7504  fiint  7547  pwfi  7565  dffi3  7628  sucprcreg  7761  sucprcregOLD  7762  cantnfp1lem3  7835  cantnfp1lem3OLD  7861  ranksuc  8019  pm54.43  8117  dif1card  8124  fseqenlem1  8141  cda1en  8291  ackbij1lem1  8336  ackbij1lem2  8337  ackbij1lem5  8340  ackbij1lem14  8349  cfsuc  8373  fin23lem26  8441  axdc3lem4  8569  unsnen  8664  wunsuc  8830  fzennn  11731  hashp1i  12102  dfon2lem3  27300  dfon2lem7  27304  brsuccf  27674  onsucsuccmpi  27992  onint1  27998  pwfi2f1o  29124  sucidALTVD  31184  sucidALT  31185  sucidVD  31186  bnj927  31340  bnj98  31438  bnj543  31464  bnj970  31518
 Copyright terms: Public domain W3C validator