Definition df-ico 13288

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 13284	. 2 class [,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11183	. . 3 class ℝ*
5	2	cv 1539	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1539	. . . . . 6 class 𝑧
8		cle 11185	. . . . . 6 class ≤
9	5, 7, 8	wbr 5102	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1539	. . . . . 6 class 𝑦
11		clt 11184	. . . . . 6 class <
12	7, 10, 11	wbr 5102	. . . . 5 wff 𝑧 < 𝑦
13	9, 12	wa 395	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)
14	13, 6, 4	crab 3402	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7371	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
16	1, 15	wceq 1540	1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  icoval  13320  elico1  13325  elicore  13335  icossico  13353  iccssico  13355  iccssico2  13357  icossxr  13369  icossicc  13373  ioossico  13375  icossioo  13377  icoun  13412  snunioo  13415  snunico  13416  ioojoin  13420  icopnfsup  13803  limsupgord  15414  leordtval2  23075  icomnfordt  23079  lecldbas  23082  mnfnei  23084  icopnfcld  24631  xrtgioo  24671  ioombl  25442  dvfsumrlimge0  25913  dvfsumrlim2  25915  psercnlem2  26310  tanord1  26422  rlimcnp  26851  rlimcnp2  26852  dchrisum0lem2a  27404  pntleml  27498  pnt  27501  joiniooico  32670  icorempo  37312  icoreresf  37313  isbasisrelowl  37319  icoreelrn  37322  relowlpssretop  37325  asindmre  37670  icof  45186  snunioo1  45483  elicores  45504  dmico  45534  liminfgord  45725  volicorescl  46524  iccdisj2  48858