Definition df-ico 13506

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 13502	. 2 class [,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11366	. . 3 class ℝ*
5	2	cv 1569	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1569	. . . . . 6 class 𝑧
8		cle 11368	. . . . . 6 class ≤
9	5, 7, 8	wbr 5106	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1569	. . . . . 6 class 𝑦
11		clt 11367	. . . . . 6 class <
12	7, 10, 11	wbr 5106	. . . . 5 wff 𝑧 < 𝑦
13	9, 12	wa 401	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)
14	13, 6, 4	crab 3416	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7442	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
16	1, 15	wceq 1570	1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})

This definition is used by:  icoval  13538  elico1  13543  elicore  13553  icossico  13571  iccssico  13573  iccssico2  13575  icossxr  13587  icossicc  13591  ioossico  13593  icossioo  13595  icoun  13630  snunioo  13633  snunico  13634  ioojoin  13638  icopnfsup  14029  limsupgord  15665  leordtval2  23557  icomnfordt  23561  lecldbas  23564  mnfnei  23566  icopnfcld  25113  xrtgioo  25153  ioombl  25913  dvfsumrlimge0  26377  dvfsumrlim2  26379  psercnlem2  26778  tanord1  26892  rlimcnp  27320  rlimcnp2  27321  dchrisum0lem2a  27871  pntleml  27965  pnt  27968  joiniooico  33433  icorempo  38465  icoreresf  38466  isbasisrelowl  38472  icoreelrn  38475  relowlpssretop  38478  asindmre  38812  icof  46435  snunioo1  46727  elicores  46748  dmico  46778  liminfgord  46967  volicorescl  47766  iccdisj2  50214