Definition df-ico 13389

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 13385	. 2 class [,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11291	. . 3 class ℝ*
5	2	cv 1535	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1535	. . . . . 6 class 𝑧
8		cle 11293	. . . . . 6 class ≤
9	5, 7, 8	wbr 5147	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1535	. . . . . 6 class 𝑦
11		clt 11292	. . . . . 6 class <
12	7, 10, 11	wbr 5147	. . . . 5 wff 𝑧 < 𝑦
13	9, 12	wa 395	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)
14	13, 6, 4	crab 3432	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7432	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
16	1, 15	wceq 1536	1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  icoval  13421  elico1  13426  elicore  13435  icossico  13453  iccssico  13455  iccssico2  13457  icossxr  13468  icossicc  13472  ioossico  13474  icossioo  13476  icoun  13511  snunioo  13514  snunico  13515  ioojoin  13519  icopnfsup  13901  limsupgord  15504  leordtval2  23235  icomnfordt  23239  lecldbas  23242  mnfnei  23244  icopnfcld  24803  xrtgioo  24841  ioombl  25613  dvfsumrlimge0  26085  dvfsumrlim2  26087  psercnlem2  26482  tanord1  26593  rlimcnp  27022  rlimcnp2  27023  dchrisum0lem2a  27575  pntleml  27669  pnt  27672  joiniooico  32782  icorempo  37333  icoreresf  37334  isbasisrelowl  37340  icoreelrn  37343  relowlpssretop  37346  asindmre  37689  icof  45161  snunioo1  45464  elicores  45485  dmico  45517  liminfgord  45709  volicorescl  46508  iccdisj2  48693