# Metamath Proof Explorer

## 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\}↔\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\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)=ℝ$