Definition df-ioc 12392

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 12388	. 2 class (,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 10352	. . 3 class ℝ*
5	2	cv 1636	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1636	. . . . . 6 class 𝑧
8		clt 10353	. . . . . 6 class <
9	5, 7, 8	wbr 4837	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1636	. . . . . 6 class 𝑦
11		cle 10354	. . . . . 6 class ≤
12	7, 10, 11	wbr 4837	. . . . 5 wff 𝑧 ≤ 𝑦
13	9, 12	wa 384	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)
14	13, 6, 4	crab 3096	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}
15	2, 3, 4, 4, 14	cmpt2 6870	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
16	1, 15	wceq 1637	1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is referenced by:  iocval  12424  elioc1  12429  iocssxr  12469  iocssicc  12474  iocssioo  12476  ioounsn  12513  ioounsnOLD  12514  snunioc  12517  leordtval2  21224  iocpnfordt  21227  lecldbas  21231  pnfnei  21232  iocmnfcld  22779  xrtgioo  22816  ismbf3d  23629  dvloglem  24602  asindmre  33801  dvasin  33802  ioossioc  40191  eliocre  40210  lbioc  40214