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 ( 𝐴 , ℝ , < ) )