Theorem supxrunb2

Description: The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by NM, 19-Jan-2006)

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

Proof

Step	Hyp	Ref	Expression
1		ssel	$$⊢A\subseteq {ℝ}^{*}\to \left(z\in A\to z\in {ℝ}^{*}\right)$$
2		pnfnlt	$$⊢z\in {ℝ}^{*}\to \neg \mathrm{+\infty }<z$$
3	1 2	syl6	$$⊢A\subseteq {ℝ}^{*}\to \left(z\in A\to \neg \mathrm{+\infty }<z\right)$$
4	3	ralrimiv	$$⊢A\subseteq {ℝ}^{*}\to \forall z\in A\neg \mathrm{+\infty }<z$$
5	4	adantr	$$⊢\left(A\subseteq {ℝ}^{*}\wedge \forall x\in ℝ\exists y\in Ax<y\right)\to \forall z\in A\neg \mathrm{+\infty }<z$$
6		breq1	$$⊢x=z\to \left(x<y\leftrightarrow z<y\right)$$
7	6	rexbidv	$$⊢x=z\to \left(\exists y\in Ax<y\leftrightarrow \exists y\in Az<y\right)$$
8	7	rspcva	$$⊢\left(z\in ℝ\wedge \forall x\in ℝ\exists y\in Ax<y\right)\to \exists y\in Az<y$$
9	8	adantrr	$$⊢\left(z\in ℝ\wedge \left(\forall x\in ℝ\exists y\in Ax<y\wedge A\subseteq {ℝ}^{*}\right)\right)\to \exists y\in Az<y$$
10	9	ancoms	$$⊢\left(\left(\forall x\in ℝ\exists y\in Ax<y\wedge A\subseteq {ℝ}^{*}\right)\wedge z\in ℝ\right)\to \exists y\in Az<y$$
11	10	exp31	$$⊢\forall x\in ℝ\exists y\in Ax<y\to \left(A\subseteq {ℝ}^{*}\to \left(z\in ℝ\to \exists y\in Az<y\right)\right)$$
12	11	a1dd	$$⊢\forall x\in ℝ\exists y\in Ax<y\to \left(A\subseteq {ℝ}^{*}\to \left(z<\mathrm{+\infty }\to \left(z\in ℝ\to \exists y\in Az<y\right)\right)\right)$$
13	12	com4r	$$⊢z\in ℝ\to \left(\forall x\in ℝ\exists y\in Ax<y\to \left(A\subseteq {ℝ}^{*}\to \left(z<\mathrm{+\infty }\to \exists y\in Az<y\right)\right)\right)$$
14	13	com13	$$⊢A\subseteq {ℝ}^{*}\to \left(\forall x\in ℝ\exists y\in Ax<y\to \left(z\in ℝ\to \left(z<\mathrm{+\infty }\to \exists y\in Az<y\right)\right)\right)$$
15	14	imp	$$⊢\left(A\subseteq {ℝ}^{*}\wedge \forall x\in ℝ\exists y\in Ax<y\right)\to \left(z\in ℝ\to \left(z<\mathrm{+\infty }\to \exists y\in Az<y\right)\right)$$
16	15	ralrimiv	$$⊢\left(A\subseteq {ℝ}^{*}\wedge \forall x\in ℝ\exists y\in Ax<y\right)\to \forall z\in ℝ\left(z<\mathrm{+\infty }\to \exists y\in Az<y\right)$$
17	5 16	jca	$$⊢\left(A\subseteq {ℝ}^{*}\wedge \forall x\in ℝ\exists y\in Ax<y\right)\to \left(\forall z\in A\neg \mathrm{+\infty }<z\wedge \forall z\in ℝ\left(z<\mathrm{+\infty }\to \exists y\in Az<y\right)\right)$$
18		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
19		supxr	$$⊢\left(\left(A\subseteq {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\wedge \left(\forall z\in A\neg \mathrm{+\infty }<z\wedge \forall z\in ℝ\left(z<\mathrm{+\infty }\to \exists y\in Az<y\right)\right)\right)\to sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }$$
20	18 19	mpanl2	$$⊢\left(A\subseteq {ℝ}^{*}\wedge \left(\forall z\in A\neg \mathrm{+\infty }<z\wedge \forall z\in ℝ\left(z<\mathrm{+\infty }\to \exists y\in Az<y\right)\right)\right)\to sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }$$
21	17 20	syldan	$$⊢\left(A\subseteq {ℝ}^{*}\wedge \forall x\in ℝ\exists y\in Ax<y\right)\to sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }$$
22	21	ex	$$⊢A\subseteq {ℝ}^{*}\to \left(\forall x\in ℝ\exists y\in Ax<y\to sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }\right)$$
23		rexr	$$⊢x\in ℝ\to x\in {ℝ}^{*}$$
24	23	ad2antlr	$$⊢\left(\left(A\subseteq {ℝ}^{*}\wedge x\in ℝ\right)\wedge sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }\right)\to x\in {ℝ}^{*}$$
25		ltpnf	$$⊢x\in ℝ\to x<\mathrm{+\infty }$$
26		breq2	$$⊢sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }\to \left(x<sup\left(A,{ℝ}^{*},<\right)\leftrightarrow x<\mathrm{+\infty }\right)$$
27	25 26	imbitrrid	$$⊢sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }\to \left(x\in ℝ\to x<sup\left(A,{ℝ}^{*},<\right)\right)$$
28	27	impcom	$$⊢\left(x\in ℝ\wedge sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }\right)\to x<sup\left(A,{ℝ}^{*},<\right)$$
29	28	adantll	$$⊢\left(\left(A\subseteq {ℝ}^{*}\wedge x\in ℝ\right)\wedge sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }\right)\to x<sup\left(A,{ℝ}^{*},<\right)$$
30		xrltso	$$⊢<\mathrm{Or}{ℝ}^{*}$$
31	30	a1i	$$⊢\left(\left(A\subseteq {ℝ}^{*}\wedge x\in ℝ\right)\wedge sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }\right)\to <\mathrm{Or}{ℝ}^{*}$$
32		xrsupss	$$⊢A\subseteq {ℝ}^{*}\to \exists z\in {ℝ}^{*}\left(\forall w\in A\neg z<w\wedge \forall w\in {ℝ}^{*}\left(w<z\to \exists y\in Aw<y\right)\right)$$
33	32	ad2antrr	$$⊢\left(\left(A\subseteq {ℝ}^{*}\wedge x\in ℝ\right)\wedge sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }\right)\to \exists z\in {ℝ}^{*}\left(\forall w\in A\neg z<w\wedge \forall w\in {ℝ}^{*}\left(w<z\to \exists y\in Aw<y\right)\right)$$
34	31 33	suplub	$$⊢\left(\left(A\subseteq {ℝ}^{*}\wedge x\in ℝ\right)\wedge sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }\right)\to \left(\left(x\in {ℝ}^{*}\wedge x<sup\left(A,{ℝ}^{*},<\right)\right)\to \exists y\in Ax<y\right)$$
35	24 29 34	mp2and	$$⊢\left(\left(A\subseteq {ℝ}^{*}\wedge x\in ℝ\right)\wedge sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }\right)\to \exists y\in Ax<y$$
36	35	exp31	$$⊢A\subseteq {ℝ}^{*}\to \left(x\in ℝ\to \left(sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }\to \exists y\in Ax<y\right)\right)$$
37	36	com23	$$⊢A\subseteq {ℝ}^{*}\to \left(sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }\to \left(x\in ℝ\to \exists y\in Ax<y\right)\right)$$
38	37	ralrimdv	$$⊢A\subseteq {ℝ}^{*}\to \left(sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }\to \forall x\in ℝ\exists y\in Ax<y\right)$$
39	22 38	impbid	$$⊢A\subseteq {ℝ}^{*}\to \left(\forall x\in ℝ\exists y\in Ax<y\leftrightarrow sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }\right)$$