Definition df-ico 13366

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

This definition is referenced by:  icoval  13398  elico1  13403  elicore  13413  icossico  13431  iccssico  13433  iccssico2  13435  icossxr  13447  icossicc  13451  ioossico  13453  icossioo  13455  icoun  13490  snunioo  13493  snunico  13494  ioojoin  13498  icopnfsup  13880  limsupgord  15486  leordtval2  23148  icomnfordt  23152  lecldbas  23155  mnfnei  23157  icopnfcld  24704  xrtgioo  24744  ioombl  25516  dvfsumrlimge0  25987  dvfsumrlim2  25989  psercnlem2  26384  tanord1  26496  rlimcnp  26925  rlimcnp2  26926  dchrisum0lem2a  27478  pntleml  27572  pnt  27575  joiniooico  32697  icorempo  37315  icoreresf  37316  isbasisrelowl  37322  icoreelrn  37325  relowlpssretop  37328  asindmre  37673  icof  45191  snunioo1  45489  elicores  45510  dmico  45540  liminfgord  45731  volicorescl  46530  iccdisj2  48819