Theorem fzssuz

Description: A finite set of sequential integers is a subset of an upper set of integers. (Contributed by NM, 28-Oct-2005)

	Ref	Expression
Assertion	fzssuz	⊢ ( 𝑀 ... 𝑁 ) ⊆ ( ℤ≥ ‘ 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		elfzuz	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
2	1	ssriv	⊢ ( 𝑀 ... 𝑁 ) ⊆ ( ℤ≥ ‘ 𝑀 )