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

Definition df-suc 4291
 Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 6416). 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 affect on a proper class (sucprc 4360), so that the successor of any ordinal class is still an ordinal class (ordsuc 4496), 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 4287 . 2
31csn 3544 . . 3
41, 3cun 3076 . 2
52, 4wceq 1619 1
 Colors of variables: wff set class This definition is referenced by:  suceq  4350  elsuci  4351  elsucg  4352  elsuc2g  4353  nfsuc  4356  suc0  4359  sucprc  4360  unisuc  4361  sssucid  4362  iunsuc  4367  trsuc2OLD  4370  orddif  4379  sucexb  4491  suceloni  4495  onuninsuci  4522  tfrlem10  6289  tfrlem16  6295  df2o3  6378  oarec  6446  limensuci  6922  infensuc  6924  phplem1  6925  sucdom2  6942  sucxpdom  6957  isinf  6961  pssnn  6966  dif1enOLD  6975  dif1en  6976  fiint  7018  pwfi  7035  dffi3  7068  sucprcreg  7197  cantnfp1lem3  7266  ranksuc  7421  pm54.43  7517  dif1card  7522  fseqenlem1  7535  cda1en  7685  ackbij1lem1  7730  ackbij1lem2  7731  ackbij1lem5  7734  ackbij1lem14  7743  cfsuc  7767  fin23lem26  7835  axdc3lem4  7963  unsnen  8057  wunsuc  8219  fzennn  10908  hashp1i  11246  dfon2lem3  23309  dfon2lem7  23313  brsuccf  23654  onsucsuccmpi  24056  onint1  24062  pwfi2f1o  26426  sucidALTVD  27336  sucidALT  27337  sucidVD  27338  bnj927  27489  bnj98  27588  bnj543  27614  bnj970  27668
 Copyright terms: Public domain W3C validator