Definition df-ico 13296

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 13292	. 2 class [,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11170	. . 3 class ℝ*
5	2	cv 1546	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1546	. . . . . 6 class 𝑧
8		cle 11172	. . . . . 6 class ≤
9	5, 7, 8	wbr 5073	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1546	. . . . . 6 class 𝑦
11		clt 11171	. . . . . 6 class <
12	7, 10, 11	wbr 5073	. . . . 5 wff 𝑧 < 𝑦
13	9, 12	wa 396	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)
14	13, 6, 4	crab 3391	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7359	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
16	1, 15	wceq 1547	1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  icoval  13328  elico1  13333  elicore  13343  icossico  13361  iccssico  13363  iccssico2  13365  icossxr  13377  icossicc  13381  ioossico  13383  icossioo  13385  icoun  13420  snunioo  13423  snunico  13424  ioojoin  13428  icopnfsup  13816  limsupgord  15426  leordtval2  23196  icomnfordt  23200  lecldbas  23203  mnfnei  23205  icopnfcld  24751  xrtgioo  24791  ioombl  25551  dvfsumrlimge0  26016  dvfsumrlim2  26018  psercnlem2  26408  tanord1  26520  rlimcnp  26948  rlimcnp2  26949  dchrisum0lem2a  27499  pntleml  27593  pnt  27596  joiniooico  32867  icorempo  37722  icoreresf  37723  isbasisrelowl  37729  icoreelrn  37732  relowlpssretop  37735  asindmre  38079  icof  45672  snunioo1  45965  elicores  45986  dmico  46016  liminfgord  46205  volicorescl  47004  iccdisj2  49395