Theorem lble

Description: If a set of reals contains a lower bound, the lower bound is less than or equal to all members of the set. (Contributed by NM, 9-Oct-2005) (Proof shortened by Mario Carneiro, 24-Dec-2016)

	Ref	Expression
Assertion	lble	$$⊢\left(S\subseteq ℝ\wedge \exists x\in S\forall y\in Sx\le y\wedge A\in S\right)\to \left(\iota x\in S|\forall y\in Sx\le y\right)\le A$$

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		nfcv	$$⊢\underset{\_}{Ⅎ}xS$$
3		nfriota1	$$⊢\underset{\_}{Ⅎ}x\left(\iota x\in S|\forall y\in Sx\le y\right)$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}x\le$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
6	3 4 5	nfbr	$$⊢Ⅎx\left(\iota x\in S|\forall y\in Sx\le y\right)\le y$$
7	2 6	nfralw	$$⊢Ⅎx\forall y\in S\left(\iota x\in S|\forall y\in Sx\le y\right)\le y$$
8		eqid	$$⊢\left(\iota x\in S|\forall y\in Sx\le y\right)=\left(\iota x\in S|\forall y\in Sx\le y\right)$$
9		nfra1	$$⊢Ⅎy\forall y\in Sx\le y$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}yS$$
11	9 10	nfriota	$$⊢\underset{\_}{Ⅎ}y\left(\iota x\in S|\forall y\in Sx\le y\right)$$
12	11	nfeq2	$$⊢Ⅎyx=\left(\iota x\in S|\forall y\in Sx\le y\right)$$
13		breq1	$$⊢x=\left(\iota x\in S|\forall y\in Sx\le y\right)\to \left(x\le y\leftrightarrow \left(\iota x\in S|\forall y\in Sx\le y\right)\le y\right)$$
14	12 13	ralbid	$$⊢x=\left(\iota x\in S|\forall y\in Sx\le y\right)\to \left(\forall y\in Sx\le y\leftrightarrow \forall y\in S\left(\iota x\in S|\forall y\in Sx\le y\right)\le y\right)$$
15	7 8 14	riotaprop	$$⊢\exists !x\in S\forall y\in Sx\le y\to \left(\left(\iota x\in S|\forall y\in Sx\le y\right)\in S\wedge \forall y\in S\left(\iota x\in S|\forall y\in Sx\le y\right)\le y\right)$$
16	1 15	syl	$$⊢\left(S\subseteq ℝ\wedge \exists x\in S\forall y\in Sx\le y\right)\to \left(\left(\iota x\in S|\forall y\in Sx\le y\right)\in S\wedge \forall y\in S\left(\iota x\in S|\forall y\in Sx\le y\right)\le y\right)$$
17	16	simprd	$$⊢\left(S\subseteq ℝ\wedge \exists x\in S\forall y\in Sx\le y\right)\to \forall y\in S\left(\iota x\in S|\forall y\in Sx\le y\right)\le y$$
18		nfcv	$$⊢\underset{\_}{Ⅎ}y\le$$
19		nfcv	$$⊢\underset{\_}{Ⅎ}yA$$
20	11 18 19	nfbr	$$⊢Ⅎy\left(\iota x\in S|\forall y\in Sx\le y\right)\le A$$
21		breq2	$$⊢y=A\to \left(\left(\iota x\in S|\forall y\in Sx\le y\right)\le y\leftrightarrow \left(\iota x\in S|\forall y\in Sx\le y\right)\le A\right)$$
22	20 21	rspc	$$⊢A\in S\to \left(\forall y\in S\left(\iota x\in S|\forall y\in Sx\le y\right)\le y\to \left(\iota x\in S|\forall y\in Sx\le y\right)\le A\right)$$
23	17 22	mpan9	$$⊢\left(\left(S\subseteq ℝ\wedge \exists x\in S\forall y\in Sx\le y\right)\wedge A\in S\right)\to \left(\iota x\in S|\forall y\in Sx\le y\right)\le A$$
24	23	3impa	$$⊢\left(S\subseteq ℝ\wedge \exists x\in S\forall y\in Sx\le y\wedge A\in S\right)\to \left(\iota x\in S|\forall y\in Sx\le y\right)\le A$$