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

Definition df-suc 4302
 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 4343). 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 4296 . 2 class suc 𝐴
31csn 3533 . . 3 class {𝐴}
41, 3cun 3075 . 2 class (𝐴 ∪ {𝐴})
52, 4wceq 1332 1 wff suc 𝐴 = (𝐴 ∪ {𝐴})
 Colors of variables: wff set class This definition is referenced by:  suceq  4333  elsuci  4334  elsucg  4335  elsuc2g  4336  nfsuc  4339  suc0  4342  sucprc  4343  unisuc  4344  unisucg  4345  sssucid  4346  iunsuc  4351  sucexb  4422  ordsucim  4425  ordsucss  4429  2ordpr  4448  orddif  4471  sucprcreg  4473  elnn  4528  omsinds  4544  tfrlemisucfn  6230  tfr1onlemsucfn  6246  tfrcllemsucfn  6259  rdgisuc1  6290  df2o3  6336  oasuc  6369  omsuc  6377  enpr2d  6720  phplem1  6755  fiunsnnn  6784  unsnfi  6817  fiintim  6827  fidcenumlemrks  6851  fidcenumlemr  6853  pm54.43  7066  dju1en  7089  pw1nel3  7102  sucpw1nel3  7104  frecfzennn  10250  hashp1i  10608  ennnfonelemg  11972  ennnfonelemhdmp1  11978  ennnfonelemkh  11981  ennnfonelemhf1o  11982  bdcsuc  13269  bdeqsuc  13270  bj-sucexg  13311  bj-nntrans  13340  bj-nnelirr  13342  bj-omtrans  13345  nninfsellemdc  13400  nninfsellemsuc  13402
 Copyright terms: Public domain W3C validator