Metamath Proof Explorer


Theorem fzossz

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

Ref Expression
Assertion fzossz ( 𝑀 ..^ 𝑁 ) ⊆ ℤ

Proof

Step Hyp Ref Expression
1 fzossfz ( 𝑀 ..^ 𝑁 ) ⊆ ( 𝑀 ... 𝑁 )
2 fzssz ( 𝑀 ... 𝑁 ) ⊆ ℤ
3 1 2 sstri ( 𝑀 ..^ 𝑁 ) ⊆ ℤ