Definition df-ico 13327

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 13323	. 2 class [,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11244	. . 3 class ℝ*
5	2	cv 1541	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1541	. . . . . 6 class 𝑧
8		cle 11246	. . . . . 6 class ≤
9	5, 7, 8	wbr 5148	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1541	. . . . . 6 class 𝑦
11		clt 11245	. . . . . 6 class <
12	7, 10, 11	wbr 5148	. . . . 5 wff 𝑧 < 𝑦
13	9, 12	wa 397	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)
14	13, 6, 4	crab 3433	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7408	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
16	1, 15	wceq 1542	1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  icoval  13359  elico1  13364  elicore  13373  icossico  13391  iccssico  13393  iccssico2  13395  icossxr  13406  icossicc  13410  ioossico  13412  icossioo  13414  icoun  13449  snunioo  13452  snunico  13453  ioojoin  13457  icopnfsup  13827  limsupgord  15413  leordtval2  22708  icomnfordt  22712  lecldbas  22715  mnfnei  22717  icopnfcld  24276  xrtgioo  24314  ioombl  25074  dvfsumrlimge0  25539  dvfsumrlim2  25541  psercnlem2  25928  tanord1  26038  rlimcnp  26460  rlimcnp2  26461  dchrisum0lem2a  27010  pntleml  27104  pnt  27107  joiniooico  31973  icorempo  36221  icoreresf  36222  isbasisrelowl  36228  icoreelrn  36231  relowlpssretop  36234  asindmre  36560  icof  43904  snunioo1  44212  elicores  44233  dmico  44265  liminfgord  44457  volicorescl  45256  iccdisj2  47484