| Description: Define the successor of a
class. When applied to an ordinal number, the
successor means the same thing as "plus 1" (see oa1suc 7611). Definition
7.22 of [TakeutiZaring] p. 41, who
use "+ 1" to denote this function.
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 5800), so that the
successor of any ordinal class is still an ordinal class (ordsuc 7014),
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.) |
