Theorem infxrlb

Description: A member of a set of extended reals is greater than or equal to the set's infimum. (Contributed by Mario Carneiro, 16-Mar-2014) (Revised by AV, 5-Sep-2020)

	Ref	Expression
Assertion	infxrlb	$$⊢\left(A\subseteq {ℝ}^{*}\wedge B\in A\right)\to inf\left(A,{ℝ}^{*},<\right)\le B$$

Proof

Step	Hyp	Ref	Expression
1		infxrcl	$$⊢A\subseteq {ℝ}^{*}\to inf\left(A,{ℝ}^{*},<\right)\in {ℝ}^{*}$$
2	1	adantr	$$⊢\left(A\subseteq {ℝ}^{*}\wedge B\in A\right)\to inf\left(A,{ℝ}^{*},<\right)\in {ℝ}^{*}$$
3		ssel2	$$⊢\left(A\subseteq {ℝ}^{*}\wedge B\in A\right)\to B\in {ℝ}^{*}$$
4		xrltso	$$⊢<\mathrm{Or}{ℝ}^{*}$$
5	4	a1i	$$⊢A\subseteq {ℝ}^{*}\to <\mathrm{Or}{ℝ}^{*}$$
6		xrinfmss	$$⊢A\subseteq {ℝ}^{*}\to \exists x\in {ℝ}^{*}\left(\forall y\in A\neg y<x\wedge \forall y\in {ℝ}^{*}\left(x<y\to \exists z\in Az<y\right)\right)$$
7	5 6	inflb	$$⊢A\subseteq {ℝ}^{*}\to \left(B\in A\to \neg B<inf\left(A,{ℝ}^{*},<\right)\right)$$
8	7	imp	$$⊢\left(A\subseteq {ℝ}^{*}\wedge B\in A\right)\to \neg B<inf\left(A,{ℝ}^{*},<\right)$$
9	2 3 8	xrnltled	$$⊢\left(A\subseteq {ℝ}^{*}\wedge B\in A\right)\to inf\left(A,{ℝ}^{*},<\right)\le B$$