This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ N ∈ Z → N + 1 ∈ Z

Proof

Step Hyp Ref Expression
1 peano2uzs.1 ⊢ Z = ℤ ≥ M
2 peano2uz ⊢ N ∈ ℤ ≥ M → N + 1 ∈ ℤ ≥ M
3 2 1 eleqtrrdi ⊢ N ∈ ℤ ≥ M → N + 1 ∈ Z
4 3 1 eleq2s ⊢ N ∈ Z → N + 1 ∈ Z