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∈Ax≤y∧B∈ℝ→B≤supAℝ<↔∀z∈AB≤z

Proof

Step Hyp Ref Expression
1 ltso ⊢<Orℝ
2 1 a1i ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ax≤y→<Orℝ
3 infm3 ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ax≤y→∃x∈ℝ∀y∈A¬y<x∧∀y∈ℝx<y→∃w∈Aw<y
4 simp1 ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ax≤y→A⊆ℝ
5 2 3 4 infglbb ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ax≤y∧B∈ℝ→supAℝ<<B↔∃w∈Aw<B
6 5 notbid ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ax≤y∧B∈ℝ→¬supAℝ<<B↔¬∃w∈Aw<B
7 infrecl ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ax≤y→supAℝ<∈ℝ
8 7 anim1i ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ax≤y∧B∈ℝ→supAℝ<∈ℝ∧B∈ℝ
9 8 ancomd ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ax≤y∧B∈ℝ→B∈ℝ∧supAℝ<∈ℝ
10 lenlt ⊢B∈ℝ∧supAℝ<∈ℝ→B≤supAℝ<↔¬supAℝ<<B
11 9 10 syl ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ax≤y∧B∈ℝ→B≤supAℝ<↔¬supAℝ<<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∈AB≤w↔∀w∈A¬w<B
18 17 3ad2antl1 ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ax≤y∧B∈ℝ→∀w∈AB≤w↔∀w∈A¬w<B
19 ralnex ⊢∀w∈A¬w<B↔¬∃w∈Aw<B
20 18 19 bitrdi ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ax≤y∧B∈ℝ→∀w∈AB≤w↔¬∃w∈Aw<B
21 6 11 20 3bitr4d ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ax≤y∧B∈ℝ→B≤supAℝ<↔∀w∈AB≤w
22 breq2 ⊢w=z→B≤w↔B≤z
23 22 cbvralvw ⊢∀w∈AB≤w↔∀z∈AB≤z
24 21 23 bitrdi ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ax≤y∧B∈ℝ→B≤supAℝ<↔∀z∈AB≤z