Theorem supxrbnd2

Description: The supremum of a bounded-above set of extended reals is less than infinity. (Contributed by NM, 30-Jan-2006)

	Ref	Expression
Assertion	supxrbnd2	$$⊢A\subseteq {ℝ}^{*}\to \left(\exists x\in ℝ\forall y\in Ay\le x\leftrightarrow sup\left(A,{ℝ}^{*},<\right)<\mathrm{+\infty }\right)$$

Proof

Step	Hyp	Ref	Expression
1		ralnex	$$⊢\forall x\in ℝ\neg \forall y\in Ay\le x\leftrightarrow \neg \exists x\in ℝ\forall y\in Ay\le x$$
2		ssel2	$$⊢\left(A\subseteq {ℝ}^{*}\wedge y\in A\right)\to y\in {ℝ}^{*}$$
3		rexr	$$⊢x\in ℝ\to x\in {ℝ}^{*}$$
4		xrlenlt	$$⊢\left(y\in {ℝ}^{*}\wedge x\in {ℝ}^{*}\right)\to \left(y\le x\leftrightarrow \neg x<y\right)$$
5	4	con2bid	$$⊢\left(y\in {ℝ}^{*}\wedge x\in {ℝ}^{*}\right)\to \left(x<y\leftrightarrow \neg y\le x\right)$$
6	2 3 5	syl2an	$$⊢\left(\left(A\subseteq {ℝ}^{*}\wedge y\in A\right)\wedge x\in ℝ\right)\to \left(x<y\leftrightarrow \neg y\le x\right)$$
7	6	an32s	$$⊢\left(\left(A\subseteq {ℝ}^{*}\wedge x\in ℝ\right)\wedge y\in A\right)\to \left(x<y\leftrightarrow \neg y\le x\right)$$
8	7	rexbidva	$$⊢\left(A\subseteq {ℝ}^{*}\wedge x\in ℝ\right)\to \left(\exists y\in Ax<y\leftrightarrow \exists y\in A\neg y\le x\right)$$
9		rexnal	$$⊢\exists y\in A\neg y\le x\leftrightarrow \neg \forall y\in Ay\le x$$
10	8 9	bitr2di	$$⊢\left(A\subseteq {ℝ}^{*}\wedge x\in ℝ\right)\to \left(\neg \forall y\in Ay\le x\leftrightarrow \exists y\in Ax<y\right)$$
11	10	ralbidva	$$⊢A\subseteq {ℝ}^{*}\to \left(\forall x\in ℝ\neg \forall y\in Ay\le x\leftrightarrow \forall x\in ℝ\exists y\in Ax<y\right)$$
12	1 11	bitr3id	$$⊢A\subseteq {ℝ}^{*}\to \left(\neg \exists x\in ℝ\forall y\in Ay\le x\leftrightarrow \forall x\in ℝ\exists y\in Ax<y\right)$$
13		supxrunb2	$$⊢A\subseteq {ℝ}^{*}\to \left(\forall x\in ℝ\exists y\in Ax<y\leftrightarrow sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }\right)$$
14		supxrcl	$$⊢A\subseteq {ℝ}^{*}\to sup\left(A,{ℝ}^{*},<\right)\in {ℝ}^{*}$$
15		nltpnft	$$⊢sup\left(A,{ℝ}^{*},<\right)\in {ℝ}^{*}\to \left(sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }\leftrightarrow \neg sup\left(A,{ℝ}^{*},<\right)<\mathrm{+\infty }\right)$$
16	14 15	syl	$$⊢A\subseteq {ℝ}^{*}\to \left(sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }\leftrightarrow \neg sup\left(A,{ℝ}^{*},<\right)<\mathrm{+\infty }\right)$$
17	12 13 16	3bitrd	$$⊢A\subseteq {ℝ}^{*}\to \left(\neg \exists x\in ℝ\forall y\in Ay\le x\leftrightarrow \neg sup\left(A,{ℝ}^{*},<\right)<\mathrm{+\infty }\right)$$
18	17	con4bid	$$⊢A\subseteq {ℝ}^{*}\to \left(\exists x\in ℝ\forall y\in Ay\le x\leftrightarrow sup\left(A,{ℝ}^{*},<\right)<\mathrm{+\infty }\right)$$