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∈Bx≤y∧A∈B→supBℝ<≤A

Proof

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