Definition df-ico 13271

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

This definition is referenced by:  icoval  13303  elico1  13308  elicore  13318  icossico  13336  iccssico  13338  iccssico2  13340  icossxr  13352  icossicc  13356  ioossico  13358  icossioo  13360  icoun  13395  snunioo  13398  snunico  13399  ioojoin  13403  icopnfsup  13789  limsupgord  15399  leordtval2  23160  icomnfordt  23164  lecldbas  23167  mnfnei  23169  icopnfcld  24715  xrtgioo  24755  ioombl  25526  dvfsumrlimge0  25997  dvfsumrlim2  25999  psercnlem2  26394  tanord1  26506  rlimcnp  26935  rlimcnp2  26936  dchrisum0lem2a  27488  pntleml  27582  pnt  27585  joiniooico  32856  icorempo  37558  icoreresf  37559  isbasisrelowl  37565  icoreelrn  37568  relowlpssretop  37571  asindmre  37906  icof  45530  snunioo1  45825  elicores  45846  dmico  45876  liminfgord  46065  volicorescl  46864  iccdisj2  49209