# Metamath Proof Explorer

## Definition df-ico

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

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

### Detailed syntax breakdown

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