Definition df-ioc 13450

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 13446	. 2 class (,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11313	. . 3 class ℝ*
5	2	cv 1569	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1569	. . . . . 6 class 𝑧
8		clt 11314	. . . . . 6 class <
9	5, 7, 8	wbr 5102	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1569	. . . . . 6 class 𝑦
11		cle 11315	. . . . . 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 7410	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
16	1, 15	wceq 1570	1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is used by:  iocval  13482  elioc1  13487  iocssxr  13531  iocssicc  13537  iocssioo  13539  ioounsn  13577  snunioc  13580  leordtval2  23491  iocpnfordt  23494  lecldbas  23498  pnfnei  23499  iocmnfcld  25048  xrtgioo  25087  ismbf3d  25936  dvloglem  26939  asindmre  38541  dvasin  38542  iocioodisjd  43299  ioossioc  46426  eliocre  46443  lbioc  46447