Theorem infxrrnmptcl

Description: The infimum of an arbitrary indexed set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	infxrrnmptcl.1	$$⊢Ⅎx\phi$$
	infxrrnmptcl.2	$$⊢\left(\phi \wedge x\in A\right)\to B\in {ℝ}^{*}$$
Assertion	infxrrnmptcl	$$⊢\phi \to inf\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right)\in {ℝ}^{*}$$

Proof

Step	Hyp	Ref	Expression
1		infxrrnmptcl.1	$$⊢Ⅎx\phi$$
2		infxrrnmptcl.2	$$⊢\left(\phi \wedge x\in A\right)\to B\in {ℝ}^{*}$$
3		eqid	$$⊢\left(x\in A⟼B\right)=\left(x\in A⟼B\right)$$
4	1 3 2	rnmptssd	$$⊢\phi \to \mathrm{ran}\left(x\in A⟼B\right)\subseteq {ℝ}^{*}$$
5	4	infxrcld	$$⊢\phi \to inf\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right)\in {ℝ}^{*}$$