Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-nn Structured version   Visualization version   GIF version

Definition df-nn 11211
 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 11215), in contrast to the more elementary ordinal natural numbers ω, df-om 7229). See nnind 11228 for the principle of mathematical induction. See df-n0 11483 for the set of nonnegative integers ℕ0. See dfn2 11495 for ℕ defined in terms of ℕ0. This is a technical definition that helps us avoid the Axiom of Infinity ax-inf2 8709 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 11224 (or its slight variant dfnn2 11223). (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
StepHypRef Expression
1 cn 11210 . 2 class
2 vx . . . . 5 setvar 𝑥
3 cvv 3338 . . . . 5 class V
42cv 1629 . . . . . 6 class 𝑥
5 c1 10127 . . . . . 6 class 1
6 caddc 10129 . . . . . 6 class +
74, 5, 6co 6811 . . . . 5 class (𝑥 + 1)
82, 3, 7cmpt 4879 . . . 4 class (𝑥 ∈ V ↦ (𝑥 + 1))
98, 5crdg 7672 . . 3 class rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1)
10 com 7228 . . 3 class ω
119, 10cima 5267 . 2 class (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
121, 11wceq 1630 1 wff ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
 Colors of variables: wff setvar class This definition is referenced by:  nnexALT  11212  peano5nni  11213  1nn  11221  peano2nn  11222
 Copyright terms: Public domain W3C validator