Definition df-ioc 13383

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 13379	. 2 class (,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11248	. . 3 class ℝ*
5	2	cv 1568	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1568	. . . . . 6 class 𝑧
8		clt 11249	. . . . . 6 class <
9	5, 7, 8	wbr 5108	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1568	. . . . . 6 class 𝑦
11		cle 11250	. . . . . 6 class ≤
12	7, 10, 11	wbr 5108	. . . . 5 wff 𝑧 ≤ 𝑦
13	9, 12	wa 400	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)
14	13, 6, 4	crab 3415	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7414	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
16	1, 15	wceq 1569	1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is used by:  iocval  13415  elioc1  13420  iocssxr  13464  iocssicc  13470  iocssioo  13472  ioounsn  13510  snunioc  13513  leordtval2  23380  iocpnfordt  23383  lecldbas  23387  pnfnei  23388  iocmnfcld  24936  xrtgioo  24975  ismbf3d  25824  dvloglem  26824  asindmre  38382  dvasin  38383  iocioodisjd  43109  ioossioc  46236  eliocre  46253  lbioc  46257