Theorem resup

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

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

Proof

Step	Hyp	Ref	Expression
1		ioomax	$$⊢\left(\mathrm{-\infty },\mathrm{+\infty }\right)=ℝ$$
2	1	supeq1i	$$⊢sup\left(\left(\mathrm{-\infty },\mathrm{+\infty }\right),{ℝ}^{*},<\right)=sup\left(ℝ,{ℝ}^{*},<\right)$$
3		mnfxr	$$⊢\mathrm{-\infty }\in {ℝ}^{*}$$
4		mnfnepnf	$$⊢\mathrm{-\infty }\ne \mathrm{+\infty }$$
5		ioopnfsup	$$⊢\left(\mathrm{-\infty }\in {ℝ}^{*}\wedge \mathrm{-\infty }\ne \mathrm{+\infty }\right)\to sup\left(\left(\mathrm{-\infty },\mathrm{+\infty }\right),{ℝ}^{*},<\right)=\mathrm{+\infty }$$
6	3 4 5	mp2an	$$⊢sup\left(\left(\mathrm{-\infty },\mathrm{+\infty }\right),{ℝ}^{*},<\right)=\mathrm{+\infty }$$
7	2 6	eqtr3i	$$⊢sup\left(ℝ,{ℝ}^{*},<\right)=\mathrm{+\infty }$$