# Metamath Proof Explorer

## Theorem infssuzcl

Description: The infimum of a subset of an upper set of integers belongs to the subset. (Contributed by NM, 11-Oct-2005) (Revised by AV, 5-Sep-2020)

Ref Expression
Assertion infssuzcl ${⊢}\left({S}\subseteq {ℤ}_{\ge {M}}\wedge {S}\ne \varnothing \right)\to sup\left({S},ℝ,<\right)\in {S}$

### Proof

Step Hyp Ref Expression
1 uzssz ${⊢}{ℤ}_{\ge {M}}\subseteq ℤ$
2 zssre ${⊢}ℤ\subseteq ℝ$
3 1 2 sstri ${⊢}{ℤ}_{\ge {M}}\subseteq ℝ$
4 sstr ${⊢}\left({S}\subseteq {ℤ}_{\ge {M}}\wedge {ℤ}_{\ge {M}}\subseteq ℝ\right)\to {S}\subseteq ℝ$
5 3 4 mpan2 ${⊢}{S}\subseteq {ℤ}_{\ge {M}}\to {S}\subseteq ℝ$
6 uzwo ${⊢}\left({S}\subseteq {ℤ}_{\ge {M}}\wedge {S}\ne \varnothing \right)\to \exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {k}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {k}$
7 lbinfcl ${⊢}\left({S}\subseteq ℝ\wedge \exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {k}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {k}\right)\to sup\left({S},ℝ,<\right)\in {S}$
8 5 6 7 syl2an2r ${⊢}\left({S}\subseteq {ℤ}_{\ge {M}}\wedge {S}\ne \varnothing \right)\to sup\left({S},ℝ,<\right)\in {S}$