Definition df-n 6070

Description: The natural numbers of analysis start at one (unlike the ordinal natural numbers, i.e. the members of the set om, df-om 3219, 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 6082 for the principle of mathematical induction. See dfnn2 6081 for a slight variant. See df-n0 6268 for the set of nonnegative integers NN0 starting at zero. See dfn2 6280 for NN defined in terms of NN0.

Assertion

Ref	Expression
df-n	|- NN = |^|{x | (1 e. x /\ A.y e. x (y + 1) e. x)}

Distinct variable group:   x,y

Detailed syntax breakdown of Definition df-n

Step	Hyp	Ref	Expression
1		cn 5450	. 2 class NN
2		c1 5389	. . . . . 6 class 1
3		vx	. . . . . . 7 set x
4	3	cv 991	. . . . . 6 class x
5	2, 4	wcel 994	. . . . 5 wff 1 e. x
6		vy	. . . . . . . . 9 set y
7	6	cv 991	. . . . . . . 8 class y
8		caddc 5391	. . . . . . . 8 class +
9	7, 2, 8	co 4021	. . . . . . 7 class (y + 1)
10	9, 4	wcel 994	. . . . . 6 wff (y + 1) e. x
11	10, 6, 4	wral 1691	. . . . 5 wff A.y e. x (y + 1) e. x
12	5, 11	wa 221	. . . 4 wff (1 e. x /\ A.y e. x (y + 1) e. x)
13	12, 3	cab 1505	. . 3 class {x | (1 e. x /\ A.y e. x (y + 1) e. x)}
14	13	cint 2600	. 2 class |^|{x | (1 e. x /\ A.y e. x (y + 1) e. x)}
15	1, 14	wceq 992	1 wff NN = |^|{x | (1 e. x /\ A.y e. x (y + 1) e. x)}

This definition is referenced by:  peano5nni 6071  1nn 6079  peano2nn 6080  dfnn2 6081  dfuzi 6373

Copyright terms: Public domain