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

Definition df-suc 4300
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 4341). 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 4294 . 2  class  suc  A
31csn 3531 . . 3  class  { A }
41, 3cun 3073 . 2  class  ( A  u.  { A }
)
52, 4wceq 1332 1  wff  suc  A  =  ( A  u.  { A } )
Colors of variables: wff set class
This definition is referenced by:  suceq  4331  elsuci  4332  elsucg  4333  elsuc2g  4334  nfsuc  4337  suc0  4340  sucprc  4341  unisuc  4342  unisucg  4343  sssucid  4344  iunsuc  4349  sucexb  4420  ordsucim  4423  ordsucss  4427  2ordpr  4446  orddif  4469  sucprcreg  4471  elnn  4526  omsinds  4542  tfrlemisucfn  6228  tfr1onlemsucfn  6244  tfrcllemsucfn  6257  rdgisuc1  6288  df2o3  6334  oasuc  6367  omsuc  6375  enpr2d  6718  phplem1  6753  fiunsnnn  6782  unsnfi  6814  fiintim  6824  fidcenumlemrks  6848  fidcenumlemr  6850  pm54.43  7062  dju1en  7085  frecfzennn  10229  hashp1i  10587  ennnfonelemg  11950  ennnfonelemhdmp1  11956  ennnfonelemkh  11959  ennnfonelemhf1o  11960  bdcsuc  13247  bdeqsuc  13248  bj-sucexg  13289  bj-nntrans  13318  bj-nnelirr  13320  bj-omtrans  13323  nninfsellemdc  13379  nninfsellemsuc  13381
  Copyright terms: Public domain W3C validator