This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝐴 , ℝ* , < ) ∈ ℝ* )