Definition df-ioc 13326

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 13322	. 2 class (,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11244	. . 3 class ℝ*
5	2	cv 1541	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1541	. . . . . 6 class 𝑧
8		clt 11245	. . . . . 6 class <
9	5, 7, 8	wbr 5148	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1541	. . . . . 6 class 𝑦
11		cle 11246	. . . . . 6 class ≤
12	7, 10, 11	wbr 5148	. . . . 5 wff 𝑧 ≤ 𝑦
13	9, 12	wa 397	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)
14	13, 6, 4	crab 3433	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7408	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
16	1, 15	wceq 1542	1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is referenced by:  iocval  13358  elioc1  13363  iocssxr  13405  iocssicc  13411  iocssioo  13413  ioounsn  13451  snunioc  13454  leordtval2  22708  iocpnfordt  22711  lecldbas  22715  pnfnei  22716  iocmnfcld  24277  xrtgioo  24314  ismbf3d  25163  dvloglem  26148  asindmre  36560  dvasin  36561  ioossioc  44192  eliocre  44209  lbioc  44213