Theorem supxrpnf

Description: The supremum of a set of extended reals containing plus infinity is plus infinity. (Contributed by NM, 15-Oct-2005)

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

Proof

Step	Hyp	Ref	Expression
1		ssel	$$⊢A\subseteq {ℝ}^{*}\to \left(y\in A\to y\in {ℝ}^{*}\right)$$
2		pnfnlt	$$⊢y\in {ℝ}^{*}\to \neg \mathrm{+\infty }<y$$
3	1 2	syl6	$$⊢A\subseteq {ℝ}^{*}\to \left(y\in A\to \neg \mathrm{+\infty }<y\right)$$
4	3	ralrimiv	$$⊢A\subseteq {ℝ}^{*}\to \forall y\in A\neg \mathrm{+\infty }<y$$
5		breq2	$$⊢z=\mathrm{+\infty }\to \left(y<z\leftrightarrow y<\mathrm{+\infty }\right)$$
6	5	rspcev	$$⊢\left(\mathrm{+\infty }\in A\wedge y<\mathrm{+\infty }\right)\to \exists z\in Ay<z$$
7	6	ex	$$⊢\mathrm{+\infty }\in A\to \left(y<\mathrm{+\infty }\to \exists z\in Ay<z\right)$$
8	7	ralrimivw	$$⊢\mathrm{+\infty }\in A\to \forall y\in ℝ\left(y<\mathrm{+\infty }\to \exists z\in Ay<z\right)$$
9	4 8	anim12i	$$⊢\left(A\subseteq {ℝ}^{*}\wedge \mathrm{+\infty }\in A\right)\to \left(\forall y\in A\neg \mathrm{+\infty }<y\wedge \forall y\in ℝ\left(y<\mathrm{+\infty }\to \exists z\in Ay<z\right)\right)$$
10		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
11		supxr	$$⊢\left(\left(A\subseteq {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\wedge \left(\forall y\in A\neg \mathrm{+\infty }<y\wedge \forall y\in ℝ\left(y<\mathrm{+\infty }\to \exists z\in Ay<z\right)\right)\right)\to sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }$$
12	10 11	mpanl2	$$⊢\left(A\subseteq {ℝ}^{*}\wedge \left(\forall y\in A\neg \mathrm{+\infty }<y\wedge \forall y\in ℝ\left(y<\mathrm{+\infty }\to \exists z\in Ay<z\right)\right)\right)\to sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }$$
13	9 12	syldan	$$⊢\left(A\subseteq {ℝ}^{*}\wedge \mathrm{+\infty }\in A\right)\to sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }$$