Definition df-ioc 13508

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 13504	. 2 class (,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11369	. . 3 class ℝ*
5	2	cv 1569	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1569	. . . . . 6 class 𝑧
8		clt 11370	. . . . . 6 class <
9	5, 7, 8	wbr 5106	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1569	. . . . . 6 class 𝑦
11		cle 11371	. . . . . 6 class ≤
12	7, 10, 11	wbr 5106	. . . . 5 wff 𝑧 ≤ 𝑦
13	9, 12	wa 401	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)
14	13, 6, 4	crab 3416	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7445	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
16	1, 15	wceq 1570	1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is used by:  iocval  13540  elioc1  13545  iocssxr  13589  iocssicc  13595  iocssioo  13597  ioounsn  13635  snunioc  13638  leordtval2  23560  iocpnfordt  23563  lecldbas  23567  pnfnei  23568  iocmnfcld  25117  xrtgioo  25156  ismbf3d  26005  dvloglem  27006  asindmre  38813  dvasin  38814  iocioodisjd  43570  ioossioc  46709  eliocre  46726  lbioc  46730