Definition df-ico 12181

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 12177	. 2 class [,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 10073	. . 3 class ℝ*
5	2	cv 1482	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1482	. . . . . 6 class 𝑧
8		cle 10075	. . . . . 6 class ≤
9	5, 7, 8	wbr 4653	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1482	. . . . . 6 class 𝑦
11		clt 10074	. . . . . 6 class <
12	7, 10, 11	wbr 4653	. . . . 5 wff 𝑧 < 𝑦
13	9, 12	wa 384	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)
14	13, 6, 4	crab 2916	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}
15	2, 3, 4, 4, 14	cmpt2 6652	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
16	1, 15	wceq 1483	1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  icoval  12213  elico1  12218  elicore  12226  icossico  12243  iccssico  12245  iccssico2  12247  icossxr  12258  icossicc  12260  ioossico  12262  icossioo  12264  icoun  12296  snunioo  12298  snunico  12299  ioojoin  12303  icopnfsup  12664  limsupgord  14203  leordtval2  21016  icomnfordt  21020  lecldbas  21023  mnfnei  21025  icopnfcld  22571  xrtgioo  22609  ioombl  23333  dvfsumrlimge0  23793  dvfsumrlim2  23795  psercnlem2  24178  tanord1  24283  rlimcnp  24692  rlimcnp2  24693  dchrisum0lem2a  25206  pntleml  25300  pnt  25303  joiniooico  29536  icorempt2  33199  icoreresf  33200  isbasisrelowl  33206  icoreelrn  33209  relowlpssretop  33212  asindmre  33495  icof  39411  snunioo1  39738  elicores  39760  dmico  39792  liminfgord  39986  volicorescl  40767