Metamath Proof Explorer

Theorem peano2nn

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

Ref Expression
Assertion peano2nn 
|- ( A e. NN -> ( A + 1 ) e. NN )

Proof

Step Hyp Ref Expression
1 frfnom 
 |-  ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) Fn _om
2 fvelrnb 
 |-  ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) Fn _om -> ( A e. ran ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) <-> E. y e. _om ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) ` y ) = A ) )
3 1 2 ax-mp 
 |-  ( A e. ran ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) <-> E. y e. _om ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) ` y ) = A )
4 ovex 
 |-  ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) ` y ) + 1 ) e. _V
5 eqid 
 |-  ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om )
6 oveq1 
 |-  ( z = x -> ( z + 1 ) = ( x + 1 ) )
7 oveq1 
 |-  ( z = ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) ` y ) -> ( z + 1 ) = ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) ` y ) + 1 ) )
8 5 6 7 frsucmpt2 
 |-  ( ( y e. _om /\ ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) ` y ) + 1 ) e. _V ) -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) ` suc y ) = ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) ` y ) + 1 ) )
9 4 8 mpan2 
 |-  ( y e. _om -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) ` suc y ) = ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) ` y ) + 1 ) )
10 peano2 
 |-  ( y e. _om -> suc y e. _om )
11 fnfvelrn 
 |-  ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) Fn _om /\ suc y e. _om ) -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) ` suc y ) e. ran ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) )
12 1 10 11 sylancr 
 |-  ( y e. _om -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) ` suc y ) e. ran ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) )
13 df-nn 
 |-  NN = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) " _om )
14 df-ima 
 |-  ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) " _om ) = ran ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om )
15 13 14 eqtri 
 |-  NN = ran ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om )
16 12 15 eleqtrrdi 
 |-  ( y e. _om -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) ` suc y ) e. NN )
17 9 16 eqeltrrd 
 |-  ( y e. _om -> ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) ` y ) + 1 ) e. NN )
18 oveq1 
 |-  ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) ` y ) = A -> ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) ` y ) + 1 ) = ( A + 1 ) )
19 18 eleq1d 
 |-  ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) ` y ) = A -> ( ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) ` y ) + 1 ) e. NN <-> ( A + 1 ) e. NN ) )
20 17 19 syl5ibcom 
 |-  ( y e. _om -> ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) ` y ) = A -> ( A + 1 ) e. NN ) )
21 20 rexlimiv 
 |-  ( E. y e. _om ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) ` y ) = A -> ( A + 1 ) e. NN )
22 3 21 sylbi 
 |-  ( A e. ran ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) -> ( A + 1 ) e. NN )
23 22 15 eleq2s 
 |-  ( A e. NN -> ( A + 1 ) e. NN )