Definition df-ico 13377

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 13373	. 2 class [,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11241	. . 3 class ℝ*
5	2	cv 1566	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1566	. . . . . 6 class 𝑧
8		cle 11243	. . . . . 6 class ≤
9	5, 7, 8	wbr 5113	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1566	. . . . . 6 class 𝑦
11		clt 11242	. . . . . 6 class <
12	7, 10, 11	wbr 5113	. . . . 5 wff 𝑧 < 𝑦
13	9, 12	wa 400	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)
14	13, 6, 4	crab 3423	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7413	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
16	1, 15	wceq 1567	1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  icoval  13409  elico1  13414  elicore  13424  icossico  13442  iccssico  13444  iccssico2  13446  icossxr  13458  icossicc  13462  ioossico  13464  icossioo  13466  icoun  13501  snunioo  13504  snunico  13505  ioojoin  13509  icopnfsup  13897  limsupgord  15522  leordtval2  23337  icomnfordt  23341  lecldbas  23344  mnfnei  23346  icopnfcld  24892  xrtgioo  24932  ioombl  25692  dvfsumrlimge0  26157  dvfsumrlim2  26159  psercnlem2  26552  tanord1  26667  rlimcnp  27095  rlimcnp2  27096  dchrisum0lem2a  27646  pntleml  27740  pnt  27743  joiniooico  33059  icorempo  37884  icoreresf  37885  isbasisrelowl  37891  icoreelrn  37894  relowlpssretop  37897  asindmre  38241  icof  45826  snunioo1  46119  elicores  46140  dmico  46170  liminfgord  46359  volicorescl  47158  iccdisj2  49559