Theorem supxrre3

Description: The supremum of a nonempty set of reals, is real if and only if it is bounded-above . (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	supxrre3	$$⊢\left(A\subseteq ℝ\wedge A\ne \varnothing \right)\to \left(sup\left(A,{ℝ}^{*},<\right)\in ℝ\leftrightarrow \exists x\in ℝ\forall y\in Ay\le x\right)$$

Proof

Step	Hyp	Ref	Expression
1		supxrre1	$$⊢\left(A\subseteq ℝ\wedge A\ne \varnothing \right)\to \left(sup\left(A,{ℝ}^{*},<\right)\in ℝ\leftrightarrow sup\left(A,{ℝ}^{*},<\right)<\mathrm{+\infty }\right)$$
2		id	$$⊢A\subseteq ℝ\to A\subseteq ℝ$$
3		rexr	$$⊢x\in ℝ\to x\in {ℝ}^{*}$$
4	3	ssriv	$$⊢ℝ\subseteq {ℝ}^{*}$$
5	4	a1i	$$⊢A\subseteq ℝ\to ℝ\subseteq {ℝ}^{*}$$
6	2 5	sstrd	$$⊢A\subseteq ℝ\to A\subseteq {ℝ}^{*}$$
7		supxrbnd2	$$⊢A\subseteq {ℝ}^{*}\to \left(\exists x\in ℝ\forall y\in Ay\le x\leftrightarrow sup\left(A,{ℝ}^{*},<\right)<\mathrm{+\infty }\right)$$
8	6 7	syl	$$⊢A\subseteq ℝ\to \left(\exists x\in ℝ\forall y\in Ay\le x\leftrightarrow sup\left(A,{ℝ}^{*},<\right)<\mathrm{+\infty }\right)$$
9	8	bicomd	$$⊢A\subseteq ℝ\to \left(sup\left(A,{ℝ}^{*},<\right)<\mathrm{+\infty }\leftrightarrow \exists x\in ℝ\forall y\in Ay\le x\right)$$
10	9	adantr	$$⊢\left(A\subseteq ℝ\wedge A\ne \varnothing \right)\to \left(sup\left(A,{ℝ}^{*},<\right)<\mathrm{+\infty }\leftrightarrow \exists x\in ℝ\forall y\in Ay\le x\right)$$
11	1 10	bitrd	$$⊢\left(A\subseteq ℝ\wedge A\ne \varnothing \right)\to \left(sup\left(A,{ℝ}^{*},<\right)\in ℝ\leftrightarrow \exists x\in ℝ\forall y\in Ay\le x\right)$$