Definition df-ico 13399

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

This definition is used by:  icoval  13431  elico1  13436  elicore  13446  icossico  13464  iccssico  13466  iccssico2  13468  icossxr  13480  icossicc  13484  ioossico  13486  icossioo  13488  icoun  13523  snunioo  13526  snunico  13527  ioojoin  13531  icopnfsup  13921  limsupgord  15552  leordtval2  23424  icomnfordt  23428  lecldbas  23431  mnfnei  23433  icopnfcld  24980  xrtgioo  25020  ioombl  25780  dvfsumrlimge0  26245  dvfsumrlim2  26247  psercnlem2  26643  tanord1  26758  rlimcnp  27186  rlimcnp2  27187  dchrisum0lem2a  27737  pntleml  27831  pnt  27834  joiniooico  33194  icorempo  38059  icoreresf  38060  isbasisrelowl  38066  icoreelrn  38069  relowlpssretop  38072  asindmre  38416  icof  46013  snunioo1  46306  elicores  46327  dmico  46357  liminfgord  46546  volicorescl  47345  iccdisj2  49752