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 )