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

Definition df-suc 4162
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 4203). 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 4156 . 2  class  suc  A
31csn 3422 . . 3  class  { A }
41, 3cun 2982 . 2  class  ( A  u.  { A }
)
52, 4wceq 1285 1  wff  suc  A  =  ( A  u.  { A } )
Colors of variables: wff set class
This definition is referenced by:  suceq  4193  elsuci  4194  elsucg  4195  elsuc2g  4196  nfsuc  4199  suc0  4202  sucprc  4203  unisuc  4204  unisucg  4205  sssucid  4206  iunsuc  4211  sucexb  4277  ordsucim  4280  ordsucss  4284  2ordpr  4303  orddif  4326  sucprcreg  4328  elnn  4383  omsinds  4398  tfrlemisucfn  6021  tfr1onlemsucfn  6037  tfrcllemsucfn  6050  rdgisuc1  6081  df2o3  6127  oasuc  6157  omsuc  6165  phplem1  6498  fiunsnnn  6527  unsnfi  6556  pm54.43  6721  frecfzennn  9722  hashp1i  10053  bdcsuc  11114  bdeqsuc  11115  bj-sucexg  11156  bj-nntrans  11189  bj-nnelirr  11191  bj-omtrans  11194  nninfsellemdc  11243  nninfsellemsuc  11245
  Copyright terms: Public domain W3C validator