Definition df-ico 13378

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 13374	. 2 class [,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11242	. . 3 class ℝ*
5	2	cv 1566	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1566	. . . . . 6 class 𝑧
8		cle 11244	. . . . . 6 class ≤
9	5, 7, 8	wbr 5113	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1566	. . . . . 6 class 𝑦
11		clt 11243	. . . . . 6 class <
12	7, 10, 11	wbr 5113	. . . . 5 wff 𝑧 < 𝑦
13	9, 12	wa 400	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)
14	13, 6, 4	crab 3423	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7413	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
16	1, 15	wceq 1567	1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  icoval  13410  elico1  13415  elicore  13425  icossico  13443  iccssico  13445  iccssico2  13447  icossxr  13459  icossicc  13463  ioossico  13465  icossioo  13467  icoun  13502  snunioo  13505  snunico  13506  ioojoin  13510  icopnfsup  13898  limsupgord  15523  leordtval2  23338  icomnfordt  23342  lecldbas  23345  mnfnei  23347  icopnfcld  24893  xrtgioo  24933  ioombl  25693  dvfsumrlimge0  26158  dvfsumrlim2  26160  psercnlem2  26553  tanord1  26668  rlimcnp  27096  rlimcnp2  27097  dchrisum0lem2a  27647  pntleml  27741  pnt  27744  joiniooico  33060  icorempo  37919  icoreresf  37920  isbasisrelowl  37926  icoreelrn  37929  relowlpssretop  37932  asindmre  38276  icof  45861  snunioo1  46154  elicores  46175  dmico  46205  liminfgord  46394  volicorescl  47193  iccdisj2  49594