Definition df-ioc 13383

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

This definition is referenced by:  iocval  13415  elioc1  13420  iocssxr  13462  iocssicc  13468  iocssioo  13470  ioounsn  13508  snunioc  13511  leordtval2  23207  iocpnfordt  23210  lecldbas  23214  pnfnei  23215  iocmnfcld  24776  xrtgioo  24813  ismbf3d  25674  dvloglem  26675  asindmre  37404  dvasin  37405  ioossioc  45110  eliocre  45127  lbioc  45131