Definition df-ico 13413

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 13409	. 2 class [,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11323	. . 3 class ℝ*
5	2	cv 1536	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1536	. . . . . 6 class 𝑧
8		cle 11325	. . . . . 6 class ≤
9	5, 7, 8	wbr 5166	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1536	. . . . . 6 class 𝑦
11		clt 11324	. . . . . 6 class <
12	7, 10, 11	wbr 5166	. . . . 5 wff 𝑧 < 𝑦
13	9, 12	wa 395	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)
14	13, 6, 4	crab 3443	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7450	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
16	1, 15	wceq 1537	1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  icoval  13445  elico1  13450  elicore  13459  icossico  13477  iccssico  13479  iccssico2  13481  icossxr  13492  icossicc  13496  ioossico  13498  icossioo  13500  icoun  13535  snunioo  13538  snunico  13539  ioojoin  13543  icopnfsup  13916  limsupgord  15518  leordtval2  23241  icomnfordt  23245  lecldbas  23248  mnfnei  23250  icopnfcld  24809  xrtgioo  24847  ioombl  25619  dvfsumrlimge0  26091  dvfsumrlim2  26093  psercnlem2  26486  tanord1  26597  rlimcnp  27026  rlimcnp2  27027  dchrisum0lem2a  27579  pntleml  27673  pnt  27676  joiniooico  32779  icorempo  37317  icoreresf  37318  isbasisrelowl  37324  icoreelrn  37327  relowlpssretop  37330  asindmre  37663  icof  45126  snunioo1  45430  elicores  45451  dmico  45483  liminfgord  45675  volicorescl  46474  iccdisj2  48577