Definition df-ioc 13388

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 13384	. 2 class (,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11291	. . 3 class ℝ*
5	2	cv 1535	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1535	. . . . . 6 class 𝑧
8		clt 11292	. . . . . 6 class <
9	5, 7, 8	wbr 5147	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1535	. . . . . 6 class 𝑦
11		cle 11293	. . . . . 6 class ≤
12	7, 10, 11	wbr 5147	. . . . 5 wff 𝑧 ≤ 𝑦
13	9, 12	wa 395	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)
14	13, 6, 4	crab 3432	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7432	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
16	1, 15	wceq 1536	1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is referenced by:  iocval  13420  elioc1  13425  iocssxr  13467  iocssicc  13473  iocssioo  13475  ioounsn  13513  snunioc  13516  leordtval2  23235  iocpnfordt  23238  lecldbas  23242  pnfnei  23243  iocmnfcld  24804  xrtgioo  24841  ismbf3d  25702  dvloglem  26704  asindmre  37689  dvasin  37690  iocioodisjd  42333  ioossioc  45444  eliocre  45461  lbioc  45465