Metamath Proof Explorer


Theorem fzssp1

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

Ref Expression
Assertion fzssp1 ( 𝑀 ... 𝑁 ) ⊆ ( 𝑀 ... ( 𝑁 + 1 ) )

Proof

Step Hyp Ref Expression
1 elfzel2 ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ℤ )
2 uzid ( 𝑁 ∈ ℤ → 𝑁 ∈ ( ℤ𝑁 ) )
3 peano2uz ( 𝑁 ∈ ( ℤ𝑁 ) → ( 𝑁 + 1 ) ∈ ( ℤ𝑁 ) )
4 fzss2 ( ( 𝑁 + 1 ) ∈ ( ℤ𝑁 ) → ( 𝑀 ... 𝑁 ) ⊆ ( 𝑀 ... ( 𝑁 + 1 ) ) )
5 1 2 3 4 4syl ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → ( 𝑀 ... 𝑁 ) ⊆ ( 𝑀 ... ( 𝑁 + 1 ) ) )
6 id ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ∈ ( 𝑀 ... 𝑁 ) )
7 5 6 sseldd ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) )
8 7 ssriv ( 𝑀 ... 𝑁 ) ⊆ ( 𝑀 ... ( 𝑁 + 1 ) )