Definition df-ico 13429

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 13425	. 2 class [,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11291	. . 3 class ℝ*
5	2	cv 1569	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1569	. . . . . 6 class 𝑧
8		cle 11293	. . . . . 6 class ≤
9	5, 7, 8	wbr 5103	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1569	. . . . . 6 class 𝑦
11		clt 11292	. . . . . 6 class <
12	7, 10, 11	wbr 5103	. . . . 5 wff 𝑧 < 𝑦
13	9, 12	wa 401	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)
14	13, 6, 4	crab 3412	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7418	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
16	1, 15	wceq 1570	1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})

This definition is used by:  icoval  13461  elico1  13466  elicore  13476  icossico  13494  iccssico  13496  iccssico2  13498  icossxr  13510  icossicc  13514  ioossico  13516  icossioo  13518  icoun  13553  snunioo  13556  snunico  13557  ioojoin  13561  icopnfsup  13951  limsupgord  15584  leordtval2  23469  icomnfordt  23473  lecldbas  23476  mnfnei  23478  icopnfcld  25025  xrtgioo  25065  ioombl  25825  dvfsumrlimge0  26289  dvfsumrlim2  26291  psercnlem2  26692  tanord1  26806  rlimcnp  27234  rlimcnp2  27235  dchrisum0lem2a  27785  pntleml  27879  pnt  27882  joiniooico  33277  icorempo  38170  icoreresf  38171  isbasisrelowl  38177  icoreelrn  38180  relowlpssretop  38183  asindmre  38517  icof  46114  snunioo1  46407  elicores  46428  dmico  46458  liminfgord  46647  volicorescl  47446  iccdisj2  49888