Definition df-ico 13482

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 13478	. 2 class [,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11342	. . 3 class ℝ*
5	2	cv 1568	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1568	. . . . . 6 class 𝑧
8		cle 11344	. . . . . 6 class ≤
9	5, 7, 8	wbr 5102	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1568	. . . . . 6 class 𝑦
11		clt 11343	. . . . . 6 class <
12	7, 10, 11	wbr 5102	. . . . 5 wff 𝑧 < 𝑦
13	9, 12	wa 401	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)
14	13, 6, 4	crab 3412	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7422	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
16	1, 15	wceq 1569	1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})

This definition is used by:  icoval  13514  elico1  13519  elicore  13529  icossico  13547  iccssico  13549  iccssico2  13551  icossxr  13563  icossicc  13567  ioossico  13569  icossioo  13571  icoun  13606  snunioo  13609  snunico  13610  ioojoin  13614  icopnfsup  14005  limsupgord  15639  leordtval2  23530  icomnfordt  23534  lecldbas  23537  mnfnei  23539  icopnfcld  25086  xrtgioo  25126  ioombl  25886  dvfsumrlimge0  26350  dvfsumrlim2  26352  psercnlem2  26751  tanord1  26865  rlimcnp  27293  rlimcnp2  27294  dchrisum0lem2a  27844  pntleml  27938  pnt  27941  joiniooico  33366  icorempo  38275  icoreresf  38276  isbasisrelowl  38282  icoreelrn  38285  relowlpssretop  38288  asindmre  38622  icof  46232  snunioo1  46524  elicores  46545  dmico  46575  liminfgord  46764  volicorescl  47563  iccdisj2  50005