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	⊢ Ⅎ 𝑥 𝜑
	infxrrnmptcl.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
Assertion	infxrrnmptcl	⊢ ( 𝜑 → inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) ∈ ℝ* )

Proof

Step	Hyp	Ref	Expression
1		infxrrnmptcl.1	⊢ Ⅎ 𝑥 𝜑
2		infxrrnmptcl.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
3		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
4	1 3 2	rnmptssd	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ* )
5	4	infxrcld	⊢ ( 𝜑 → inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) ∈ ℝ* )