Definition df-ioc 13270

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 13266	. 2 class (,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11169	. . 3 class ℝ*
5	2	cv 1541	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1541	. . . . . 6 class 𝑧
8		clt 11170	. . . . . 6 class <
9	5, 7, 8	wbr 5099	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1541	. . . . . 6 class 𝑦
11		cle 11171	. . . . . 6 class ≤
12	7, 10, 11	wbr 5099	. . . . 5 wff 𝑧 ≤ 𝑦
13	9, 12	wa 395	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)
14	13, 6, 4	crab 3400	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7362	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
16	1, 15	wceq 1542	1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is referenced by:  iocval  13302  elioc1  13307  iocssxr  13351  iocssicc  13357  iocssioo  13359  ioounsn  13397  snunioc  13400  leordtval2  23160  iocpnfordt  23163  lecldbas  23167  pnfnei  23168  iocmnfcld  24716  xrtgioo  24755  ismbf3d  25615  dvloglem  26617  asindmre  37875  dvasin  37876  iocioodisjd  42611  ioossioc  45774  eliocre  45791  lbioc  45795