Metamath Proof Explorer

Definition df-ioc

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

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cioc ${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 cle ${class}\le$
10 3 cv ${setvar}{y}$
11 7 10 9 wbr ${wff}{z}\le {y}$
12 8 11 wa ${wff}\left({x}<{z}\wedge {z}\le {y}\right)$
13 12 4 2 crab ${class}\left\{{z}\in {ℝ}^{*}|\left({x}<{z}\wedge {z}\le {y}\right)\right\}$
14 1 3 2 2 13 cmpo ${class}\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}<{z}\wedge {z}\le {y}\right)\right\}\right)$
15 0 14 wceq ${wff}\left(.\right]=\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}<{z}\wedge {z}\le {y}\right)\right\}\right)$