Metamath Proof Explorer

Theorem infregelb

Description: Any lower bound of a nonempty set of real numbers is less than or equal to its infimum. (Contributed by Jeff Hankins, 1-Sep-2013) (Revised by AV, 4-Sep-2020) (Proof modification is discouraged.)

Ref Expression
Assertion infregelb ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A x ≤ y ∧ B ∈ ℝ → B ≤ inf A ℝ < ↔ ∀ z ∈ A B ≤ z

Proof

Step Hyp Ref Expression
1 ltso ⊢ < Or ℝ
2 1 a1i ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A x ≤ y → < Or ℝ
3 infm3 ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A x ≤ y → ∃ x ∈ ℝ ∀ y ∈ A ¬ y < x ∧ ∀ y ∈ ℝ x < y → ∃ w ∈ A w < y
4 simp1 ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A x ≤ y → A ⊆ ℝ
5 2 3 4 infglbb ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A x ≤ y ∧ B ∈ ℝ → inf A ℝ < < B ↔ ∃ w ∈ A w < B
6 5 notbid ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A x ≤ y ∧ B ∈ ℝ → ¬ inf A ℝ < < B ↔ ¬ ∃ w ∈ A w < B
7 infrecl ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A x ≤ y → inf A ℝ < ∈ ℝ
8 7 anim1i ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A x ≤ y ∧ B ∈ ℝ → inf A ℝ < ∈ ℝ ∧ B ∈ ℝ
9 8 ancomd ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A x ≤ y ∧ B ∈ ℝ → B ∈ ℝ ∧ inf A ℝ < ∈ ℝ
10 lenlt ⊢ B ∈ ℝ ∧ inf A ℝ < ∈ ℝ → B ≤ inf A ℝ < ↔ ¬ inf A ℝ < < B
11 9 10 syl ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A x ≤ y ∧ B ∈ ℝ → B ≤ inf A ℝ < ↔ ¬ inf A ℝ < < B
12 simplr ⊢ A ⊆ ℝ ∧ B ∈ ℝ ∧ w ∈ A → B ∈ ℝ
13 ssel ⊢ A ⊆ ℝ → w ∈ A → w ∈ ℝ
14 13 adantr ⊢ A ⊆ ℝ ∧ B ∈ ℝ → w ∈ A → w ∈ ℝ
15 14 imp ⊢ A ⊆ ℝ ∧ B ∈ ℝ ∧ w ∈ A → w ∈ ℝ
16 12 15 lenltd ⊢ A ⊆ ℝ ∧ B ∈ ℝ ∧ w ∈ A → B ≤ w ↔ ¬ w < B
17 16 ralbidva ⊢ A ⊆ ℝ ∧ B ∈ ℝ → ∀ w ∈ A B ≤ w ↔ ∀ w ∈ A ¬ w < B
18 17 3ad2antl1 ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A x ≤ y ∧ B ∈ ℝ → ∀ w ∈ A B ≤ w ↔ ∀ w ∈ A ¬ w < B
19 ralnex ⊢ ∀ w ∈ A ¬ w < B ↔ ¬ ∃ w ∈ A w < B
20 18 19 bitrdi ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A x ≤ y ∧ B ∈ ℝ → ∀ w ∈ A B ≤ w ↔ ¬ ∃ w ∈ A w < B
21 6 11 20 3bitr4d ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A x ≤ y ∧ B ∈ ℝ → B ≤ inf A ℝ < ↔ ∀ w ∈ A B ≤ w
22 breq2 ⊢ w = z → B ≤ w ↔ B ≤ z
23 22 cbvralvw ⊢ ∀ w ∈ A B ≤ w ↔ ∀ z ∈ A B ≤ z
24 21 23 bitrdi ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A x ≤ y ∧ B ∈ ℝ → B ≤ inf A ℝ < ↔ ∀ z ∈ A B ≤ z