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

Definition df-suc 4033
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 4074). 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 ∪ {A})

Detailed syntax breakdown of Definition df-suc
StepHypRef Expression
1 cA . . 3 class A
21csuc 4028 . 2 class suc A
31csn 3328 . . 3 class {A}
41, 3cun 2894 . 2 class (A ∪ {A})
52, 4wceq 1374 1 wff suc A = (A ∪ {A})
Colors of variables: wff set class
This definition is referenced by:  suceq  4064  elsuci  4065  elsucg  4066  elsuc2g  4067  nfsuc  4070  suc0  4073  sucprc  4074  unisuc  4075  unisucg  4076  sssucid  4077  iunsuc  4082  sucexb  4149  ordsucim  4152  ordsucss  4156  onsucelsucexmidlem  4174  sucprcreg  4187  elnn  4231  tfrlemisucfn  5834  rdgisuc1  5866  df2o3  5904  oasuc  5934  omsuc  5941
  Copyright terms: Public domain W3C validator