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\left(\mathrm{Lim}y\to x\in y\right)\right\}$$

Detailed syntax breakdown

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