Definition df-n 5873

Description: The natural numbers of analysis start at one (unlike the ordinal natural numbers, i.e. the members of the set om, df-om 3122, 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 5885 for the principle of mathematical induction. See dfnn2 5884 for a slight variant. See df-n0 6047 for the set of nonnegative integers NN0 starting at zero. See dfn2 6059 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 5268	. 2 class NN
2		c1 5207	. . . . . 6 class 1
3		vx	. . . . . . 7 set x
4	3	cv 952	. . . . . 6 class x
5	2, 4	wcel 955	. . . . 5 wff 1 e. x
6		vy	. . . . . . . . 9 set y
7	6	cv 952	. . . . . . . 8 class y
8		caddc 5209	. . . . . . . 8 class +
9	7, 2, 8	co 3948	. . . . . . 7 class (y + 1)
10	9, 4	wcel 955	. . . . . 6 wff (y + 1) e. x
11	10, 6, 4	wral 1637	. . . . 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 1456	. . 3 class {x | (1 e. x /\ A.y e. x (y + 1) e. x)}
14	13	cint 2523	. 2 class |^|{x | (1 e. x /\ A.y e. x (y + 1) e. x)}
15	1, 14	wceq 953	1 wff NN = |^|{x | (1 e. x /\ A.y e. x (y + 1) e. x)}

This definition is referenced by:  peano5nn 5874  1nn 5882  peano2nn 5883  dfnn2 5884  dfuz 6150

Copyright terms: Public domain