# Metamath Proof Explorer

## Definition df-ioo

Description: Define the set of open intervals of extended reals. (Contributed by NM, 24-Dec-2006)

Ref Expression
Assertion df-ioo ${⊢}\left(.\right)=\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}<{z}\wedge {z}<{y}\right)\right\}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cioo ${class}\left(.\right)$
1 vx ${setvar}{x}$
2 cxr ${class}{ℝ}^{*}$
3 vy ${setvar}{y}$
4 vz ${setvar}{z}$
5 1 cv ${setvar}{x}$
6 clt ${class}<$
7 4 cv ${setvar}{z}$
8 5 7 6 wbr ${wff}{x}<{z}$
9 3 cv ${setvar}{y}$
10 7 9 6 wbr ${wff}{z}<{y}$
11 8 10 wa ${wff}\left({x}<{z}\wedge {z}<{y}\right)$
12 11 4 2 crab ${class}\left\{{z}\in {ℝ}^{*}|\left({x}<{z}\wedge {z}<{y}\right)\right\}$
13 1 3 2 2 12 cmpo ${class}\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}<{z}\wedge {z}<{y}\right)\right\}\right)$
14 0 13 wceq ${wff}\left(.\right)=\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}<{z}\wedge {z}<{y}\right)\right\}\right)$