Definition df-n 5931

Description: The natural numbers of analysis start at one (unlike the ordinal natural numbers, i.e. the members of the set ω, df-om 3146, which start at zero). This is the convention used by most analysis books, and it is often convenient in proofs because we don't have to worry about division by zero. See nnind 5943 for the principle of mathematical induction. See dfnn2 5942 for a slight variant. See df-n0 6106 for the set of nonnegative integers ℕ₀ starting at zero. See dfn2 6118 for ℕ defined in terms of ℕ₀.

Assertion

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

Distinct variable group:   x,y

Detailed syntax breakdown of Definition df-n

Step	Hyp	Ref	Expression
1		cn 5309	. 2 class ℕ
2		c1 5248	. . . . . 6 class 1
3		vx	. . . . . . 7 set x
4	3	cv 959	. . . . . 6 class x
5	2, 4	wcel 962	. . . . 5 wff 1 ∈ x
6		vy	. . . . . . . . 9 set y
7	6	cv 959	. . . . . . . 8 class y
8		caddc 5250	. . . . . . . 8 class +
9	7, 2, 8	co 3977	. . . . . . 7 class (y + 1)
10	9, 4	wcel 962	. . . . . 6 wff (y + 1) ∈ x
11	10, 6, 4	wral 1652	. . . . 5 wff ∀y ∈ x (y + 1) ∈ x
12	5, 11	wa 223	. . . 4 wff (1 ∈ x ⋀ ∀y ∈ x (y + 1) ∈ x)
13	12, 3	cab 1470	. . 3 class {x∣(1 ∈ x ⋀ ∀y ∈ x (y + 1) ∈ x)}
14	13	cint 2545	. 2 class ∩{x∣(1 ∈ x ⋀ ∀y ∈ x (y + 1) ∈ x)}
15	1, 14	wceq 960	1 wff ℕ = ∩{x∣(1 ∈ x ⋀ ∀y ∈ x (y + 1) ∈ x)}

This definition is referenced by:  peano5nn 5932  1nn 5940  peano2nn 5941  dfnn2 5942  dfuz 6211

Copyright terms: Public domain