Theorem supxrbnd1

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

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

Proof

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