Metamath Proof Explorer

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 
|- ( M ... N ) C_ ( ZZ>= ` M )

Proof

Step Hyp Ref Expression
1 elfzuz 
 |-  ( k e. ( M ... N ) -> k e. ( ZZ>= ` M ) )
2 1 ssriv 
 |-  ( M ... N ) C_ ( ZZ>= ` M )