Definition df-ioc 12744

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 12740	. 2 class (,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 10674	. . 3 class ℝ*
5	2	cv 1536	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1536	. . . . . 6 class 𝑧
8		clt 10675	. . . . . 6 class <
9	5, 7, 8	wbr 5066	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1536	. . . . . 6 class 𝑦
11		cle 10676	. . . . . 6 class ≤
12	7, 10, 11	wbr 5066	. . . . 5 wff 𝑧 ≤ 𝑦
13	9, 12	wa 398	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)
14	13, 6, 4	crab 3142	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7158	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
16	1, 15	wceq 1537	1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is referenced by:  iocval  12776  elioc1  12781  iocssxr  12821  iocssicc  12826  iocssioo  12828  ioounsn  12864  snunioc  12867  leordtval2  21820  iocpnfordt  21823  lecldbas  21827  pnfnei  21828  iocmnfcld  23377  xrtgioo  23414  ismbf3d  24255  dvloglem  25231  asindmre  34992  dvasin  34993  ioossioc  41815  eliocre  41834  lbioc  41838