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 
|- Z = ( ZZ>= ` M )
Assertion uzssz2 
|- Z C_ ZZ

Proof

Step Hyp Ref Expression
1 uzssz2.1 
 |-  Z = ( ZZ>= ` M )
2 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
3 1 2 eqsstri 
 |-  Z C_ ZZ