Definition df-ico 13281

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

This definition is referenced by:  icoval  13313  elico1  13318  elicore  13328  icossico  13346  iccssico  13348  iccssico2  13350  icossxr  13362  icossicc  13366  ioossico  13368  icossioo  13370  icoun  13405  snunioo  13408  snunico  13409  ioojoin  13413  icopnfsup  13799  limsupgord  15409  leordtval2  23173  icomnfordt  23177  lecldbas  23180  mnfnei  23182  icopnfcld  24728  xrtgioo  24768  ioombl  25539  dvfsumrlimge0  26010  dvfsumrlim2  26012  psercnlem2  26407  tanord1  26519  rlimcnp  26948  rlimcnp2  26949  dchrisum0lem2a  27501  pntleml  27595  pnt  27598  joiniooico  32871  icorempo  37633  icoreresf  37634  isbasisrelowl  37640  icoreelrn  37643  relowlpssretop  37646  asindmre  37983  icof  45606  snunioo1  45901  elicores  45922  dmico  45952  liminfgord  46141  volicorescl  46940  iccdisj2  49285