Definition df-ioc 13405

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 13401	. 2 class (,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11269	. . 3 class ℝ*
5	2	cv 1569	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1569	. . . . . 6 class 𝑧
8		clt 11270	. . . . . 6 class <
9	5, 7, 8	wbr 5107	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1569	. . . . . 6 class 𝑦
11		cle 11271	. . . . . 6 class ≤
12	7, 10, 11	wbr 5107	. . . . 5 wff 𝑧 ≤ 𝑦
13	9, 12	wa 401	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)
14	13, 6, 4	crab 3414	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7418	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
16	1, 15	wceq 1570	1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is used by:  iocval  13437  elioc1  13442  iocssxr  13486  iocssicc  13492  iocssioo  13494  ioounsn  13532  snunioc  13535  leordtval2  23438  iocpnfordt  23441  lecldbas  23445  pnfnei  23446  iocmnfcld  24995  xrtgioo  25034  ismbf3d  25883  dvloglem  26883  asindmre  38439  dvasin  38440  iocioodisjd  43182  ioossioc  46309  eliocre  46326  lbioc  46330