Metamath Proof Explorer


Theorem uzssz2

Description: An upper set of integers is a subset of all integers. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypothesis uzssz2.1 𝑍 = ( ℤ𝑀 )
Assertion uzssz2 𝑍 ⊆ ℤ

Proof

Step Hyp Ref Expression
1 uzssz2.1 𝑍 = ( ℤ𝑀 )
2 uzssz ( ℤ𝑀 ) ⊆ ℤ
3 1 2 eqsstri 𝑍 ⊆ ℤ