Definition df-nn 11983

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 ℕ is a subset of complex numbers (nnsscn 11987), in contrast to the more elementary ordinal natural numbers ω, df-om 7722). See nnind 12000 for the principle of mathematical induction. See df-n0 12243 for the set of nonnegative integers ℕ₀. See dfn2 12255 for ℕ defined in terms of ℕ₀.

This is a technical definition that helps us avoid the Axiom of Infinity ax-inf2 9408 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 11996 (or its slight variant dfnn2 11995). (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 3-May-2014.)

Assertion

Ref	Expression
df-nn	⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)

Detailed syntax breakdown of Definition df-nn

Step	Hyp	Ref	Expression
1		cn 11982	. 2 class ℕ
2		vx	. . . . 5 setvar 𝑥
3		cvv 3433	. . . . 5 class V
4	2	cv 1538	. . . . . 6 class 𝑥
5		c1 10881	. . . . . 6 class 1
6		caddc 10883	. . . . . 6 class +
7	4, 5, 6	co 7284	. . . . 5 class (𝑥 + 1)
8	2, 3, 7	cmpt 5158	. . . 4 class (𝑥 ∈ V ↦ (𝑥 + 1))
9	8, 5	crdg 8249	. . 3 class rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1)
10		com 7721	. . 3 class ω
11	9, 10	cima 5593	. 2 class (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
12	1, 11	wceq 1539	1 wff ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)

This definition is referenced by:  nnexALT  11984  peano5nni  11985  1nn  11993  peano2nn  11994