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 ) )