Definition df-ico 13304

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 13300	. 2 class [,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11178	. . 3 class ℝ*
5	2	cv 1541	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1541	. . . . . 6 class 𝑧
8		cle 11180	. . . . . 6 class ≤
9	5, 7, 8	wbr 5085	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1541	. . . . . 6 class 𝑦
11		clt 11179	. . . . . 6 class <
12	7, 10, 11	wbr 5085	. . . . 5 wff 𝑧 < 𝑦
13	9, 12	wa 395	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)
14	13, 6, 4	crab 3389	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7369	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
16	1, 15	wceq 1542	1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  icoval  13336  elico1  13341  elicore  13351  icossico  13369  iccssico  13371  iccssico2  13373  icossxr  13385  icossicc  13389  ioossico  13391  icossioo  13393  icoun  13428  snunioo  13431  snunico  13432  ioojoin  13436  icopnfsup  13824  limsupgord  15434  leordtval2  23177  icomnfordt  23181  lecldbas  23184  mnfnei  23186  icopnfcld  24732  xrtgioo  24772  ioombl  25532  dvfsumrlimge0  25997  dvfsumrlim2  25999  psercnlem2  26389  tanord1  26501  rlimcnp  26929  rlimcnp2  26930  dchrisum0lem2a  27480  pntleml  27574  pnt  27577  joiniooico  32847  icorempo  37667  icoreresf  37668  isbasisrelowl  37674  icoreelrn  37677  relowlpssretop  37680  asindmre  38024  icof  45648  snunioo1  45942  elicores  45963  dmico  45993  liminfgord  46182  volicorescl  46981  iccdisj2  49372