Theorem supxrre1

Description: The supremum of a nonempty set of reals is real iff it is less than plus infinity. (Contributed by NM, 5-Feb-2006)

	Ref	Expression
Assertion	supxrre1	$$⊢\left(A\subseteq ℝ\wedge A\ne \varnothing \right)\to \left(sup\left(A,{ℝ}^{*},<\right)\in ℝ\leftrightarrow sup\left(A,{ℝ}^{*},<\right)<\mathrm{+\infty }\right)$$

Proof

Step	Hyp	Ref	Expression
1		supxrgtmnf	$$⊢\left(A\subseteq ℝ\wedge A\ne \varnothing \right)\to \mathrm{-\infty }<sup\left(A,{ℝ}^{*},<\right)$$
2		ressxr	$$⊢ℝ\subseteq {ℝ}^{*}$$
3		sstr	$$⊢\left(A\subseteq ℝ\wedge ℝ\subseteq {ℝ}^{*}\right)\to A\subseteq {ℝ}^{*}$$
4	2 3	mpan2	$$⊢A\subseteq ℝ\to A\subseteq {ℝ}^{*}$$
5		supxrcl	$$⊢A\subseteq {ℝ}^{*}\to sup\left(A,{ℝ}^{*},<\right)\in {ℝ}^{*}$$
6		xrrebnd	$$⊢sup\left(A,{ℝ}^{*},<\right)\in {ℝ}^{*}\to \left(sup\left(A,{ℝ}^{*},<\right)\in ℝ\leftrightarrow \left(\mathrm{-\infty }<sup\left(A,{ℝ}^{*},<\right)\wedge sup\left(A,{ℝ}^{*},<\right)<\mathrm{+\infty }\right)\right)$$
7	4 5 6	3syl	$$⊢A\subseteq ℝ\to \left(sup\left(A,{ℝ}^{*},<\right)\in ℝ\leftrightarrow \left(\mathrm{-\infty }<sup\left(A,{ℝ}^{*},<\right)\wedge sup\left(A,{ℝ}^{*},<\right)<\mathrm{+\infty }\right)\right)$$
8	7	adantr	$$⊢\left(A\subseteq ℝ\wedge A\ne \varnothing \right)\to \left(sup\left(A,{ℝ}^{*},<\right)\in ℝ\leftrightarrow \left(\mathrm{-\infty }<sup\left(A,{ℝ}^{*},<\right)\wedge sup\left(A,{ℝ}^{*},<\right)<\mathrm{+\infty }\right)\right)$$
9	1 8	mpbirand	$$⊢\left(A\subseteq ℝ\wedge A\ne \varnothing \right)\to \left(sup\left(A,{ℝ}^{*},<\right)\in ℝ\leftrightarrow sup\left(A,{ℝ}^{*},<\right)<\mathrm{+\infty }\right)$$