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 {\mathbb{Z}}_{\ge M}\wedge S\ne \varnothing \right)\to inf\left(S,ℝ,<\right)\in S$$

Proof

Step	Hyp	Ref	Expression
1		uzssz	$$⊢{\mathbb{Z}}_{\ge M}\subseteq \mathbb{Z}$$
2		zssre	$$⊢\mathbb{Z}\subseteq ℝ$$
3	1 2	sstri	$$⊢{\mathbb{Z}}_{\ge M}\subseteq ℝ$$
4		sstr	$$⊢\left(S\subseteq {\mathbb{Z}}_{\ge M}\wedge {\mathbb{Z}}_{\ge M}\subseteq ℝ\right)\to S\subseteq ℝ$$
5	3 4	mpan2	$$⊢S\subseteq {\mathbb{Z}}_{\ge M}\to S\subseteq ℝ$$
6		uzwo	$$⊢\left(S\subseteq {\mathbb{Z}}_{\ge M}\wedge S\ne \varnothing \right)\to \exists j\in S\forall k\in Sj\le k$$
7		lbinfcl	$$⊢\left(S\subseteq ℝ\wedge \exists j\in S\forall k\in Sj\le k\right)\to inf\left(S,ℝ,<\right)\in S$$
8	5 6 7	syl2an2r	$$⊢\left(S\subseteq {\mathbb{Z}}_{\ge M}\wedge S\ne \varnothing \right)\to inf\left(S,ℝ,<\right)\in S$$