Definition df-n 5881

Description: The natural numbers of analysis start at one (unlike the ordinal natural numbers, i.e. the members of the set om, df-om 3127, 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 5893 for the principle of mathematical induction. See dfnn2 5892 for a slight variant. See df-n0 6055 for the set of nonnegative integers NN0 starting at zero. See dfn2 6067 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 5276	. 2 class NN
2		c1 5215	. . . . . 6 class 1
3		vx	. . . . . . 7 set x
4	3	cv 953	. . . . . 6 class x
5	2, 4	wcel 956	. . . . 5 wff 1 e. x
6		vy	. . . . . . . . 9 set y
7	6	cv 953	. . . . . . . 8 class y
8		caddc 5217	. . . . . . . 8 class +
9	7, 2, 8	co 3954	. . . . . . 7 class (y + 1)
10	9, 4	wcel 956	. . . . . 6 wff (y + 1) e. x
11	10, 6, 4	wral 1642	. . . . 5 wff A.y e. x (y + 1) e. x
12	5, 11	wa 223	. . . 4 wff (1 e. x /\ A.y e. x (y + 1) e. x)
13	12, 3	cab 1461	. . 3 class {x | (1 e. x /\ A.y e. x (y + 1) e. x)}
14	13	cint 2528	. 2 class |^|{x | (1 e. x /\ A.y e. x (y + 1) e. x)}
15	1, 14	wceq 954	1 wff NN = |^|{x | (1 e. x /\ A.y e. x (y + 1) e. x)}

This definition is referenced by:  peano5nn 5882  1nn 5890  peano2nn 5891  dfnn2 5892  dfuz 6158

Copyright terms: Public domain