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 ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑥𝑦 ) ∧ 𝐵 ∈ ℝ ) → ( 𝐵 ≤ inf ( 𝐴 , ℝ , < ) ↔ ∀ 𝑧𝐴 𝐵𝑧 ) )

Proof

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