Definition df-ioc 13333

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

Assertion

Ref	Expression
df-ioc	⊢ (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})

Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-ioc

Step	Hyp	Ref	Expression
1		cioc 13329	. 2 class (,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11251	. . 3 class ℝ*
5	2	cv 1540	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1540	. . . . . 6 class 𝑧
8		clt 11252	. . . . . 6 class <
9	5, 7, 8	wbr 5148	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1540	. . . . . 6 class 𝑦
11		cle 11253	. . . . . 6 class ≤
12	7, 10, 11	wbr 5148	. . . . 5 wff 𝑧 ≤ 𝑦
13	9, 12	wa 396	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)
14	13, 6, 4	crab 3432	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7413	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
16	1, 15	wceq 1541	1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is referenced by:  iocval  13365  elioc1  13370  iocssxr  13412  iocssicc  13418  iocssioo  13420  ioounsn  13458  snunioc  13461  leordtval2  22936  iocpnfordt  22939  lecldbas  22943  pnfnei  22944  iocmnfcld  24505  xrtgioo  24542  ismbf3d  25395  dvloglem  26380  asindmre  36874  dvasin  36875  ioossioc  44504  eliocre  44521  lbioc  44525