Definition df-ico 13254

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

This definition is referenced by:  icoval  13286  elico1  13291  elicore  13301  icossico  13319  iccssico  13321  iccssico2  13323  icossxr  13335  icossicc  13339  ioossico  13341  icossioo  13343  icoun  13378  snunioo  13381  snunico  13382  ioojoin  13386  icopnfsup  13769  limsupgord  15379  leordtval2  23097  icomnfordt  23101  lecldbas  23104  mnfnei  23106  icopnfcld  24653  xrtgioo  24693  ioombl  25464  dvfsumrlimge0  25935  dvfsumrlim2  25937  psercnlem2  26332  tanord1  26444  rlimcnp  26873  rlimcnp2  26874  dchrisum0lem2a  27426  pntleml  27520  pnt  27523  joiniooico  32717  icorempo  37325  icoreresf  37326  isbasisrelowl  37332  icoreelrn  37335  relowlpssretop  37338  asindmre  37683  icof  45197  snunioo1  45493  elicores  45514  dmico  45544  liminfgord  45735  volicorescl  46534  iccdisj2  48881