Definition df-suc 2205

Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 3132). 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 2297), so that the successor of any ordinal class is still an ordinal class (ordsuc 2318), 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

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	csuc 2201	. 2 class suc A
3	1	csn 1808	. . 3 class {A}
4	1, 3	cun 1485	. 2 class (A u. {A})
5	2, 4	wceq 1091	1 wff suc A = (A u. {A})

This definition is referenced by:  suceq 2288  elsuci 2289  elsucg 2290  elsuc2g 2291  sucprc 2297  unisuc 2299  sssucid 2300  sucexb 2301  sucid 2304  suceloni 2314  orddif 2326  onuninsuc 2356  tfrlem10 2958  df1o2 3111  df2o2 3112  limensuci 3401  phplem2 3404  pssnn 3428  fiint 3445  sucprcreg 3451  infensuc 3484  sucxpdom 3652  cfsuc 3709  cda1en 3721

metamath.org