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 | ⊢ 𝑍 ⊆ ℤ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uzssz2.1 | ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 ) | |
2 | uzssz | ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ | |
3 | 1 2 | eqsstri | ⊢ 𝑍 ⊆ ℤ |