Definition df-ico 13094

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 13090	. 2 class [,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11017	. . 3 class ℝ*
5	2	cv 1538	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1538	. . . . . 6 class 𝑧
8		cle 11019	. . . . . 6 class ≤
9	5, 7, 8	wbr 5075	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1538	. . . . . 6 class 𝑦
11		clt 11018	. . . . . 6 class <
12	7, 10, 11	wbr 5075	. . . . 5 wff 𝑧 < 𝑦
13	9, 12	wa 396	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)
14	13, 6, 4	crab 3069	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7286	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
16	1, 15	wceq 1539	1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  icoval  13126  elico1  13131  elicore  13140  icossico  13158  iccssico  13160  iccssico2  13162  icossxr  13173  icossicc  13177  ioossico  13179  icossioo  13181  icoun  13216  snunioo  13219  snunico  13220  ioojoin  13224  icopnfsup  13594  limsupgord  15190  leordtval2  22372  icomnfordt  22376  lecldbas  22379  mnfnei  22381  icopnfcld  23940  xrtgioo  23978  ioombl  24738  dvfsumrlimge0  25203  dvfsumrlim2  25205  psercnlem2  25592  tanord1  25702  rlimcnp  26124  rlimcnp2  26125  dchrisum0lem2a  26674  pntleml  26768  pnt  26771  joiniooico  31104  icorempo  35531  icoreresf  35532  isbasisrelowl  35538  icoreelrn  35541  relowlpssretop  35544  asindmre  35869  icof  42766  snunioo1  43057  elicores  43078  dmico  43110  liminfgord  43302  volicorescl  44098  iccdisj2  46202