Theorem ioomax

Description: The open interval from minus to plus infinity. (Contributed by NM, 6-Feb-2007)

	Ref	Expression
Assertion	ioomax	$$⊢\left(\mathrm{-\infty },\mathrm{+\infty }\right)=ℝ$$

Proof

Step	Hyp	Ref	Expression
1		mnfxr	$$⊢\mathrm{-\infty }\in {ℝ}^{*}$$
2		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
3		iooval2	$$⊢\left(\mathrm{-\infty }\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\to \left(\mathrm{-\infty },\mathrm{+\infty }\right)=\left\{x\in ℝ|\left(\mathrm{-\infty }<x\wedge x<\mathrm{+\infty }\right)\right\}$$
4	1 2 3	mp2an	$$⊢\left(\mathrm{-\infty },\mathrm{+\infty }\right)=\left\{x\in ℝ|\left(\mathrm{-\infty }<x\wedge x<\mathrm{+\infty }\right)\right\}$$
5		rabid2	$$⊢ℝ=\left\{x\in ℝ|\left(\mathrm{-\infty }<x\wedge x<\mathrm{+\infty }\right)\right\}\leftrightarrow \forall x\in ℝ\left(\mathrm{-\infty }<x\wedge x<\mathrm{+\infty }\right)$$
6		mnflt	$$⊢x\in ℝ\to \mathrm{-\infty }<x$$
7		ltpnf	$$⊢x\in ℝ\to x<\mathrm{+\infty }$$
8	6 7	jca	$$⊢x\in ℝ\to \left(\mathrm{-\infty }<x\wedge x<\mathrm{+\infty }\right)$$
9	5 8	mprgbir	$$⊢ℝ=\left\{x\in ℝ|\left(\mathrm{-\infty }<x\wedge x<\mathrm{+\infty }\right)\right\}$$
10	4 9	eqtr4i	$$⊢\left(\mathrm{-\infty },\mathrm{+\infty }\right)=ℝ$$