Metamath Proof Explorer

Theorem fzossuz

Description: A half-open integer interval is a subset of an upper set of integers. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Assertion fzossuz 
|- ( M ..^ N ) C_ ( ZZ>= ` M )

Proof

Step Hyp Ref Expression
1 fzossfz 
 |-  ( M ..^ N ) C_ ( M ... N )
2 fzssuz 
 |-  ( M ... N ) C_ ( ZZ>= ` M )
3 1 2 sstri 
 |-  ( M ..^ N ) C_ ( ZZ>= ` M )