Metamath Proof Explorer


Theorem infmrgelbi

Description: Any lower bound of a nonempty set of real numbers is less than or equal to its infimum, one-direction version. (Contributed by Stefan O'Rear, 1-Sep-2013) (Revised by AV, 17-Sep-2020)

Ref Expression
Assertion infmrgelbi ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ 𝐵 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝐵𝑥 ) → 𝐵 ≤ inf ( 𝐴 , ℝ , < ) )

Proof

Step Hyp Ref Expression
1 simpr ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ 𝐵 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝐵𝑥 ) → ∀ 𝑥𝐴 𝐵𝑥 )
2 simpl1 ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ 𝐵 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝐵𝑥 ) → 𝐴 ⊆ ℝ )
3 simpl2 ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ 𝐵 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝐵𝑥 ) → 𝐴 ≠ ∅ )
4 breq1 ( 𝑧 = 𝐵 → ( 𝑧𝑥𝐵𝑥 ) )
5 4 ralbidv ( 𝑧 = 𝐵 → ( ∀ 𝑥𝐴 𝑧𝑥 ↔ ∀ 𝑥𝐴 𝐵𝑥 ) )
6 5 rspcev ( ( 𝐵 ∈ ℝ ∧ ∀ 𝑥𝐴 𝐵𝑥 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥𝐴 𝑧𝑥 )
7 6 3ad2antl3 ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ 𝐵 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝐵𝑥 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥𝐴 𝑧𝑥 )
8 simpl3 ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ 𝐵 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝐵𝑥 ) → 𝐵 ∈ ℝ )
9 infregelb ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑥𝐴 𝑧𝑥 ) ∧ 𝐵 ∈ ℝ ) → ( 𝐵 ≤ inf ( 𝐴 , ℝ , < ) ↔ ∀ 𝑥𝐴 𝐵𝑥 ) )
10 2 3 7 8 9 syl31anc ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ 𝐵 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝐵𝑥 ) → ( 𝐵 ≤ inf ( 𝐴 , ℝ , < ) ↔ ∀ 𝑥𝐴 𝐵𝑥 ) )
11 1 10 mpbird ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ 𝐵 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝐵𝑥 ) → 𝐵 ≤ inf ( 𝐴 , ℝ , < ) )