Theorem infssuzle

Description: The infimum of a subset of an upper set of integers is less than or equal to all members of the subset. (Contributed by NM, 11-Oct-2005) (Revised by AV, 5-Sep-2020)

	Ref	Expression
Assertion	infssuzle	$$⊢\left(S\subseteq {\mathbb{Z}}_{\ge M}\wedge A\in S\right)\to inf\left(S,ℝ,<\right)\le A$$

Proof

Step	Hyp	Ref	Expression
1		ne0i	$$⊢A\in S\to S\ne \varnothing$$
2		uzwo	$$⊢\left(S\subseteq {\mathbb{Z}}_{\ge M}\wedge S\ne \varnothing \right)\to \exists j\in S\forall k\in Sj\le k$$
3	1 2	sylan2	$$⊢\left(S\subseteq {\mathbb{Z}}_{\ge M}\wedge A\in S\right)\to \exists j\in S\forall k\in Sj\le k$$
4		uzssz	$$⊢{\mathbb{Z}}_{\ge M}\subseteq \mathbb{Z}$$
5		zssre	$$⊢\mathbb{Z}\subseteq ℝ$$
6	4 5	sstri	$$⊢{\mathbb{Z}}_{\ge M}\subseteq ℝ$$
7		sstr	$$⊢\left(S\subseteq {\mathbb{Z}}_{\ge M}\wedge {\mathbb{Z}}_{\ge M}\subseteq ℝ\right)\to S\subseteq ℝ$$
8	6 7	mpan2	$$⊢S\subseteq {\mathbb{Z}}_{\ge M}\to S\subseteq ℝ$$
9		lbinfle	$$⊢\left(S\subseteq ℝ\wedge \exists j\in S\forall k\in Sj\le k\wedge A\in S\right)\to inf\left(S,ℝ,<\right)\le A$$
10	9	3com23	$$⊢\left(S\subseteq ℝ\wedge A\in S\wedge \exists j\in S\forall k\in Sj\le k\right)\to inf\left(S,ℝ,<\right)\le A$$
11	8 10	syl3an1	$$⊢\left(S\subseteq {\mathbb{Z}}_{\ge M}\wedge A\in S\wedge \exists j\in S\forall k\in Sj\le k\right)\to inf\left(S,ℝ,<\right)\le A$$
12	3 11	mpd3an3	$$⊢\left(S\subseteq {\mathbb{Z}}_{\ge M}\wedge A\in S\right)\to inf\left(S,ℝ,<\right)\le A$$