Metamath Proof Explorer

Definition df-nn

Description: Define the set of positive integers. Some authors, especially in analysis books, call these the natural numbers, whereas other authors choose to include 0 in their definition of natural numbers. Note that NN is a subset of complex numbers ( nnsscn ), in contrast to the more elementary ordinal natural numbers _om , df-om ). See nnind for the principle of mathematical induction. See df-n0 for the set of nonnegative integers NN0 . See dfn2 for NN defined in terms of NN0 .

This is a technical definition that helps us avoid the Axiom of Infinity ax-inf2 in certain proofs. For a more conventional and intuitive definition ("the smallest set of reals containing 1 as well as the successor of every member") see dfnn3 (or its slight variant dfnn2 ). (Contributed by NM, 10-Jan-1997) (Revised by Mario Carneiro, 3-May-2014)

		Ref	Expression
	Assertion	df-nn	$⊢ ℕ = rec ((x \in V ⟼ x + 1), 1) [ω]$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cn	$class ℕ$
1		vx	$setvar x$
2		cvv	$class V$
3	1	cv	$setvar x$
4		caddc	$class +$
5		c1	$class 1$
6	3 5 4	co	$class (x + 1)$
7	1 2 6	cmpt	$class (x \in V ⟼ x + 1)$
8	7 5	crdg	$class rec ((x \in V ⟼ x + 1), 1)$
9		com	$class ω$
10	8 9	cima	$class rec ((x \in V ⟼ x + 1), 1) [ω]$
11	0 10	wceq	$wff ℕ = rec ((x \in V ⟼ x + 1), 1) [ω]$