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\in ℕ$

Proof

Step Hyp Ref Expression
1 1ex ${⊢}1\in \mathrm{V}$
2 fr0g ${⊢}1\in \mathrm{V}\to \left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left(\varnothing \right)=1$
3 1 2 ax-mp ${⊢}\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left(\varnothing \right)=1$
4 frfnom ${⊢}\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)Fn\mathrm{\omega }$
5 peano1 ${⊢}\varnothing \in \mathrm{\omega }$
6 fnfvelrn ${⊢}\left(\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)Fn\mathrm{\omega }\wedge \varnothing \in \mathrm{\omega }\right)\to \left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left(\varnothing \right)\in \mathrm{ran}\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)$
7 4 5 6 mp2an ${⊢}\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left(\varnothing \right)\in \mathrm{ran}\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)$
8 3 7 eqeltrri ${⊢}1\in \mathrm{ran}\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)$
9 df-nn ${⊢}ℕ=\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)\left[\mathrm{\omega }\right]$
10 df-ima ${⊢}\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)\left[\mathrm{\omega }\right]=\mathrm{ran}\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)$
11 9 10 eqtri ${⊢}ℕ=\mathrm{ran}\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)$
12 8 11 eleqtrri ${⊢}1\in ℕ$