Definition df-ico 13312

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 13308	. 2 class [,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11207	. . 3 class ℝ*
5	2	cv 1539	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1539	. . . . . 6 class 𝑧
8		cle 11209	. . . . . 6 class ≤
9	5, 7, 8	wbr 5107	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1539	. . . . . 6 class 𝑦
11		clt 11208	. . . . . 6 class <
12	7, 10, 11	wbr 5107	. . . . 5 wff 𝑧 < 𝑦
13	9, 12	wa 395	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)
14	13, 6, 4	crab 3405	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7389	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
16	1, 15	wceq 1540	1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  icoval  13344  elico1  13349  elicore  13359  icossico  13377  iccssico  13379  iccssico2  13381  icossxr  13393  icossicc  13397  ioossico  13399  icossioo  13401  icoun  13436  snunioo  13439  snunico  13440  ioojoin  13444  icopnfsup  13827  limsupgord  15438  leordtval2  23099  icomnfordt  23103  lecldbas  23106  mnfnei  23108  icopnfcld  24655  xrtgioo  24695  ioombl  25466  dvfsumrlimge0  25937  dvfsumrlim2  25939  psercnlem2  26334  tanord1  26446  rlimcnp  26875  rlimcnp2  26876  dchrisum0lem2a  27428  pntleml  27522  pnt  27525  joiniooico  32697  icorempo  37339  icoreresf  37340  isbasisrelowl  37346  icoreelrn  37349  relowlpssretop  37352  asindmre  37697  icof  45213  snunioo1  45510  elicores  45531  dmico  45561  liminfgord  45752  volicorescl  46551  iccdisj2  48885