Definition df-ioc 13481

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 13477	. 2 class (,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11342	. . 3 class ℝ*
5	2	cv 1568	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1568	. . . . . 6 class 𝑧
8		clt 11343	. . . . . 6 class <
9	5, 7, 8	wbr 5102	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1568	. . . . . 6 class 𝑦
11		cle 11344	. . . . . 6 class ≤
12	7, 10, 11	wbr 5102	. . . . 5 wff 𝑧 ≤ 𝑦
13	9, 12	wa 401	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)
14	13, 6, 4	crab 3412	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7422	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
16	1, 15	wceq 1569	1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is used by:  iocval  13513  elioc1  13518  iocssxr  13562  iocssicc  13568  iocssioo  13570  ioounsn  13608  snunioc  13611  leordtval2  23530  iocpnfordt  23533  lecldbas  23537  pnfnei  23538  iocmnfcld  25087  xrtgioo  25126  ismbf3d  25975  dvloglem  26976  asindmre  38664  dvasin  38665  iocioodisjd  43420  ioossioc  46547  eliocre  46564  lbioc  46568