Definition df-ico 13382

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 13378	. 2 class [,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11246	. . 3 class ℝ*
5	2	cv 1569	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1569	. . . . . 6 class 𝑧
8		cle 11248	. . . . . 6 class ≤
9	5, 7, 8	wbr 5109	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1569	. . . . . 6 class 𝑦
11		clt 11247	. . . . . 6 class <
12	7, 10, 11	wbr 5109	. . . . 5 wff 𝑧 < 𝑦
13	9, 12	wa 400	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)
14	13, 6, 4	crab 3416	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7412	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
16	1, 15	wceq 1570	1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})

This definition is used by:  icoval  13414  elico1  13419  elicore  13429  icossico  13447  iccssico  13449  iccssico2  13451  icossxr  13463  icossicc  13467  ioossico  13469  icossioo  13471  icoun  13506  snunioo  13509  snunico  13510  ioojoin  13514  icopnfsup  13903  limsupgord  15528  leordtval2  23378  icomnfordt  23382  lecldbas  23385  mnfnei  23387  icopnfcld  24933  xrtgioo  24973  ioombl  25733  dvfsumrlimge0  26198  dvfsumrlim2  26200  psercnlem2  26596  tanord1  26711  rlimcnp  27139  rlimcnp2  27140  dchrisum0lem2a  27690  pntleml  27784  pnt  27787  joiniooico  33128  icorempo  38025  icoreresf  38026  isbasisrelowl  38032  icoreelrn  38035  relowlpssretop  38038  asindmre  38382  icof  45963  snunioo1  46256  elicores  46277  dmico  46307  liminfgord  46496  volicorescl  47295  iccdisj2  49703