This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) ‘ ∅ ) = 1 )
3 1 2 ax-mp ⊢ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) ‘ ∅ ) = 1
4 frfnom ⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) Fn ω
5 peano1 ⊢ ∅ ∈ ω
6 fnfvelrn ⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) Fn ω ∧ ∅ ∈ ω ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) ‘ ∅ ) ∈ ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) )
7 4 5 6 mp2an ⊢ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) ‘ ∅ ) ∈ ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω )
8 3 7 eqeltrri ⊢ 1 ∈ ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω )
9 df-nn ⊢ ℕ = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) “ ω )
10 df-ima ⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) “ ω ) = ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω )
11 9 10 eqtri ⊢ ℕ = ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω )
12 8 11 eleqtrri ⊢ 1 ∈ ℕ