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 om 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	|- om = |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) }

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-iom

Step	Hyp	Ref	Expression
1		com 4442	. 2 class om
2		c0 3310	. . . . . 6 class (/)
3		vx	. . . . . . 7 setvar x
4	3	cv 1298	. . . . . 6 class x
5	2, 4	wcel 1448	. . . . 5 wff (/) e. x
6		vy	. . . . . . . . 9 setvar y
7	6	cv 1298	. . . . . . . 8 class y
8	7	csuc 4225	. . . . . . 7 class suc y
9	8, 4	wcel 1448	. . . . . 6 wff suc y e. x
10	9, 6, 4	wral 2375	. . . . 5 wff A. y e. x suc y e. x
11	5, 10	wa 103	. . . 4 wff ( (/) e. x /\ A. y e. x suc y e. x )
12	11, 3	cab 2086	. . 3 class { x | ( (/) e. x /\ A. y e. x suc y e. x ) }
13	12	cint 3718	. 2 class |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) }
14	1, 13	wceq 1299	1 wff om = |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) }

This definition is referenced by:  dfom3  4444