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	|- _om = { x e. On | A. y ( Lim y -> x e. y ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		com	|- _om
1		vx	|- x
2		con0	|- On
3		vy	|- y
4	3	cv	|- y
5	4	wlim	|- Lim y
6	1	cv	|- x
7	6 4	wcel	|- x e. y
8	5 7	wi	|- ( Lim y -> x e. y )
9	8 3	wal	|- A. y ( Lim y -> x e. y )
10	9 1 2	crab	|- { x e. On | A. y ( Lim y -> x e. y ) }
11	0 10	wceq	|- _om = { x e. On | A. y ( Lim y -> x e. y ) }