Metamath Proof Explorer


Theorem infxrge0lb

Description: A member of a set of nonnegative extended reals is greater than or equal to the set's infimum. (Contributed by Thierry Arnoux, 19-Jul-2020) (Revised by AV, 4-Oct-2020)

Ref Expression
Hypotheses infxrge0lb.a ( 𝜑𝐴 ⊆ ( 0 [,] +∞ ) )
infxrge0lb.b ( 𝜑𝐵𝐴 )
Assertion infxrge0lb ( 𝜑 → inf ( 𝐴 , ( 0 [,] +∞ ) , < ) ≤ 𝐵 )

Proof

Step Hyp Ref Expression
1 infxrge0lb.a ( 𝜑𝐴 ⊆ ( 0 [,] +∞ ) )
2 infxrge0lb.b ( 𝜑𝐵𝐴 )
3 iccssxr ( 0 [,] +∞ ) ⊆ ℝ*
4 xrltso < Or ℝ*
5 soss ( ( 0 [,] +∞ ) ⊆ ℝ* → ( < Or ℝ* → < Or ( 0 [,] +∞ ) ) )
6 3 4 5 mp2 < Or ( 0 [,] +∞ )
7 6 a1i ( 𝜑 → < Or ( 0 [,] +∞ ) )
8 xrge0infss ( 𝐴 ⊆ ( 0 [,] +∞ ) → ∃ 𝑥 ∈ ( 0 [,] +∞ ) ( ∀ 𝑦𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 < 𝑦 → ∃ 𝑧𝐴 𝑧 < 𝑦 ) ) )
9 1 8 syl ( 𝜑 → ∃ 𝑥 ∈ ( 0 [,] +∞ ) ( ∀ 𝑦𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 < 𝑦 → ∃ 𝑧𝐴 𝑧 < 𝑦 ) ) )
10 7 9 infcl ( 𝜑 → inf ( 𝐴 , ( 0 [,] +∞ ) , < ) ∈ ( 0 [,] +∞ ) )
11 3 10 sselid ( 𝜑 → inf ( 𝐴 , ( 0 [,] +∞ ) , < ) ∈ ℝ* )
12 1 2 sseldd ( 𝜑𝐵 ∈ ( 0 [,] +∞ ) )
13 3 12 sselid ( 𝜑𝐵 ∈ ℝ* )
14 7 9 inflb ( 𝜑 → ( 𝐵𝐴 → ¬ 𝐵 < inf ( 𝐴 , ( 0 [,] +∞ ) , < ) ) )
15 2 14 mpd ( 𝜑 → ¬ 𝐵 < inf ( 𝐴 , ( 0 [,] +∞ ) , < ) )
16 11 13 15 xrnltled ( 𝜑 → inf ( 𝐴 , ( 0 [,] +∞ ) , < ) ≤ 𝐵 )