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