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

Definition df-suc 5452
Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 7264). 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 5521), so that the successor of any ordinal class is still an ordinal class (ordsuc 6673), 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 5448 . 2  class  suc  A
31csn 3980 . . 3  class  { A }
41, 3cun 3414 . 2  class  ( A  u.  { A }
)
52, 4wceq 1455 1  wff  suc  A  =  ( A  u.  { A } )
Colors of variables: wff setvar class
This definition is referenced by:  suceq  5511  elsuci  5512  elsucg  5513  elsuc2g  5514  nfsuc  5517  suc0  5520  sucprc  5521  unisuc  5522  sssucid  5523  iunsuc  5528  orddif  5539  sucexb  6668  suceloni  6672  onuninsuci  6699  tfrlem10  7136  tfrlem16  7142  df2o3  7226  oarec  7294  limensuci  7779  infensuc  7781  phplem1  7782  sucdom2  7799  sucxpdom  7812  isinf  7816  pssnn  7821  dif1en  7835  fiint  7879  pwfi  7900  dffi3  7976  sucprcreg  8145  cantnfp1lem3  8216  ranksuc  8367  pm54.43  8465  dif1card  8472  fseqenlem1  8486  cda1en  8636  ackbij1lem1  8681  ackbij1lem2  8682  ackbij1lem5  8685  ackbij1lem14  8694  cfsuc  8718  fin23lem26  8786  axdc3lem4  8914  unsnen  9009  wunsuc  9173  fzennn  12219  hashp1i  12618  bnj927  29630  bnj98  29728  bnj543  29754  bnj970  29808  dfon2lem3  30481  dfon2lem7  30485  brsuccf  30758  onsucsuccmpi  31153  onint1  31159  pwfi2f1o  36000  sucidALTVD  37308  sucidALT  37309  sucidVD  37310
  Copyright terms: Public domain W3C validator