Description: Define the class of
natural numbers, which are all ordinal numbers that
are less than every limit ordinal, i.e. all finite ordinals. Our
definition is a variant of the Definition of N of [BellMachover]
p. 471. See dfom26702 for an alternate definition. Later, when we
assume
the Axiom of Infinity, we show is a set in omex8081,
and
can then be defined per dfom38085 (the smallest inductive set) and
dfom48087.

Note: the natural numbers are a subset of the
ordinal numbers
df-on4887. They are completely different from the
natural numbers
(df-nn10562) that are a subset of the complex numbers
defined much later
in our development, although the two sets have analogous properties and
operations defined on them. (Contributed by NM,
15-May-1994.)