Metamath Proof Explorer

Theorem infxrge0gelb

Description: The infimum of a set of nonnegative extended reals is greater than or equal to a lower bound. (Contributed by Thierry Arnoux, 19-Jul-2020) (Revised by AV, 4-Oct-2020)

Ref Expression
Hypotheses infxrge0glb.a ⊢ φ → A ⊆ 0 +∞
infxrge0glb.b ⊢ φ → B ∈ 0 +∞
Assertion infxrge0gelb ⊢ φ → B ≤ sup A 0 +∞ < ↔ ∀ x ∈ A B ≤ x

Proof

Step Hyp Ref Expression
1 infxrge0glb.a ⊢ φ → A ⊆ 0 +∞
2 infxrge0glb.b ⊢ φ → B ∈ 0 +∞
3 1 2 infxrge0glb ⊢ φ → sup A 0 +∞ < < B ↔ ∃ x ∈ A x < B
4 3 notbid ⊢ φ → ¬ sup A 0 +∞ < < B ↔ ¬ ∃ x ∈ A x < B
5 iccssxr ⊢ 0 +∞ ⊆ ℝ *
6 5 2 sselid ⊢ φ → B ∈ ℝ *
7 xrltso ⊢ < Or ℝ *
8 soss ⊢ 0 +∞ ⊆ ℝ * → < Or ℝ * → < Or 0 +∞
9 5 7 8 mp2 ⊢ < Or 0 +∞
10 9 a1i ⊢ φ → < Or 0 +∞
11 xrge0infss ⊢ A ⊆ 0 +∞ → ∃ x ∈ 0 +∞ ∀ y ∈ A ¬ y < x ∧ ∀ y ∈ 0 +∞ x < y → ∃ z ∈ A z < y
12 1 11 syl ⊢ φ → ∃ x ∈ 0 +∞ ∀ y ∈ A ¬ y < x ∧ ∀ y ∈ 0 +∞ x < y → ∃ z ∈ A z < y
13 10 12 infcl ⊢ φ → sup A 0 +∞ < ∈ 0 +∞
14 5 13 sselid ⊢ φ → sup A 0 +∞ < ∈ ℝ *
15 6 14 xrlenltd ⊢ φ → B ≤ sup A 0 +∞ < ↔ ¬ sup A 0 +∞ < < B
16 6 adantr ⊢ φ ∧ x ∈ A → B ∈ ℝ *
17 1 5 sstrdi ⊢ φ → A ⊆ ℝ *
18 17 sselda ⊢ φ ∧ x ∈ A → x ∈ ℝ *
19 16 18 xrlenltd ⊢ φ ∧ x ∈ A → B ≤ x ↔ ¬ x < B
20 19 ralbidva ⊢ φ → ∀ x ∈ A B ≤ x ↔ ∀ x ∈ A ¬ x < B
21 ralnex ⊢ ∀ x ∈ A ¬ x < B ↔ ¬ ∃ x ∈ A x < B
22 20 21 bitrdi ⊢ φ → ∀ x ∈ A B ≤ x ↔ ¬ ∃ x ∈ A x < B
23 4 15 22 3bitr4d ⊢ φ → B ≤ sup A 0 +∞ < ↔ ∀ x ∈ A B ≤ x