This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝑀 ..^ 𝑁 ) ⊆ ℤ