Definition df-ioc 13361

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 13357	. 2 class (,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11277	. . 3 class ℝ*
5	2	cv 1532	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1532	. . . . . 6 class 𝑧
8		clt 11278	. . . . . 6 class <
9	5, 7, 8	wbr 5148	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1532	. . . . . 6 class 𝑦
11		cle 11279	. . . . . 6 class ≤
12	7, 10, 11	wbr 5148	. . . . 5 wff 𝑧 ≤ 𝑦
13	9, 12	wa 394	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)
14	13, 6, 4	crab 3419	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7419	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
16	1, 15	wceq 1533	1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is referenced by:  iocval  13393  elioc1  13398  iocssxr  13440  iocssicc  13446  iocssioo  13448  ioounsn  13486  snunioc  13489  leordtval2  23146  iocpnfordt  23149  lecldbas  23153  pnfnei  23154  iocmnfcld  24715  xrtgioo  24752  ismbf3d  25613  dvloglem  26612  asindmre  37246  dvasin  37247  ioossioc  44940  eliocre  44957  lbioc  44961