Theorem infxrcl

Description: The infimum of an arbitrary set of extended reals is an extended real. (Contributed by NM, 19-Jan-2006) (Revised by AV, 5-Sep-2020)

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

Proof

Step	Hyp	Ref	Expression
1		xrltso	$$⊢<\mathrm{Or}{ℝ}^{*}$$
2	1	a1i	$$⊢A\subseteq {ℝ}^{*}\to <\mathrm{Or}{ℝ}^{*}$$
3		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)$$
4	2 3	infcl	$$⊢A\subseteq {ℝ}^{*}\to inf\left(A,{ℝ}^{*},<\right)\in {ℝ}^{*}$$