Theorem infrefilb

Description: The infimum of a finite set of reals is less than or equal to any of its elements. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Assertion	infrefilb	⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝐵 ∈ Fin ∧ 𝐴 ∈ 𝐵 ) → inf ( 𝐵 , ℝ , < ) ≤ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝐵 ∈ Fin ∧ 𝐴 ∈ 𝐵 ) → 𝐵 ⊆ ℝ )
2		fiminre2	⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝐵 ∈ Fin ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 )
3	2	3adant3	⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝐵 ∈ Fin ∧ 𝐴 ∈ 𝐵 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 )
4		simp3	⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝐵 ∈ Fin ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ 𝐵 )
5		infrelb	⊢ ( ( 𝐵 ⊆ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 ∧ 𝐴 ∈ 𝐵 ) → inf ( 𝐵 , ℝ , < ) ≤ 𝐴 )
6	1 3 4 5	syl3anc	⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝐵 ∈ Fin ∧ 𝐴 ∈ 𝐵 ) → inf ( 𝐵 , ℝ , < ) ≤ 𝐴 )