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

Definition df-suc 4074
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 4115). 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 4068 . 2 class suc A
31csn 3367 . . 3 class {A}
41, 3cun 2909 . 2 class (A ∪ {A})
52, 4wceq 1242 1 wff suc A = (A ∪ {A})
Colors of variables: wff set class
This definition is referenced by:  suceq  4105  elsuci  4106  elsucg  4107  elsuc2g  4108  nfsuc  4111  suc0  4114  sucprc  4115  unisuc  4116  unisucg  4117  sssucid  4118  iunsuc  4123  sucexb  4189  ordsucim  4192  ordsucss  4196  onsucelsucexmidlem  4214  sucprcreg  4227  elnn  4271  tfrlemisucfn  5879  rdgisuc1  5911  df2o3  5953  oasuc  5983  omsuc  5990  frecfzennn  8844  bdcsuc  9269  bdeqsuc  9270  bj-sucexg  9307  bj-nntrans  9339  bj-nnelirr  9341  bj-omtrans  9344
  Copyright terms: Public domain W3C validator