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

Definition df-suc 4108
 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 4149). 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 𝐴 = (𝐴 ∪ {𝐴})

Detailed syntax breakdown of Definition df-suc
StepHypRef Expression
1 cA . . 3 class 𝐴
21csuc 4102 . 2 class suc 𝐴
31csn 3375 . . 3 class {𝐴}
41, 3cun 2915 . 2 class (𝐴 ∪ {𝐴})
52, 4wceq 1243 1 wff suc 𝐴 = (𝐴 ∪ {𝐴})
 Colors of variables: wff set class This definition is referenced by:  suceq  4139  elsuci  4140  elsucg  4141  elsuc2g  4142  nfsuc  4145  suc0  4148  sucprc  4149  unisuc  4150  unisucg  4151  sssucid  4152  iunsuc  4157  sucexb  4223  ordsucim  4226  ordsucss  4230  2ordpr  4249  orddif  4271  sucprcreg  4273  elnn  4328  tfrlemisucfn  5938  rdgisuc1  5971  df2o3  6014  oasuc  6044  omsuc  6051  phplem1  6315  fiunsnnn  6338  frecfzennn  9203  bdcsuc  10000  bdeqsuc  10001  bj-sucexg  10042  bj-nntrans  10076  bj-nnelirr  10078  bj-omtrans  10081
 Copyright terms: Public domain W3C validator