Metamath Proof Explorer

Theorem 1nn

Description: Peano postulate: 1 is a positive integer. (Contributed by NM, 11-Jan-1997) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion 1nn ⊢ 1 ∈ ℕ

Proof

Step Hyp Ref Expression
1 1ex ⊢ 1 ∈ V
2 fr0g ⊢ 1 ∈ V → rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω ⁡ ∅ = 1
3 1 2 ax-mp ⊢ rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω ⁡ ∅ = 1
4 frfnom ⊢ rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω Fn ω
5 peano1 ⊢ ∅ ∈ ω
6 fnfvelrn ⊢ rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω Fn ω ∧ ∅ ∈ ω → rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω ⁡ ∅ ∈ ran ⁡ rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω
7 4 5 6 mp2an ⊢ rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω ⁡ ∅ ∈ ran ⁡ rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω
8 3 7 eqeltrri ⊢ 1 ∈ ran ⁡ rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω
9 df-nn ⊢ ℕ = rec ⁡ x ∈ V ⟼ x + 1 1 ω
10 df-ima ⊢ rec ⁡ x ∈ V ⟼ x + 1 1 ω = ran ⁡ rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω
11 9 10 eqtri ⊢ ℕ = ran ⁡ rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω
12 8 11 eleqtrri ⊢ 1 ∈ ℕ