Definition df-ico 12219

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 12215	. 2 class [,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 10111	. . 3 class ℝ*
5	2	cv 1522	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1522	. . . . . 6 class 𝑧
8		cle 10113	. . . . . 6 class ≤
9	5, 7, 8	wbr 4685	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1522	. . . . . 6 class 𝑦
11		clt 10112	. . . . . 6 class <
12	7, 10, 11	wbr 4685	. . . . 5 wff 𝑧 < 𝑦
13	9, 12	wa 383	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)
14	13, 6, 4	crab 2945	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}
15	2, 3, 4, 4, 14	cmpt2 6692	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
16	1, 15	wceq 1523	1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  icoval  12251  elico1  12256  elicore  12264  icossico  12281  iccssico  12283  iccssico2  12285  icossxr  12296  icossicc  12298  ioossico  12300  icossioo  12302  icoun  12334  snunioo  12336  snunico  12337  ioojoin  12341  icopnfsup  12704  limsupgord  14247  leordtval2  21064  icomnfordt  21068  lecldbas  21071  mnfnei  21073  icopnfcld  22618  xrtgioo  22656  ioombl  23379  dvfsumrlimge0  23838  dvfsumrlim2  23840  psercnlem2  24223  tanord1  24328  rlimcnp  24737  rlimcnp2  24738  dchrisum0lem2a  25251  pntleml  25345  pnt  25348  joiniooico  29664  icorempt2  33329  icoreresf  33330  isbasisrelowl  33336  icoreelrn  33339  relowlpssretop  33342  asindmre  33625  icof  39725  snunioo1  40056  elicores  40078  dmico  40110  liminfgord  40304  volicorescl  41088