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

Definition df-suc 5384
Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 7181). 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 5453), so that the successor of any ordinal class is still an ordinal class (ordsuc 6592), 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 5380 . 2  class  suc  A
31csn 3934 . . 3  class  { A }
41, 3cun 3370 . 2  class  ( A  u.  { A }
)
52, 4wceq 1437 1  wff  suc  A  =  ( A  u.  { A } )
Colors of variables: wff setvar class
This definition is referenced by:  suceq  5443  elsuci  5444  elsucg  5445  elsuc2g  5446  nfsuc  5449  suc0  5452  sucprc  5453  unisuc  5454  sssucid  5455  iunsuc  5460  orddif  5471  sucexb  6587  suceloni  6591  onuninsuci  6618  tfrlem10  7053  tfrlem16  7059  df2o3  7143  oarec  7211  limensuci  7694  infensuc  7696  phplem1  7697  sucdom2  7714  sucxpdom  7727  isinf  7731  pssnn  7736  dif1en  7750  fiint  7794  pwfi  7815  dffi3  7891  sucprcreg  8060  cantnfp1lem3  8130  ranksuc  8281  pm54.43  8379  dif1card  8386  fseqenlem1  8399  cda1en  8549  ackbij1lem1  8594  ackbij1lem2  8595  ackbij1lem5  8598  ackbij1lem14  8607  cfsuc  8631  fin23lem26  8699  axdc3lem4  8827  unsnen  8922  wunsuc  9086  fzennn  12124  hashp1i  12523  bnj927  29525  bnj98  29623  bnj543  29649  bnj970  29703  dfon2lem3  30375  dfon2lem7  30379  brsuccf  30650  onsucsuccmpi  31045  onint1  31051  pwfi2f1o  35861  sucidALTVD  37177  sucidALT  37178  sucidVD  37179
  Copyright terms: Public domain W3C validator