Metamath Proof Explorer

Theorem infrelb

Description: If a nonempty set of real numbers has a lower bound, its infimum is less than or equal to any of its elements. (Contributed by Jeff Hankins, 15-Sep-2013) (Revised by AV, 4-Sep-2020)

Ref Expression
Assertion infrelb ⊢ B ⊆ ℝ ∧ ∃ x ∈ ℝ ∀ y ∈ B x ≤ y ∧ A ∈ B → inf B ℝ < ≤ A

Proof

Step Hyp Ref Expression
1 simp1 ⊢ B ⊆ ℝ ∧ ∃ x ∈ ℝ ∀ y ∈ B x ≤ y ∧ A ∈ B → B ⊆ ℝ
2 ne0i ⊢ A ∈ B → B ≠ ∅
3 2 3ad2ant3 ⊢ B ⊆ ℝ ∧ ∃ x ∈ ℝ ∀ y ∈ B x ≤ y ∧ A ∈ B → B ≠ ∅
4 simp2 ⊢ B ⊆ ℝ ∧ ∃ x ∈ ℝ ∀ y ∈ B x ≤ y ∧ A ∈ B → ∃ x ∈ ℝ ∀ y ∈ B x ≤ y
5 infrecl ⊢ B ⊆ ℝ ∧ B ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ B x ≤ y → inf B ℝ < ∈ ℝ
6 1 3 4 5 syl3anc ⊢ B ⊆ ℝ ∧ ∃ x ∈ ℝ ∀ y ∈ B x ≤ y ∧ A ∈ B → inf B ℝ < ∈ ℝ
7 ssel2 ⊢ B ⊆ ℝ ∧ A ∈ B → A ∈ ℝ
8 7 3adant2 ⊢ B ⊆ ℝ ∧ ∃ x ∈ ℝ ∀ y ∈ B x ≤ y ∧ A ∈ B → A ∈ ℝ
9 ltso ⊢ < Or ℝ
10 9 a1i ⊢ B ⊆ ℝ ∧ ∃ x ∈ ℝ ∀ y ∈ B x ≤ y ∧ A ∈ B → < Or ℝ
11 simpll ⊢ B ⊆ ℝ ∧ ∃ x ∈ ℝ ∀ y ∈ B x ≤ y ∧ A ∈ B → B ⊆ ℝ
12 2 adantl ⊢ B ⊆ ℝ ∧ ∃ x ∈ ℝ ∀ y ∈ B x ≤ y ∧ A ∈ B → B ≠ ∅
13 simplr ⊢ B ⊆ ℝ ∧ ∃ x ∈ ℝ ∀ y ∈ B x ≤ y ∧ A ∈ B → ∃ x ∈ ℝ ∀ y ∈ B x ≤ y
14 infm3 ⊢ B ⊆ ℝ ∧ B ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ B x ≤ y → ∃ x ∈ ℝ ∀ y ∈ B ¬ y < x ∧ ∀ y ∈ ℝ x < y → ∃ z ∈ B z < y
15 11 12 13 14 syl3anc ⊢ B ⊆ ℝ ∧ ∃ x ∈ ℝ ∀ y ∈ B x ≤ y ∧ A ∈ B → ∃ x ∈ ℝ ∀ y ∈ B ¬ y < x ∧ ∀ y ∈ ℝ x < y → ∃ z ∈ B z < y
16 10 15 inflb ⊢ B ⊆ ℝ ∧ ∃ x ∈ ℝ ∀ y ∈ B x ≤ y ∧ A ∈ B → A ∈ B → ¬ A < inf B ℝ <
17 16 expcom ⊢ A ∈ B → B ⊆ ℝ ∧ ∃ x ∈ ℝ ∀ y ∈ B x ≤ y → A ∈ B → ¬ A < inf B ℝ <
18 17 pm2.43b ⊢ B ⊆ ℝ ∧ ∃ x ∈ ℝ ∀ y ∈ B x ≤ y → A ∈ B → ¬ A < inf B ℝ <
19 18 3impia ⊢ B ⊆ ℝ ∧ ∃ x ∈ ℝ ∀ y ∈ B x ≤ y ∧ A ∈ B → ¬ A < inf B ℝ <
20 6 8 19 nltled ⊢ B ⊆ ℝ ∧ ∃ x ∈ ℝ ∀ y ∈ B x ≤ y ∧ A ∈ B → inf B ℝ < ≤ A