Definition df-n 4423

Description: The natural numbers of analysis start at one (unlike the natural numbers of set theory, i.e. the members of set omega, which start at zero). This is the convention used by most analysis books, and it also convenient for proofs in that we never have to worry about division by zero. See nnind 4434 for the principle of mathematical induction. Definition of positive integers in [Apostol] p. 22.

Assertion

Ref	Expression
df-n	⊢ ℕ = ∩{x∣(1 ∈ x ∧ ∀y(y ∈ x → (y + 1) ∈ x))}

Distinct variable group(s):   x,y

Detailed syntax breakdown of Definition df-n

Step	Hyp	Ref	Expression
1		cn 4093	. 2 class ℕ
2		c1 4029	. . . . . 6 class 1
3		vx	. . . . . . 7 set x
4	3	cv 1089	. . . . . 6 class x
5	2, 4	wcel 1092	. . . . 5 wff 1 ∈ x
6		vy	. . . . . . . 8 set y
7	6, 3	wel 803	. . . . . . 7 wff y ∈ x
8	6	cv 1089	. . . . . . . . 9 class y
9		caddc 4031	. . . . . . . . 9 class +
10	8, 2, 9	co 3001	. . . . . . . 8 class (y + 1)
11	10, 4	wcel 1092	. . . . . . 7 wff (y + 1) ∈ x
12	7, 11	wi 2	. . . . . 6 wff (y ∈ x → (y + 1) ∈ x)
13	12, 6	wal 672	. . . . 5 wff ∀y(y ∈ x → (y + 1) ∈ x)
14	5, 13	wa 196	. . . 4 wff (1 ∈ x ∧ ∀y(y ∈ x → (y + 1) ∈ x))
15	14, 3	cab 1090	. . 3 class {x∣(1 ∈ x ∧ ∀y(y ∈ x → (y + 1) ∈ x))}
16	15	cint 1965	. 2 class ∩{x∣(1 ∈ x ∧ ∀y(y ∈ x → (y + 1) ∈ x))}
17	1, 16	wceq 1091	1 wff ℕ = ∩{x∣(1 ∈ x ∧ ∀y(y ∈ x → (y + 1) ∈ x))}

This definition is referenced by:  peano5nn 4424  1nn 4432  peano2nn 4433

metamath.org