Theorem infxrunb3

Description: The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Assertion	infxrunb3	$$⊢A\subseteq {ℝ}^{*}\to \left(\forall x\in ℝ\exists y\in Ay\le x\leftrightarrow sup\left(A,{ℝ}^{*},<\right)=\mathrm{-\infty }\right)$$

Proof

Step	Hyp	Ref	Expression
1		unb2ltle	$$⊢A\subseteq {ℝ}^{*}\to \left(\forall w\in ℝ\exists y\in Ay<w\leftrightarrow \forall x\in ℝ\exists y\in Ay\le x\right)$$
2		infxrunb2	$$⊢A\subseteq {ℝ}^{*}\to \left(\forall w\in ℝ\exists y\in Ay<w\leftrightarrow sup\left(A,{ℝ}^{*},<\right)=\mathrm{-\infty }\right)$$
3	1 2	bitr3d	$$⊢A\subseteq {ℝ}^{*}\to \left(\forall x\in ℝ\exists y\in Ay\le x\leftrightarrow sup\left(A,{ℝ}^{*},<\right)=\mathrm{-\infty }\right)$$