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	$$⊢\left(S\subseteq ℝ\wedge \exists x\in S\forall y\in Sx\le y\right)\to \left(\iota x\in S|\forall y\in Sx\le y\right)\in S$$

Proof

Step	Hyp	Ref	Expression
1		lbreu	$$⊢\left(S\subseteq ℝ\wedge \exists x\in S\forall y\in Sx\le y\right)\to \exists !x\in S\forall y\in Sx\le y$$
2		riotacl	$$⊢\exists !x\in S\forall y\in Sx\le y\to \left(\iota x\in S|\forall y\in Sx\le y\right)\in S$$
3	1 2	syl	$$⊢\left(S\subseteq ℝ\wedge \exists x\in S\forall y\in Sx\le y\right)\to \left(\iota x\in S|\forall y\in Sx\le y\right)\in S$$