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

Definition df-suc 4047
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 4088). 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 4041 . 2 class suc A
31csn 3340 . . 3 class {A}
41, 3cun 2884 . 2 class (A ∪ {A})
52, 4wceq 1224 1 wff suc A = (A ∪ {A})
Colors of variables: wff set class
This definition is referenced by:  suceq  4078  elsuci  4079  elsucg  4080  elsuc2g  4081  nfsuc  4084  suc0  4087  sucprc  4088  unisuc  4089  unisucg  4090  sssucid  4091  iunsuc  4096  sucexb  4162  ordsucim  4165  ordsucss  4169  onsucelsucexmidlem  4187  sucprcreg  4200  elnn  4244  tfrlemisucfn  5848  rdgisuc1  5880  df2o3  5918  oasuc  5948  omsuc  5955  bdcsuc  8337  bdeqsuc  8338  bj-sucexg  8375  bj-nntrans  8407  bj-nnelirr  8409  bj-omtrans  8412
  Copyright terms: Public domain W3C validator