Definition df-iom 4230

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 4044. 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 4231 instead for naming consistency with set.mm. (New usage is discouraged.)

Assertion

Ref	Expression
df-iom	⊢ 𝜔 = ∩ {x ∣ (∅ ∈ x ∧ ∀y ∈ x suc y ∈ x)}

Distinct variable group:   x,y

Detailed syntax breakdown of Definition df-iom

Step	Hyp	Ref	Expression
1		com 4229	. 2 class 𝜔
2		c0 3193	. . . . . 6 class ∅
3		vx	. . . . . . 7 setvar x
4	3	cv 1223	. . . . . 6 class x
5	2, 4	wcel 1367	. . . . 5 wff ∅ ∈ x
6		vy	. . . . . . . . 9 setvar y
7	6	cv 1223	. . . . . . . 8 class y
8	7	csuc 4041	. . . . . . 7 class suc y
9	8, 4	wcel 1367	. . . . . 6 wff suc y ∈ x
10	9, 6, 4	wral 2276	. . . . 5 wff ∀y ∈ x suc y ∈ x
11	5, 10	wa 97	. . . 4 wff (∅ ∈ x ∧ ∀y ∈ x suc y ∈ x)
12	11, 3	cab 2000	. . 3 class {x ∣ (∅ ∈ x ∧ ∀y ∈ x suc y ∈ x)}
13	12	cint 3579	. 2 class ∩ {x ∣ (∅ ∈ x ∧ ∀y ∈ x suc y ∈ x)}
14	1, 13	wceq 1224	1 wff 𝜔 = ∩ {x ∣ (∅ ∈ x ∧ ∀y ∈ x suc y ∈ x)}

This definition is referenced by:  dfom3  4231