Theorem infxrglb

Description: The infimum of a set of extended reals is less than an extended real if and only if the set contains a smaller number. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Assertion	infxrglb	$$⊢\left(A\subseteq {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(sup\left(A,{ℝ}^{*},<\right)<B\leftrightarrow \exists x\in Ax<B\right)$$

Proof

Step	Hyp	Ref	Expression
1		xrltso	$$⊢<\mathrm{Or}{ℝ}^{*}$$
2	1	a1i	$$⊢A\subseteq {ℝ}^{*}\to <\mathrm{Or}{ℝ}^{*}$$
3		xrinfmss	$$⊢A\subseteq {ℝ}^{*}\to \exists z\in {ℝ}^{*}\left(\forall y\in A\neg y<z\wedge \forall y\in {ℝ}^{*}\left(z<y\to \exists x\in Ax<y\right)\right)$$
4		id	$$⊢A\subseteq {ℝ}^{*}\to A\subseteq {ℝ}^{*}$$
5	2 3 4	infglbb	$$⊢\left(A\subseteq {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(sup\left(A,{ℝ}^{*},<\right)<B\leftrightarrow \exists x\in Ax<B\right)$$