Definition df-ioc 13256

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 13252	. 2 class (,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11151	. . 3 class ℝ*
5	2	cv 1540	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1540	. . . . . 6 class 𝑧
8		clt 11152	. . . . . 6 class <
9	5, 7, 8	wbr 5093	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1540	. . . . . 6 class 𝑦
11		cle 11153	. . . . . 6 class ≤
12	7, 10, 11	wbr 5093	. . . . 5 wff 𝑧 ≤ 𝑦
13	9, 12	wa 395	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)
14	13, 6, 4	crab 3395	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7354	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
16	1, 15	wceq 1541	1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is referenced by:  iocval  13288  elioc1  13293  iocssxr  13337  iocssicc  13343  iocssioo  13345  ioounsn  13383  snunioc  13386  leordtval2  23133  iocpnfordt  23136  lecldbas  23140  pnfnei  23141  iocmnfcld  24689  xrtgioo  24728  ismbf3d  25588  dvloglem  26590  asindmre  37749  dvasin  37750  iocioodisjd  42419  ioossioc  45597  eliocre  45614  lbioc  45618