Metamath Proof Explorer

Theorem lbinfle

Description: If a set of reals contains a lower bound, its infimum is less than or equal to all members of the set. (Contributed by NM, 11-Oct-2005) (Revised by AV, 4-Sep-2020)

		Ref	Expression
	Assertion	lbinfle	$⊢ (S \subseteq ℝ \land \exists x \in S \forall y \in S x \leq y \land A \in S) \to sup (S ℝ <) \leq A$

Proof

Step	Hyp	Ref	Expression
1		lbinf	$⊢ (S \subseteq ℝ \land \exists x \in S \forall y \in S x \leq y) \to sup (S ℝ <) = (ι x \in S \| \forall y \in S x \leq y)$
2	1	3adant3	$⊢ (S \subseteq ℝ \land \exists x \in S \forall y \in S x \leq y \land A \in S) \to sup (S ℝ <) = (ι x \in S \| \forall y \in S x \leq y)$
3		lble	$⊢ (S \subseteq ℝ \land \exists x \in S \forall y \in S x \leq y \land A \in S) \to (ι x \in S \| \forall y \in S x \leq y) \leq A$
4	2 3	eqbrtrd	$⊢ (S \subseteq ℝ \land \exists x \in S \forall y \in S x \leq y \land A \in S) \to sup (S ℝ <) \leq A$