Theorem infxrgelb

Description: The infimum of a set of extended reals is greater than or equal to a lower bound. (Contributed by Mario Carneiro, 16-Mar-2014) (Revised by AV, 5-Sep-2020)

	Ref	Expression
Assertion	infxrgelb	$$⊢\left(A\subseteq {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(B\le sup\left(A,{ℝ}^{*},<\right)\leftrightarrow \forall x\in AB\le x\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)$$
6	5	notbid	$$⊢\left(A\subseteq {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(\neg sup\left(A,{ℝ}^{*},<\right)<B\leftrightarrow \neg \exists x\in Ax<B\right)$$
7		ralnex	$$⊢\forall x\in A\neg x<B\leftrightarrow \neg \exists x\in Ax<B$$
8	6 7	bitr4di	$$⊢\left(A\subseteq {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(\neg sup\left(A,{ℝ}^{*},<\right)<B\leftrightarrow \forall x\in A\neg x<B\right)$$
9		id	$$⊢B\in {ℝ}^{*}\to B\in {ℝ}^{*}$$
10		infxrcl	$$⊢A\subseteq {ℝ}^{*}\to sup\left(A,{ℝ}^{*},<\right)\in {ℝ}^{*}$$
11		xrlenlt	$$⊢\left(B\in {ℝ}^{*}\wedge sup\left(A,{ℝ}^{*},<\right)\in {ℝ}^{*}\right)\to \left(B\le sup\left(A,{ℝ}^{*},<\right)\leftrightarrow \neg sup\left(A,{ℝ}^{*},<\right)<B\right)$$
12	9 10 11	syl2anr	$$⊢\left(A\subseteq {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(B\le sup\left(A,{ℝ}^{*},<\right)\leftrightarrow \neg sup\left(A,{ℝ}^{*},<\right)<B\right)$$
13		simplr	$$⊢\left(\left(A\subseteq {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\wedge x\in A\right)\to B\in {ℝ}^{*}$$
14		simpl	$$⊢\left(A\subseteq {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to A\subseteq {ℝ}^{*}$$
15	14	sselda	$$⊢\left(\left(A\subseteq {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\wedge x\in A\right)\to x\in {ℝ}^{*}$$
16	13 15	xrlenltd	$$⊢\left(\left(A\subseteq {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\wedge x\in A\right)\to \left(B\le x\leftrightarrow \neg x<B\right)$$
17	16	ralbidva	$$⊢\left(A\subseteq {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(\forall x\in AB\le x\leftrightarrow \forall x\in A\neg x<B\right)$$
18	8 12 17	3bitr4d	$$⊢\left(A\subseteq {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(B\le sup\left(A,{ℝ}^{*},<\right)\leftrightarrow \forall x\in AB\le x\right)$$