Theorem peano2uzs

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

	Ref	Expression
Hypothesis	peano2uzs.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion	peano2uzs	⊢ ( 𝑁 ∈ 𝑍 → ( 𝑁 + 1 ) ∈ 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		peano2uzs.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		peano2uz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
3	2 1	eleqtrrdi	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 1 ) ∈ 𝑍 )
4	3 1	eleq2s	⊢ ( 𝑁 ∈ 𝑍 → ( 𝑁 + 1 ) ∈ 𝑍 )