Metamath Proof Explorer


Definition df-om

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 dfom2 for an alternate definition. Later, when we assume the Axiom of Infinity, we show _om is a set in omex , and _om can then be defined per dfom3 (the smallest inductive set) and dfom4 .

Note: the natural numbers _om are a subset of the ordinal numbers df-on . They are completely different from the natural numbers NN ( df-nn ) 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)

Ref Expression
Assertion df-om ω = x On | y Lim y x y

Detailed syntax breakdown

Step Hyp Ref Expression
0 com class ω
1 vx setvar x
2 con0 class On
3 vy setvar y
4 3 cv setvar y
5 4 wlim wff Lim y
6 1 cv setvar x
7 6 4 wcel wff x y
8 5 7 wi wff Lim y x y
9 8 3 wal wff y Lim y x y
10 9 1 2 crab class x On | y Lim y x y
11 0 10 wceq wff ω = x On | y Lim y x y