Definition df-n 7441

Description: The natural numbers of analysis start at one (unlike the ordinal natural numbers, i.e. the members of the set om, df-om 4086, 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 7453 for the principle of mathematical induction. See dfnn2 7452 for a slight variant. See df-n0 7649 for the set of nonnegative integers NN0 starting at zero. See dfn2 7661 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 6992	. 2 class NN
2		c1 6753	. . . . . 6 class 1
3		vx	. . . . . . 7 set x
4	3	cv 1585	. . . . . 6 class x
5	2, 4	wcel 1588	. . . . 5 wff 1 e. x
6		vy	. . . . . . . . 9 set y
7	6	cv 1585	. . . . . . . 8 class y
8		caddc 6755	. . . . . . . 8 class +
9	7, 2, 8	co 4981	. . . . . . 7 class (y + 1)
10	9, 4	wcel 1588	. . . . . 6 wff (y + 1) e. x
11	10, 6, 4	wral 2355	. . . . 5 wff A.y e. x (y + 1) e. x
12	5, 11	wa 337	. . . 4 wff (1 e. x /\ A.y e. x (y + 1) e. x)
13	12, 3	cab 2128	. . 3 class {x | (1 e. x /\ A.y e. x (y + 1) e. x)}
14	13	cint 3400	. 2 class |^|{x | (1 e. x /\ A.y e. x (y + 1) e. x)}
15	1, 14	wceq 1586	1 wff NN = |^|{x | (1 e. x /\ A.y e. x (y + 1) e. x)}

This definition is referenced by:  peano5nni 7442  1nn 7450  peano2nn 7451  dfnn2 7452  dfuzi 7757

Copyright terms: Public domain