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	⊢ ω = { 𝑥 ∈ On ∣ ∀ 𝑦 ( Lim 𝑦 → 𝑥 ∈ 𝑦 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		com	⊢ ω
1		vx	⊢ 𝑥
2		con0	⊢ On
3		vy	⊢ 𝑦
4	3	cv	⊢ 𝑦
5	4	wlim	⊢ Lim 𝑦
6	1	cv	⊢ 𝑥
7	6 4	wcel	⊢ 𝑥 ∈ 𝑦
8	5 7	wi	⊢ ( Lim 𝑦 → 𝑥 ∈ 𝑦 )
9	8 3	wal	⊢ ∀ 𝑦 ( Lim 𝑦 → 𝑥 ∈ 𝑦 )
10	9 1 2	crab	⊢ { 𝑥 ∈ On ∣ ∀ 𝑦 ( Lim 𝑦 → 𝑥 ∈ 𝑦 ) }
11	0 10	wceq	⊢ ω = { 𝑥 ∈ On ∣ ∀ 𝑦 ( Lim 𝑦 → 𝑥 ∈ 𝑦 ) }