Definition df-ico 12820

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 12816	. 2 class [,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 10745	. . 3 class ℝ*
5	2	cv 1541	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1541	. . . . . 6 class 𝑧
8		cle 10747	. . . . . 6 class ≤
9	5, 7, 8	wbr 5027	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1541	. . . . . 6 class 𝑦
11		clt 10746	. . . . . 6 class <
12	7, 10, 11	wbr 5027	. . . . 5 wff 𝑧 < 𝑦
13	9, 12	wa 399	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)
14	13, 6, 4	crab 3057	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7166	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
16	1, 15	wceq 1542	1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  icoval  12852  elico1  12857  elicore  12866  icossico  12884  iccssico  12886  iccssico2  12888  icossxr  12899  icossicc  12903  ioossico  12905  icossioo  12907  icoun  12942  snunioo  12945  snunico  12946  ioojoin  12950  icopnfsup  13317  limsupgord  14912  leordtval2  21956  icomnfordt  21960  lecldbas  21963  mnfnei  21965  icopnfcld  23513  xrtgioo  23551  ioombl  24310  dvfsumrlimge0  24774  dvfsumrlim2  24776  psercnlem2  25163  tanord1  25273  rlimcnp  25695  rlimcnp2  25696  dchrisum0lem2a  26245  pntleml  26339  pnt  26342  joiniooico  30662  icorempo  35134  icoreresf  35135  isbasisrelowl  35141  icoreelrn  35144  relowlpssretop  35147  asindmre  35472  icof  42281  snunioo1  42574  elicores  42595  dmico  42627  liminfgord  42821  volicorescl  43617  iccdisj2  45698