Metamath Proof Explorer

Theorem peano2nn0

Description: Second Peano postulate for nonnegative integers. (Contributed by NM, 9-May-2004)

Ref Expression
Assertion peano2nn0 
|- ( N e. NN0 -> ( N + 1 ) e. NN0 )

Proof

Step Hyp Ref Expression
1 1nn0 
 |-  1 e. NN0
2 nn0addcl 
 |-  ( ( N e. NN0 /\ 1 e. NN0 ) -> ( N + 1 ) e. NN0 )
3 1 2 mpan2 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )