Theorem infxrcld

Description: The infimum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypothesis	infxrcld.1	$$⊢\phi \to A\subseteq {ℝ}^{*}$$
Assertion	infxrcld	$$⊢\phi \to inf\left(A,{ℝ}^{*},<\right)\in {ℝ}^{*}$$

Proof

Step	Hyp	Ref	Expression
1		infxrcld.1	$$⊢\phi \to A\subseteq {ℝ}^{*}$$
2		infxrcl	$$⊢A\subseteq {ℝ}^{*}\to inf\left(A,{ℝ}^{*},<\right)\in {ℝ}^{*}$$
3	1 2	syl	$$⊢\phi \to inf\left(A,{ℝ}^{*},<\right)\in {ℝ}^{*}$$