Metamath Proof Explorer

Theorem infxrge0glb

Description: The infimum of a set of nonnegative extended reals is the greatest 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 infxrge0glb ⊢ φ → sup A 0 +∞ < < B ↔ ∃ x ∈ A x < B

Proof

Step Hyp Ref Expression
1 infxrge0glb.a ⊢ φ → A ⊆ 0 +∞
2 infxrge0glb.b ⊢ φ → B ∈ 0 +∞
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 1 infglbb ⊢ φ ∧ B ∈ 0 +∞ → sup A 0 +∞ < < B ↔ ∃ z ∈ A z < B
11 2 10 mpdan ⊢ φ → sup A 0 +∞ < < B ↔ ∃ z ∈ A z < B
12 breq1 ⊢ x = z → x < B ↔ z < B
13 12 cbvrexvw ⊢ ∃ x ∈ A x < B ↔ ∃ z ∈ A z < B
14 11 13 bitr4di ⊢ φ → sup A 0 +∞ < < B ↔ ∃ x ∈ A x < B