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 ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) “ ω ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cn | ⊢ ℕ | |
| 1 | vx | ⊢ 𝑥 | |
| 2 | cvv | ⊢ V | |
| 3 | 1 | cv | ⊢ 𝑥 |
| 4 | caddc | ⊢ + | |
| 5 | c1 | ⊢ 1 | |
| 6 | 3 5 4 | co | ⊢ ( 𝑥 + 1 ) |
| 7 | 1 2 6 | cmpt | ⊢ ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) |
| 8 | 7 5 | crdg | ⊢ rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) |
| 9 | com | ⊢ ω | |
| 10 | 8 9 | cima | ⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) “ ω ) |
| 11 | 0 10 | wceq | ⊢ ℕ = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) “ ω ) |