Definition df-ico 13393

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 13389	. 2 class [,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11294	. . 3 class ℝ*
5	2	cv 1539	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1539	. . . . . 6 class 𝑧
8		cle 11296	. . . . . 6 class ≤
9	5, 7, 8	wbr 5143	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1539	. . . . . 6 class 𝑦
11		clt 11295	. . . . . 6 class <
12	7, 10, 11	wbr 5143	. . . . 5 wff 𝑧 < 𝑦
13	9, 12	wa 395	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)
14	13, 6, 4	crab 3436	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7433	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
16	1, 15	wceq 1540	1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  icoval  13425  elico1  13430  elicore  13439  icossico  13457  iccssico  13459  iccssico2  13461  icossxr  13472  icossicc  13476  ioossico  13478  icossioo  13480  icoun  13515  snunioo  13518  snunico  13519  ioojoin  13523  icopnfsup  13905  limsupgord  15508  leordtval2  23220  icomnfordt  23224  lecldbas  23227  mnfnei  23229  icopnfcld  24788  xrtgioo  24828  ioombl  25600  dvfsumrlimge0  26071  dvfsumrlim2  26073  psercnlem2  26468  tanord1  26579  rlimcnp  27008  rlimcnp2  27009  dchrisum0lem2a  27561  pntleml  27655  pnt  27658  joiniooico  32776  icorempo  37352  icoreresf  37353  isbasisrelowl  37359  icoreelrn  37362  relowlpssretop  37365  asindmre  37710  icof  45224  snunioo1  45525  elicores  45546  dmico  45578  liminfgord  45769  volicorescl  46568  iccdisj2  48795