Definition df-ico 12745

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 12741	. 2 class [,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 10674	. . 3 class ℝ*
5	2	cv 1536	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1536	. . . . . 6 class 𝑧
8		cle 10676	. . . . . 6 class ≤
9	5, 7, 8	wbr 5066	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1536	. . . . . 6 class 𝑦
11		clt 10675	. . . . . 6 class <
12	7, 10, 11	wbr 5066	. . . . 5 wff 𝑧 < 𝑦
13	9, 12	wa 398	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)
14	13, 6, 4	crab 3142	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7158	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
16	1, 15	wceq 1537	1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  icoval  12777  elico1  12782  elicore  12790  icossico  12807  iccssico  12809  iccssico2  12811  icossxr  12822  icossicc  12825  ioossico  12827  icossioo  12829  icoun  12862  snunioo  12865  snunico  12866  ioojoin  12870  icopnfsup  13234  limsupgord  14829  leordtval2  21820  icomnfordt  21824  lecldbas  21827  mnfnei  21829  icopnfcld  23376  xrtgioo  23414  ioombl  24166  dvfsumrlimge0  24627  dvfsumrlim2  24629  psercnlem2  25012  tanord1  25121  rlimcnp  25543  rlimcnp2  25544  dchrisum0lem2a  26093  pntleml  26187  pnt  26190  joiniooico  30497  icorempo  34635  icoreresf  34636  isbasisrelowl  34642  icoreelrn  34645  relowlpssretop  34648  asindmre  34992  icof  41531  snunioo1  41837  elicores  41858  dmico  41890  liminfgord  42084  volicorescl  42884