Definition df-iom 4443

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 4228. Later, when we define complex numbers, we will be able to also define a subset of the complex numbers with analogous properties and operations, but they will be different sets. (Contributed by NM, 6-Aug-1994.) Use its alias dfom3 4444 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 4442	. 2 class ω
2		c0 3310	. . . . . 6 class ∅
3		vx	. . . . . . 7 setvar 𝑥
4	3	cv 1298	. . . . . 6 class 𝑥
5	2, 4	wcel 1448	. . . . 5 wff ∅ ∈ 𝑥
6		vy	. . . . . . . . 9 setvar 𝑦
7	6	cv 1298	. . . . . . . 8 class 𝑦
8	7	csuc 4225	. . . . . . 7 class suc 𝑦
9	8, 4	wcel 1448	. . . . . 6 wff suc 𝑦 ∈ 𝑥
10	9, 6, 4	wral 2375	. . . . 5 wff ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥
11	5, 10	wa 103	. . . 4 wff (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
12	11, 3	cab 2086	. . 3 class {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)}
13	12	cint 3718	. 2 class ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)}
14	1, 13	wceq 1299	1 wff ω = ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)}

This definition is referenced by:  dfom3  4444