Metamath Proof Explorer


Theorem peano2uzs

Description: Second Peano postulate for an upper set of integers. (Contributed by Mario Carneiro, 26-Dec-2013)

Ref Expression
Hypothesis peano2uzs.1
|- Z = ( ZZ>= ` M )
Assertion peano2uzs
|- ( N e. Z -> ( N + 1 ) e. Z )

Proof

Step Hyp Ref Expression
1 peano2uzs.1
 |-  Z = ( ZZ>= ` M )
2 peano2uz
 |-  ( N e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( ZZ>= ` M ) )
3 2 1 eleqtrrdi
 |-  ( N e. ( ZZ>= ` M ) -> ( N + 1 ) e. Z )
4 3 1 eleq2s
 |-  ( N e. Z -> ( N + 1 ) e. Z )