Definition df-ioc 13377

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 13373	. 2 class (,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11242	. . 3 class ℝ*
5	2	cv 1566	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1566	. . . . . 6 class 𝑧
8		clt 11243	. . . . . 6 class <
9	5, 7, 8	wbr 5111	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1566	. . . . . 6 class 𝑦
11		cle 11244	. . . . . 6 class ≤
12	7, 10, 11	wbr 5111	. . . . 5 wff 𝑧 ≤ 𝑦
13	9, 12	wa 400	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)
14	13, 6, 4	crab 3422	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7413	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
16	1, 15	wceq 1567	1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is referenced by:  iocval  13409  elioc1  13414  iocssxr  13458  iocssicc  13464  iocssioo  13466  ioounsn  13504  snunioc  13507  leordtval2  23338  iocpnfordt  23341  lecldbas  23345  pnfnei  23346  iocmnfcld  24894  xrtgioo  24933  ismbf3d  25782  dvloglem  26779  asindmre  38277  dvasin  38278  iocioodisjd  43006  ioossioc  46135  eliocre  46152  lbioc  46156