Definition df-ico 13014

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 13010	. 2 class [,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 10939	. . 3 class ℝ*
5	2	cv 1538	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1538	. . . . . 6 class 𝑧
8		cle 10941	. . . . . 6 class ≤
9	5, 7, 8	wbr 5070	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1538	. . . . . 6 class 𝑦
11		clt 10940	. . . . . 6 class <
12	7, 10, 11	wbr 5070	. . . . 5 wff 𝑧 < 𝑦
13	9, 12	wa 395	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)
14	13, 6, 4	crab 3067	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7257	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
16	1, 15	wceq 1539	1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  icoval  13046  elico1  13051  elicore  13060  icossico  13078  iccssico  13080  iccssico2  13082  icossxr  13093  icossicc  13097  ioossico  13099  icossioo  13101  icoun  13136  snunioo  13139  snunico  13140  ioojoin  13144  icopnfsup  13513  limsupgord  15109  leordtval2  22271  icomnfordt  22275  lecldbas  22278  mnfnei  22280  icopnfcld  23837  xrtgioo  23875  ioombl  24634  dvfsumrlimge0  25099  dvfsumrlim2  25101  psercnlem2  25488  tanord1  25598  rlimcnp  26020  rlimcnp2  26021  dchrisum0lem2a  26570  pntleml  26664  pnt  26667  joiniooico  30997  icorempo  35449  icoreresf  35450  isbasisrelowl  35456  icoreelrn  35459  relowlpssretop  35462  asindmre  35787  icof  42648  snunioo1  42940  elicores  42961  dmico  42993  liminfgord  43185  volicorescl  43981  iccdisj2  46079