This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lbcl

Description: If a set of reals contains a lower bound, it contains a unique lower bound that belongs to the set. (Contributed by NM, 9-Oct-2005) (Revised by Mario Carneiro, 24-Dec-2016)

		Ref	Expression
	Assertion	lbcl	$⊢ (S \subseteq ℝ \land \exists x \in S \forall y \in S x \leq y) \to (ι x \in S \| \forall y \in S x \leq y) \in S$

Proof

Step	Hyp	Ref	Expression
1		lbreu	$⊢ (S \subseteq ℝ \land \exists x \in S \forall y \in S x \leq y) \to \exists! x \in S \forall y \in S x \leq y$
2		riotacl	$⊢ \exists! x \in S \forall y \in S x \leq y \to (ι x \in S \| \forall y \in S x \leq y) \in S$
3	1 2	syl	$⊢ (S \subseteq ℝ \land \exists x \in S \forall y \in S x \leq y) \to (ι x \in S \| \forall y \in S x \leq y) \in S$