Theorem suprltrp

Description: The supremum of a nonempty bounded set of reals can be approximated from below by elements of the set. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	suprltrp.a	$$⊢\phi \to A\subseteq ℝ$$
	suprltrp.n0	$$⊢\phi \to A\ne \varnothing$$
	suprltrp.bnd	$$⊢\phi \to \exists x\in ℝ\forall y\in Ay\le x$$
	suprltrp.x	$$⊢\phi \to X\in {ℝ}^{+}$$
Assertion	suprltrp	$$⊢\phi \to \exists z\in Asup\left(A,ℝ,<\right)-X<z$$

Proof

Step	Hyp	Ref	Expression
1		suprltrp.a	$$⊢\phi \to A\subseteq ℝ$$
2		suprltrp.n0	$$⊢\phi \to A\ne \varnothing$$
3		suprltrp.bnd	$$⊢\phi \to \exists x\in ℝ\forall y\in Ay\le x$$
4		suprltrp.x	$$⊢\phi \to X\in {ℝ}^{+}$$
5		suprcl	$$⊢\left(A\subseteq ℝ\wedge A\ne \varnothing \wedge \exists x\in ℝ\forall y\in Ay\le x\right)\to sup\left(A,ℝ,<\right)\in ℝ$$
6	1 2 3 5	syl3anc	$$⊢\phi \to sup\left(A,ℝ,<\right)\in ℝ$$
7	6 4	ltsubrpd	$$⊢\phi \to sup\left(A,ℝ,<\right)-X<sup\left(A,ℝ,<\right)$$
8	4	rpred	$$⊢\phi \to X\in ℝ$$
9	6 8	resubcld	$$⊢\phi \to sup\left(A,ℝ,<\right)-X\in ℝ$$
10		suprlub	$$⊢\left(\left(A\subseteq ℝ\wedge A\ne \varnothing \wedge \exists x\in ℝ\forall y\in Ay\le x\right)\wedge sup\left(A,ℝ,<\right)-X\in ℝ\right)\to \left(sup\left(A,ℝ,<\right)-X<sup\left(A,ℝ,<\right)\leftrightarrow \exists z\in Asup\left(A,ℝ,<\right)-X<z\right)$$
11	1 2 3 9 10	syl31anc	$$⊢\phi \to \left(sup\left(A,ℝ,<\right)-X<sup\left(A,ℝ,<\right)\leftrightarrow \exists z\in Asup\left(A,ℝ,<\right)-X<z\right)$$
12	7 11	mpbid	$$⊢\phi \to \exists z\in Asup\left(A,ℝ,<\right)-X<z$$