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

Definition df-suc 4263
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 4304). 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 4257 . 2  class  suc  A
31csn 3497 . . 3  class  { A }
41, 3cun 3039 . 2  class  ( A  u.  { A }
)
52, 4wceq 1316 1  wff  suc  A  =  ( A  u.  { A } )
Colors of variables: wff set class
This definition is referenced by:  suceq  4294  elsuci  4295  elsucg  4296  elsuc2g  4297  nfsuc  4300  suc0  4303  sucprc  4304  unisuc  4305  unisucg  4306  sssucid  4307  iunsuc  4312  sucexb  4383  ordsucim  4386  ordsucss  4390  2ordpr  4409  orddif  4432  sucprcreg  4434  elnn  4489  omsinds  4505  tfrlemisucfn  6189  tfr1onlemsucfn  6205  tfrcllemsucfn  6218  rdgisuc1  6249  df2o3  6295  oasuc  6328  omsuc  6336  enpr2d  6679  phplem1  6714  fiunsnnn  6743  unsnfi  6775  fiintim  6785  fidcenumlemrks  6809  fidcenumlemr  6811  pm54.43  7014  dju1en  7037  frecfzennn  10154  hashp1i  10511  ennnfonelemg  11827  ennnfonelemhdmp1  11833  ennnfonelemkh  11836  ennnfonelemhf1o  11837  bdcsuc  12974  bdeqsuc  12975  bj-sucexg  13016  bj-nntrans  13045  bj-nnelirr  13047  bj-omtrans  13050  nninfsellemdc  13102  nninfsellemsuc  13104
  Copyright terms: Public domain W3C validator