# 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 . Later, when we define complex numbers, we will be able to also define a subset of the complex numbers ( df-nn ) with analogous properties and operations, but they will be different sets. (Contributed by NM, 15-May-1994)

Ref Expression
Assertion df-om ${⊢}\mathrm{\omega }=\left\{{x}\in \mathrm{On}|\forall {y}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Lim}{y}\to {x}\in {y}\right)\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 com ${class}\mathrm{\omega }$
1 vx ${setvar}{x}$
2 con0 ${class}\mathrm{On}$
3 vy ${setvar}{y}$
4 3 cv ${setvar}{y}$
5 4 wlim ${wff}\mathrm{Lim}{y}$
6 1 cv ${setvar}{x}$
7 6 4 wcel ${wff}{x}\in {y}$
8 5 7 wi ${wff}\left(\mathrm{Lim}{y}\to {x}\in {y}\right)$
9 8 3 wal ${wff}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Lim}{y}\to {x}\in {y}\right)$
10 9 1 2 crab ${class}\left\{{x}\in \mathrm{On}|\forall {y}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Lim}{y}\to {x}\in {y}\right)\right\}$
11 0 10 wceq ${wff}\mathrm{\omega }=\left\{{x}\in \mathrm{On}|\forall {y}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Lim}{y}\to {x}\in {y}\right)\right\}$