Metamath Proof Explorer


Theorem fzp1ss

Description: Subset relationship for finite sets of sequential integers. (Contributed by NM, 26-Jul-2005) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion fzp1ss ( 𝑀 ∈ ℤ → ( ( 𝑀 + 1 ) ... 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) )

Proof

Step Hyp Ref Expression
1 uzid ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ𝑀 ) )
2 peano2uz ( 𝑀 ∈ ( ℤ𝑀 ) → ( 𝑀 + 1 ) ∈ ( ℤ𝑀 ) )
3 fzss1 ( ( 𝑀 + 1 ) ∈ ( ℤ𝑀 ) → ( ( 𝑀 + 1 ) ... 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) )
4 1 2 3 3syl ( 𝑀 ∈ ℤ → ( ( 𝑀 + 1 ) ... 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) )