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

Definition df-suc 4172
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 4213). 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 4166 . 2  class  suc  A
31csn 3431 . . 3  class  { A }
41, 3cun 2986 . 2  class  ( A  u.  { A }
)
52, 4wceq 1287 1  wff  suc  A  =  ( A  u.  { A } )
Colors of variables: wff set class
This definition is referenced by:  suceq  4203  elsuci  4204  elsucg  4205  elsuc2g  4206  nfsuc  4209  suc0  4212  sucprc  4213  unisuc  4214  unisucg  4215  sssucid  4216  iunsuc  4221  sucexb  4287  ordsucim  4290  ordsucss  4294  2ordpr  4313  orddif  4336  sucprcreg  4338  elnn  4393  omsinds  4408  tfrlemisucfn  6043  tfr1onlemsucfn  6059  tfrcllemsucfn  6072  rdgisuc1  6103  df2o3  6149  oasuc  6179  omsuc  6187  phplem1  6520  fiunsnnn  6549  unsnfi  6581  pm54.43  6762  frecfzennn  9761  hashp1i  10115  bdcsuc  11216  bdeqsuc  11217  bj-sucexg  11258  bj-nntrans  11291  bj-nnelirr  11293  bj-omtrans  11296  nninfsellemdc  11347  nninfsellemsuc  11349
  Copyright terms: Public domain W3C validator