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 e. NN

Proof

Step Hyp Ref Expression
1 1ex 
 |-  1 e. _V
2 fr0g 
 |-  ( 1 e. _V -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) ` (/) ) = 1 )
3 1 2 ax-mp 
 |-  ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) ` (/) ) = 1
4 frfnom 
 |-  ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) Fn _om
5 peano1 
 |-  (/) e. _om
6 fnfvelrn 
 |-  ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) Fn _om /\ (/) e. _om ) -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) ` (/) ) e. ran ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) )
7 4 5 6 mp2an 
 |-  ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) ` (/) ) e. ran ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om )
8 3 7 eqeltrri 
 |-  1 e. ran ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om )
9 df-nn 
 |-  NN = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) " _om )
10 df-ima 
 |-  ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) " _om ) = ran ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om )
11 9 10 eqtri 
 |-  NN = ran ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om )
12 8 11 eleqtrri 
 |-  1 e. NN