Definition df-ico 13319

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

This definition is referenced by:  icoval  13351  elico1  13356  elicore  13366  icossico  13384  iccssico  13386  iccssico2  13388  icossxr  13400  icossicc  13404  ioossico  13406  icossioo  13408  icoun  13443  snunioo  13446  snunico  13447  ioojoin  13451  icopnfsup  13834  limsupgord  15445  leordtval2  23106  icomnfordt  23110  lecldbas  23113  mnfnei  23115  icopnfcld  24662  xrtgioo  24702  ioombl  25473  dvfsumrlimge0  25944  dvfsumrlim2  25946  psercnlem2  26341  tanord1  26453  rlimcnp  26882  rlimcnp2  26883  dchrisum0lem2a  27435  pntleml  27529  pnt  27532  joiniooico  32704  icorempo  37346  icoreresf  37347  isbasisrelowl  37353  icoreelrn  37356  relowlpssretop  37359  asindmre  37704  icof  45220  snunioo1  45517  elicores  45538  dmico  45568  liminfgord  45759  volicorescl  46558  iccdisj2  48889