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=M
Assertion peano2uzs NZN+1Z

Proof

Step Hyp Ref Expression
1 peano2uzs.1 Z=M
2 peano2uz NMN+1M
3 2 1 eleqtrrdi NMN+1Z
4 3 1 eleq2s NZN+1Z