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={\mathbb{Z}}_{\ge M}$$
Assertion	peano2uzs	$$⊢N\in Z\to N+1\in Z$$

Proof

Step	Hyp	Ref	Expression
1		peano2uzs.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		peano2uz	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N+1\in {\mathbb{Z}}_{\ge M}$$
3	2 1	eleqtrrdi	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N+1\in Z$$
4	3 1	eleq2s	$$⊢N\in Z\to N+1\in Z$$