Definition df-iom 4713

Description: Define the class of natural numbers as the smallest inductive set, which is valid provided we assume the Axiom of Infinity. Definition 6.3 of [Eisenberg] p. 82.

Note: the natural numbers ω are a subset of the ordinal numbers df-on 4489. Later, when we define complex numbers, we will be able to also define a subset of the complex numbers (df-inn 9238) with analogous properties and operations, but they will be different sets.

We are unable to use the terms finite ordinal and natural number interchangeably, as shown at exmidonfin 7497. (Contributed by NM, 6-Aug-1994.) Use its alias dfom3 4714 instead for naming consistency with set.mm. (New usage is discouraged.)

Assertion

Ref	Expression
df-iom	⊢ ω = ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)}

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-iom

Step	Hyp	Ref	Expression
1		com 4712	. 2 class ω
2		c0 3508	. . . . . 6 class ∅
3		vx	. . . . . . 7 setvar 𝑥
4	3	cv 1397	. . . . . 6 class 𝑥
5	2, 4	wcel 2203	. . . . 5 wff ∅ ∈ 𝑥
6		vy	. . . . . . . . 9 setvar 𝑦
7	6	cv 1397	. . . . . . . 8 class 𝑦
8	7	csuc 4486	. . . . . . 7 class suc 𝑦
9	8, 4	wcel 2203	. . . . . 6 wff suc 𝑦 ∈ 𝑥
10	9, 6, 4	wral 2520	. . . . 5 wff ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥
11	5, 10	wa 104	. . . 4 wff (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
12	11, 3	cab 2218	. . 3 class {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)}
13	12	cint 3949	. 2 class ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)}
14	1, 13	wceq 1398	1 wff ω = ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)}

This definition is referenced by:  dfom3  4714