Theorem supxrre2

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

	Ref	Expression
Assertion	supxrre2	$$⊢\left(A\subseteq ℝ\wedge A\ne \varnothing \right)\to \left(sup\left(A,{ℝ}^{*},<\right)\in ℝ\leftrightarrow sup\left(A,{ℝ}^{*},<\right)\ne \mathrm{+\infty }\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		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		nltpnft	$$⊢sup\left(A,{ℝ}^{*},<\right)\in {ℝ}^{*}\to \left(sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }\leftrightarrow \neg sup\left(A,{ℝ}^{*},<\right)<\mathrm{+\infty }\right)$$
7	4 5 6	3syl	$$⊢A\subseteq ℝ\to \left(sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }\leftrightarrow \neg sup\left(A,{ℝ}^{*},<\right)<\mathrm{+\infty }\right)$$
8	7	necon2abid	$$⊢A\subseteq ℝ\to \left(sup\left(A,{ℝ}^{*},<\right)<\mathrm{+\infty }\leftrightarrow sup\left(A,{ℝ}^{*},<\right)\ne \mathrm{+\infty }\right)$$
9	8	adantr	$$⊢\left(A\subseteq ℝ\wedge A\ne \varnothing \right)\to \left(sup\left(A,{ℝ}^{*},<\right)<\mathrm{+\infty }\leftrightarrow sup\left(A,{ℝ}^{*},<\right)\ne \mathrm{+\infty }\right)$$
10	1 9	bitrd	$$⊢\left(A\subseteq ℝ\wedge A\ne \varnothing \right)\to \left(sup\left(A,{ℝ}^{*},<\right)\in ℝ\leftrightarrow sup\left(A,{ℝ}^{*},<\right)\ne \mathrm{+\infty }\right)$$