Definition df-n 7108

Description: The natural numbers of analysis start at one (unlike the ordinal natural numbers, i.e. the members of the set om, df-om 3950, 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 7120 for the principle of mathematical induction. See dfnn2 7119 for a slight variant. See df-n0 7309 for the set of nonnegative integers NN0 starting at zero. See dfn2 7321 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 6449	. 2 class NN
2		c1 6387	. . . . . 6 class 1
3		vx	. . . . . . 7 set x
4	3	cv 1297	. . . . . 6 class x
5	2, 4	wcel 1300	. . . . 5 wff 1 e. x
6		vy	. . . . . . . . 9 set y
7	6	cv 1297	. . . . . . . 8 class y
8		caddc 6389	. . . . . . . 8 class +
9	7, 2, 8	co 4884	. . . . . . 7 class (y + 1)
10	9, 4	wcel 1300	. . . . . 6 wff (y + 1) e. x
11	10, 6, 4	wral 2105	. . . . 5 wff A.y e. x (y + 1) e. x
12	5, 11	wa 240	. . . 4 wff (1 e. x /\ A.y e. x (y + 1) e. x)
13	12, 3	cab 1871	. . 3 class {x | (1 e. x /\ A.y e. x (y + 1) e. x)}
14	13	cint 3214	. 2 class |^|{x | (1 e. x /\ A.y e. x (y + 1) e. x)}
15	1, 14	wceq 1298	1 wff NN = |^|{x | (1 e. x /\ A.y e. x (y + 1) e. x)}

This definition is referenced by:  peano5nni 7109  1nn 7117  peano2nn 7118  dfnn2 7119  dfuzi 7414

Copyright terms: Public domain