Definition df-ioc 12731

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 12727	. 2 class (,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 10663	. . 3 class ℝ*
5	2	cv 1537	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1537	. . . . . 6 class 𝑧
8		clt 10664	. . . . . 6 class <
9	5, 7, 8	wbr 5030	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1537	. . . . . 6 class 𝑦
11		cle 10665	. . . . . 6 class ≤
12	7, 10, 11	wbr 5030	. . . . 5 wff 𝑧 ≤ 𝑦
13	9, 12	wa 399	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)
14	13, 6, 4	crab 3110	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7137	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
16	1, 15	wceq 1538	1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is referenced by:  iocval  12763  elioc1  12768  iocssxr  12809  iocssicc  12815  iocssioo  12817  ioounsn  12855  snunioc  12858  leordtval2  21817  iocpnfordt  21820  lecldbas  21824  pnfnei  21825  iocmnfcld  23374  xrtgioo  23411  ismbf3d  24258  dvloglem  25239  asindmre  35140  dvasin  35141  ioossioc  42129  eliocre  42146  lbioc  42150