Definition df-suc

Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc ). Definition 7.22 of TakeutiZaring p. 41, who use "+ 1" to denote this function. Definition 1.4 of Schloeder p. 1, similarly. Ordinal natural numbers defined using this successor function and 0 as the empty set are also called von Neumann ordinals; 0 is the empty set {}, 1 is {0, {0}}, 2 is {1, {1}}, and so on. 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 ), so that the successor of any ordinal class is still an ordinal class ( ordsuc ), 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. (Contributed by NM, 30-Aug-1993)

	Ref	Expression
Assertion	df-suc	$$⊢\mathrm{suc}A=A\cup \left\{A\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1	0	csuc	$$class\mathrm{suc}A$$
2	0	csn	$$class\left\{A\right\}$$
3	0 2	cun	$$class\left(A\cup \left\{A\right\}\right)$$
4	1 3	wceq	$$wff\mathrm{suc}A=A\cup \left\{A\right\}$$