Definition df-ico 13246

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 13242	. 2 class [,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11140	. . 3 class ℝ*
5	2	cv 1540	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1540	. . . . . 6 class 𝑧
8		cle 11142	. . . . . 6 class ≤
9	5, 7, 8	wbr 5086	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1540	. . . . . 6 class 𝑦
11		clt 11141	. . . . . 6 class <
12	7, 10, 11	wbr 5086	. . . . 5 wff 𝑧 < 𝑦
13	9, 12	wa 395	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)
14	13, 6, 4	crab 3395	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7343	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
16	1, 15	wceq 1541	1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  icoval  13278  elico1  13283  elicore  13293  icossico  13311  iccssico  13313  iccssico2  13315  icossxr  13327  icossicc  13331  ioossico  13333  icossioo  13335  icoun  13370  snunioo  13373  snunico  13374  ioojoin  13378  icopnfsup  13764  limsupgord  15374  leordtval2  23122  icomnfordt  23126  lecldbas  23129  mnfnei  23131  icopnfcld  24677  xrtgioo  24717  ioombl  25488  dvfsumrlimge0  25959  dvfsumrlim2  25961  psercnlem2  26356  tanord1  26468  rlimcnp  26897  rlimcnp2  26898  dchrisum0lem2a  27450  pntleml  27544  pnt  27547  joiniooico  32749  icorempo  37385  icoreresf  37386  isbasisrelowl  37392  icoreelrn  37395  relowlpssretop  37398  asindmre  37743  icof  45256  snunioo1  45552  elicores  45573  dmico  45603  liminfgord  45792  volicorescl  46591  iccdisj2  48928