Theorem rpsup

Description: The positive reals are unbounded above. (Contributed by Mario Carneiro, 7-May-2016)

	Ref	Expression
Assertion	rpsup	$$⊢sup\left({ℝ}^{+},{ℝ}^{*},<\right)=\mathrm{+\infty }$$

Proof

Step	Hyp	Ref	Expression
1		ioorp	$$⊢\left(0,\mathrm{+\infty }\right)={ℝ}^{+}$$
2	1	supeq1i	$$⊢sup\left(\left(0,\mathrm{+\infty }\right),{ℝ}^{*},<\right)=sup\left({ℝ}^{+},{ℝ}^{*},<\right)$$
3		0xr	$$⊢0\in {ℝ}^{*}$$
4		0re	$$⊢0\in ℝ$$
5		renepnf	$$⊢0\in ℝ\to 0\ne \mathrm{+\infty }$$
6	4 5	ax-mp	$$⊢0\ne \mathrm{+\infty }$$
7		ioopnfsup	$$⊢\left(0\in {ℝ}^{*}\wedge 0\ne \mathrm{+\infty }\right)\to sup\left(\left(0,\mathrm{+\infty }\right),{ℝ}^{*},<\right)=\mathrm{+\infty }$$
8	3 6 7	mp2an	$$⊢sup\left(\left(0,\mathrm{+\infty }\right),{ℝ}^{*},<\right)=\mathrm{+\infty }$$
9	2 8	eqtr3i	$$⊢sup\left({ℝ}^{+},{ℝ}^{*},<\right)=\mathrm{+\infty }$$