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

Definition df-suc 4057
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 4098). 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 4051 . 2 class suc A
31csn 3350 . . 3 class {A}
41, 3cun 2892 . 2 class (A ∪ {A})
52, 4wceq 1228 1 wff suc A = (A ∪ {A})
Colors of variables: wff set class
This definition is referenced by:  suceq  4088  elsuci  4089  elsucg  4090  elsuc2g  4091  nfsuc  4094  suc0  4097  sucprc  4098  unisuc  4099  unisucg  4100  sssucid  4101  iunsuc  4106  sucexb  4173  ordsucim  4176  ordsucss  4180  onsucelsucexmidlem  4198  sucprcreg  4211  elnn  4255  tfrlemisucfn  5859  rdgisuc1  5891  df2o3  5929  oasuc  5959  omsuc  5966  bdcsuc  7107  bdeqsuc  7108  bj-sucexg  7145  bj-nntrans  7173  bj-nnelirr  7175  bj-omtrans  7178
  Copyright terms: Public domain W3C validator