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 ⊢ φ → A ⊆ 0 +∞
infxrge0lb.b ⊢ φ → B ∈ A
Assertion infxrge0lb ⊢ φ → sup A 0 +∞ < ≤ B

Proof

Step Hyp Ref Expression
1 infxrge0lb.a ⊢ φ → A ⊆ 0 +∞
2 infxrge0lb.b ⊢ φ → B ∈ A
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 ⊢ A ⊆ 0 +∞ → ∃ x ∈ 0 +∞ ∀ y ∈ A ¬ y < x ∧ ∀ y ∈ 0 +∞ x < y → ∃ z ∈ A z < y
9 1 8 syl ⊢ φ → ∃ x ∈ 0 +∞ ∀ y ∈ A ¬ y < x ∧ ∀ y ∈ 0 +∞ x < y → ∃ z ∈ A z < y
10 7 9 infcl ⊢ φ → sup A 0 +∞ < ∈ 0 +∞
11 3 10 sselid ⊢ φ → sup A 0 +∞ < ∈ ℝ *
12 1 2 sseldd ⊢ φ → B ∈ 0 +∞
13 3 12 sselid ⊢ φ → B ∈ ℝ *
14 7 9 inflb ⊢ φ → B ∈ A → ¬ B < sup A 0 +∞ <
15 2 14 mpd ⊢ φ → ¬ B < sup A 0 +∞ <
16 11 13 15 xrnltled ⊢ φ → sup A 0 +∞ < ≤ B