Metamath Proof Explorer


Theorem uzssre

Description: An upper set of integers is a subset of the reals. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Assertion uzssre ( ℤ𝑀 ) ⊆ ℝ

Proof

Step Hyp Ref Expression
1 uzssz ( ℤ𝑀 ) ⊆ ℤ
2 zssre ℤ ⊆ ℝ
3 1 2 sstri ( ℤ𝑀 ) ⊆ ℝ