Definition df-ico 13265

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

This definition is referenced by:  icoval  13297  elico1  13302  elicore  13312  icossico  13330  iccssico  13332  iccssico2  13334  icossxr  13346  icossicc  13350  ioossico  13352  icossioo  13354  icoun  13389  snunioo  13392  snunico  13393  ioojoin  13397  icopnfsup  13783  limsupgord  15393  leordtval2  23154  icomnfordt  23158  lecldbas  23161  mnfnei  23163  icopnfcld  24709  xrtgioo  24749  ioombl  25520  dvfsumrlimge0  25991  dvfsumrlim2  25993  psercnlem2  26388  tanord1  26500  rlimcnp  26929  rlimcnp2  26930  dchrisum0lem2a  27482  pntleml  27576  pnt  27579  joiniooico  32803  icorempo  37495  icoreresf  37496  isbasisrelowl  37502  icoreelrn  37505  relowlpssretop  37508  asindmre  37843  icof  45405  snunioo1  45700  elicores  45721  dmico  45751  liminfgord  45940  volicorescl  46739  iccdisj2  49084