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	⊢ ( 𝐴 ⊆ ℝ* → inf ( 𝐴 , ℝ* , < ) ∈ ℝ* )

Proof

Step	Hyp	Ref	Expression
1		xrltso	⊢ < Or ℝ*
2	1	a1i	⊢ ( 𝐴 ⊆ ℝ* → < Or ℝ* )
3		xrinfmss	⊢ ( 𝐴 ⊆ ℝ* → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
4	2 3	infcl	⊢ ( 𝐴 ⊆ ℝ* → inf ( 𝐴 , ℝ* , < ) ∈ ℝ* )