Definition df-ioc 13340

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 13336	. 2 class (,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11201	. . 3 class ℝ*
5	2	cv 1549	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1549	. . . . . 6 class 𝑧
8		clt 11202	. . . . . 6 class <
9	5, 7, 8	wbr 5090	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1549	. . . . . 6 class 𝑦
11		cle 11203	. . . . . 6 class ≤
12	7, 10, 11	wbr 5090	. . . . 5 wff 𝑧 ≤ 𝑦
13	9, 12	wa 398	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)
14	13, 6, 4	crab 3404	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7383	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
16	1, 15	wceq 1550	1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is referenced by:  iocval  13372  elioc1  13377  iocssxr  13421  iocssicc  13427  iocssioo  13429  ioounsn  13467  snunioc  13470  leordtval2  23241  iocpnfordt  23244  lecldbas  23248  pnfnei  23249  iocmnfcld  24797  xrtgioo  24836  ismbf3d  25685  dvloglem  26679  asindmre  38140  dvasin  38141  iocioodisjd  42867  ioossioc  46006  eliocre  46023  lbioc  46027