HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Definition df-suc 2980
Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 4298). 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 affect on a proper class (sucprc 3047), so that the successor of any ordinal class is still an ordinal class (ordsuc 3170), simplifying certain proofs. 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.
Assertion
Ref Expression
df-suc |- suc A = (A u. {A})

Detailed syntax breakdown of Definition df-suc
StepHypRef Expression
1 cA . . 3 class A
21csuc 2976 . 2 class suc A
31csn 2466 . . 3 class {A}
41, 3cun 2096 . 2 class (A u. {A})
52, 4wceq 991 1 wff suc A = (A u. {A})
Colors of variables: wff set class
This definition is referenced by:  suceq 3037  elsuci 3038  elsucg 3039  elsuc2g 3040  suc0 3046  sucprc 3047  unisuc 3048  sssucid 3049  sucid 3050  orddif 3064  sucexb 3165  suceloni 3169  onuninsuci 3193  tfrlem10 4219  df2o2 4275  oarec 4330  ac6sfilem2 4587  ac6sfi 4589  limensuci 4651  phplem1 4653  pssnn 4679  unifi 4699  fiint 4701  fodomfi 4707  pwfi 4712  pm54.43 4713  sucprcreg 4741  infensuc 4782  ranksuc 4844  unsnen 4981  sucxpdom 4994  cfsuc 5063  cda1en 5076  fbssint 11521  fcluscomplem 11623
Copyright terms: Public domain