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	$⊢ (B \subseteq ℝ \land B \in Fin \land A \in B) \to sup (B ℝ <) \leq A$

Step	Hyp	Ref	Expression
1		simp1	$⊢ (B \subseteq ℝ \land B \in Fin \land A \in B) \to B \subseteq ℝ$
2		fiminre2	$⊢ (B \subseteq ℝ \land B \in Fin) \to \exists x \in ℝ \forall y \in B x \leq y$
3	2	3adant3	$⊢ (B \subseteq ℝ \land B \in Fin \land A \in B) \to \exists x \in ℝ \forall y \in B x \leq y$
4		simp3	$⊢ (B \subseteq ℝ \land B \in Fin \land A \in B) \to A \in B$
5		infrelb	$⊢ (B \subseteq ℝ \land \exists x \in ℝ \forall y \in B x \leq y \land A \in B) \to sup (B ℝ <) \leq A$
6	1 3 4 5	syl3anc	$⊢ (B \subseteq ℝ \land B \in Fin \land A \in B) \to sup (B ℝ <) \leq A$

Metamath Proof Explorer