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