Metamath Proof Explorer

Theorem infmrgelbi

Description: Any lower bound of a nonempty set of real numbers is less than or equal to its infimum, one-direction version. (Contributed by Stefan O'Rear, 1-Sep-2013) (Revised by AV, 17-Sep-2020)

Ref Expression
Assertion infmrgelbi ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ B ∈ ℝ ∧ ∀ x ∈ A B ≤ x → B ≤ inf A ℝ <

Proof

Step Hyp Ref Expression
1 simpr ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ B ∈ ℝ ∧ ∀ x ∈ A B ≤ x → ∀ x ∈ A B ≤ x
2 simpl1 ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ B ∈ ℝ ∧ ∀ x ∈ A B ≤ x → A ⊆ ℝ
3 simpl2 ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ B ∈ ℝ ∧ ∀ x ∈ A B ≤ x → A ≠ ∅
4 breq1 ⊢ z = B → z ≤ x ↔ B ≤ x
5 4 ralbidv ⊢ z = B → ∀ x ∈ A z ≤ x ↔ ∀ x ∈ A B ≤ x
6 5 rspcev ⊢ B ∈ ℝ ∧ ∀ x ∈ A B ≤ x → ∃ z ∈ ℝ ∀ x ∈ A z ≤ x
7 6 3ad2antl3 ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ B ∈ ℝ ∧ ∀ x ∈ A B ≤ x → ∃ z ∈ ℝ ∀ x ∈ A z ≤ x
8 simpl3 ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ B ∈ ℝ ∧ ∀ x ∈ A B ≤ x → B ∈ ℝ
9 infregelb ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ z ∈ ℝ ∀ x ∈ A z ≤ x ∧ B ∈ ℝ → B ≤ inf A ℝ < ↔ ∀ x ∈ A B ≤ x
10 2 3 7 8 9 syl31anc ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ B ∈ ℝ ∧ ∀ x ∈ A B ≤ x → B ≤ inf A ℝ < ↔ ∀ x ∈ A B ≤ x
11 1 10 mpbird ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ B ∈ ℝ ∧ ∀ x ∈ A B ≤ x → B ≤ inf A ℝ <