Definition df-ioc 12218

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 12214	. 2 class (,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 10111	. . 3 class ℝ*
5	2	cv 1522	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1522	. . . . . 6 class 𝑧
8		clt 10112	. . . . . 6 class <
9	5, 7, 8	wbr 4685	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1522	. . . . . 6 class 𝑦
11		cle 10113	. . . . . 6 class ≤
12	7, 10, 11	wbr 4685	. . . . 5 wff 𝑧 ≤ 𝑦
13	9, 12	wa 383	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)
14	13, 6, 4	crab 2945	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}
15	2, 3, 4, 4, 14	cmpt2 6692	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
16	1, 15	wceq 1523	1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is referenced by:  iocval  12250  elioc1  12255  iocssxr  12295  iocssicc  12299  iocssioo  12301  snunioc  12338  leordtval2  21064  iocpnfordt  21067  lecldbas  21071  pnfnei  21072  iocmnfcld  22619  xrtgioo  22656  ismbf3d  23466  dvloglem  24439  asindmre  33625  dvasin  33626  ioounsn  38112  ioossioc  40031  snunioo2  40049  eliocre  40052  lbioc  40057