Definition df-ico 13330

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

This definition is referenced by:  icoval  13362  elico1  13367  elicore  13376  icossico  13394  iccssico  13396  iccssico2  13398  icossxr  13409  icossicc  13413  ioossico  13415  icossioo  13417  icoun  13452  snunioo  13455  snunico  13456  ioojoin  13460  icopnfsup  13830  limsupgord  15416  leordtval2  22716  icomnfordt  22720  lecldbas  22723  mnfnei  22725  icopnfcld  24284  xrtgioo  24322  ioombl  25082  dvfsumrlimge0  25547  dvfsumrlim2  25549  psercnlem2  25936  tanord1  26046  rlimcnp  26470  rlimcnp2  26471  dchrisum0lem2a  27020  pntleml  27114  pnt  27117  joiniooico  32016  icorempo  36280  icoreresf  36281  isbasisrelowl  36287  icoreelrn  36290  relowlpssretop  36293  asindmre  36619  icof  43966  snunioo1  44273  elicores  44294  dmico  44326  liminfgord  44518  volicorescl  45317  iccdisj2  47578