ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-suc Unicode version

Definition df-suc 4135
Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1". 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 4176). 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 4129 . 2  class  suc  A
31csn 3402 . . 3  class  { A }
41, 3cun 2942 . 2  class  ( A  u.  { A }
)
52, 4wceq 1259 1  wff  suc  A  =  ( A  u.  { A } )
Colors of variables: wff set class
This definition is referenced by:  suceq  4166  elsuci  4167  elsucg  4168  elsuc2g  4169  nfsuc  4172  suc0  4175  sucprc  4176  unisuc  4177  unisucg  4178  sssucid  4179  iunsuc  4184  sucexb  4250  ordsucim  4253  ordsucss  4257  2ordpr  4276  orddif  4298  sucprcreg  4300  elnn  4355  tfrlemisucfn  5968  rdgisuc1  6001  df2o3  6044  oasuc  6074  omsuc  6081  phplem1  6345  fiunsnnn  6368  frecfzennn  9366  bdcsuc  10366  bdeqsuc  10367  bj-sucexg  10408  bj-nntrans  10442  bj-nnelirr  10444  bj-omtrans  10447
  Copyright terms: Public domain W3C validator