Definition df-ico 12732

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 12728	. 2 class [,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 10663	. . 3 class ℝ*
5	2	cv 1537	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1537	. . . . . 6 class 𝑧
8		cle 10665	. . . . . 6 class ≤
9	5, 7, 8	wbr 5030	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1537	. . . . . 6 class 𝑦
11		clt 10664	. . . . . 6 class <
12	7, 10, 11	wbr 5030	. . . . 5 wff 𝑧 < 𝑦
13	9, 12	wa 399	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)
14	13, 6, 4	crab 3110	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7137	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
16	1, 15	wceq 1538	1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  icoval  12764  elico1  12769  elicore  12777  icossico  12795  iccssico  12797  iccssico2  12799  icossxr  12810  icossicc  12814  ioossico  12816  icossioo  12818  icoun  12853  snunioo  12856  snunico  12857  ioojoin  12861  icopnfsup  13228  limsupgord  14821  leordtval2  21817  icomnfordt  21821  lecldbas  21824  mnfnei  21826  icopnfcld  23373  xrtgioo  23411  ioombl  24169  dvfsumrlimge0  24633  dvfsumrlim2  24635  psercnlem2  25019  tanord1  25129  rlimcnp  25551  rlimcnp2  25552  dchrisum0lem2a  26101  pntleml  26195  pnt  26198  joiniooico  30523  icorempo  34768  icoreresf  34769  isbasisrelowl  34775  icoreelrn  34778  relowlpssretop  34781  asindmre  35140  icof  41848  snunioo1  42149  elicores  42170  dmico  42202  liminfgord  42396  volicorescl  43192