Definition df-ico 13299

Description: Define the set of closed-below, open-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.)

Assertion

Ref	Expression
df-ico	⊢ [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})

Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-ico

Step	Hyp	Ref	Expression
1		cico 13295	. 2 class [,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11173	. . 3 class ℝ*
5	2	cv 1541	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1541	. . . . . 6 class 𝑧
8		cle 11175	. . . . . 6 class ≤
9	5, 7, 8	wbr 5086	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1541	. . . . . 6 class 𝑦
11		clt 11174	. . . . . 6 class <
12	7, 10, 11	wbr 5086	. . . . 5 wff 𝑧 < 𝑦
13	9, 12	wa 395	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)
14	13, 6, 4	crab 3390	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7364	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
16	1, 15	wceq 1542	1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  icoval  13331  elico1  13336  elicore  13346  icossico  13364  iccssico  13366  iccssico2  13368  icossxr  13380  icossicc  13384  ioossico  13386  icossioo  13388  icoun  13423  snunioo  13426  snunico  13427  ioojoin  13431  icopnfsup  13819  limsupgord  15429  leordtval2  23191  icomnfordt  23195  lecldbas  23198  mnfnei  23200  icopnfcld  24746  xrtgioo  24786  ioombl  25546  dvfsumrlimge0  26011  dvfsumrlim2  26013  psercnlem2  26406  tanord1  26518  rlimcnp  26946  rlimcnp2  26947  dchrisum0lem2a  27498  pntleml  27592  pnt  27595  joiniooico  32866  icorempo  37685  icoreresf  37686  isbasisrelowl  37692  icoreelrn  37695  relowlpssretop  37698  asindmre  38042  icof  45670  snunioo1  45964  elicores  45985  dmico  46015  liminfgord  46204  volicorescl  47003  iccdisj2  49388