Metamath Proof Explorer

Theorem infxrgelb

Description: The infimum of a set of extended reals is greater than or equal to a lower bound. (Contributed by Mario Carneiro, 16-Mar-2014) (Revised by AV, 5-Sep-2020)

Ref Expression
Assertion infxrgelb ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * → B ≤ sup A ℝ * < ↔ ∀ x ∈ A B ≤ x

Proof

Step Hyp Ref Expression
1 xrltso ⊢ < Or ℝ *
2 1 a1i ⊢ A ⊆ ℝ * → < Or ℝ *
3 xrinfmss ⊢ A ⊆ ℝ * → ∃ z ∈ ℝ * ∀ y ∈ A ¬ y < z ∧ ∀ y ∈ ℝ * z < y → ∃ x ∈ A x < y
4 id ⊢ A ⊆ ℝ * → A ⊆ ℝ *
5 2 3 4 infglbb ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * → sup A ℝ * < < B ↔ ∃ x ∈ A x < B
6 5 notbid ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * → ¬ sup A ℝ * < < B ↔ ¬ ∃ x ∈ A x < B
7 ralnex ⊢ ∀ x ∈ A ¬ x < B ↔ ¬ ∃ x ∈ A x < B
8 6 7 bitr4di ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * → ¬ sup A ℝ * < < B ↔ ∀ x ∈ A ¬ x < B
9 id ⊢ B ∈ ℝ * → B ∈ ℝ *
10 infxrcl ⊢ A ⊆ ℝ * → sup A ℝ * < ∈ ℝ *
11 xrlenlt ⊢ B ∈ ℝ * ∧ sup A ℝ * < ∈ ℝ * → B ≤ sup A ℝ * < ↔ ¬ sup A ℝ * < < B
12 9 10 11 syl2anr ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * → B ≤ sup A ℝ * < ↔ ¬ sup A ℝ * < < B
13 simplr ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * ∧ x ∈ A → B ∈ ℝ *
14 simpl ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * → A ⊆ ℝ *
15 14 sselda ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * ∧ x ∈ A → x ∈ ℝ *
16 13 15 xrlenltd ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * ∧ x ∈ A → B ≤ x ↔ ¬ x < B
17 16 ralbidva ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * → ∀ x ∈ A B ≤ x ↔ ∀ x ∈ A ¬ x < B
18 8 12 17 3bitr4d ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * → B ≤ sup A ℝ * < ↔ ∀ x ∈ A B ≤ x