# Metamath Proof Explorer

## Theorem ioof

Description: The set of open intervals of extended reals maps to subsets of reals. (Contributed by NM, 7-Feb-2007) (Revised by Mario Carneiro, 16-Nov-2013)

Ref Expression
Assertion ioof ${⊢}\left(.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫ℝ$

### Proof

Step Hyp Ref Expression
1 iooval ${⊢}\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\to \left({x},{y}\right)=\left\{{z}\in {ℝ}^{*}|\left({x}<{z}\wedge {z}<{y}\right)\right\}$
2 ioossre ${⊢}\left({x},{y}\right)\subseteq ℝ$
3 ovex ${⊢}\left({x},{y}\right)\in \mathrm{V}$
4 3 elpw ${⊢}\left({x},{y}\right)\in 𝒫ℝ↔\left({x},{y}\right)\subseteq ℝ$
5 2 4 mpbir ${⊢}\left({x},{y}\right)\in 𝒫ℝ$
6 1 5 eqeltrrdi ${⊢}\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\to \left\{{z}\in {ℝ}^{*}|\left({x}<{z}\wedge {z}<{y}\right)\right\}\in 𝒫ℝ$
7 6 rgen2 ${⊢}\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left\{{z}\in {ℝ}^{*}|\left({x}<{z}\wedge {z}<{y}\right)\right\}\in 𝒫ℝ$
8 df-ioo ${⊢}\left(.\right)=\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}<{z}\wedge {z}<{y}\right)\right\}\right)$
9 8 fmpo ${⊢}\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left\{{z}\in {ℝ}^{*}|\left({x}<{z}\wedge {z}<{y}\right)\right\}\in 𝒫ℝ↔\left(.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫ℝ$
10 7 9 mpbi ${⊢}\left(.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫ℝ$