Metamath Proof Explorer


Theorem infxrglb

Description: The infimum of a set of extended reals is less than an extended real if and only if the set contains a smaller number. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Assertion infxrglb ( ( 𝐴 ⊆ ℝ*𝐵 ∈ ℝ* ) → ( inf ( 𝐴 , ℝ* , < ) < 𝐵 ↔ ∃ 𝑥𝐴 𝑥 < 𝐵 ) )

Proof

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