Definition df-ico 13356

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 13352	. 2 class [,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11216	. . 3 class ℝ*
5	2	cv 1560	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1560	. . . . . 6 class 𝑧
8		cle 11218	. . . . . 6 class ≤
9	5, 7, 8	wbr 5101	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1560	. . . . . 6 class 𝑦
11		clt 11217	. . . . . 6 class <
12	7, 10, 11	wbr 5101	. . . . 5 wff 𝑧 < 𝑦
13	9, 12	wa 399	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)
14	13, 6, 4	crab 3415	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7399	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
16	1, 15	wceq 1561	1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  icoval  13388  elico1  13393  elicore  13403  icossico  13421  iccssico  13423  iccssico2  13425  icossxr  13437  icossicc  13441  ioossico  13443  icossioo  13445  icoun  13480  snunioo  13483  snunico  13484  ioojoin  13488  icopnfsup  13876  limsupgord  15500  leordtval2  23273  icomnfordt  23277  lecldbas  23280  mnfnei  23282  icopnfcld  24828  xrtgioo  24868  ioombl  25628  dvfsumrlimge0  26093  dvfsumrlim2  26095  psercnlem2  26488  tanord1  26603  rlimcnp  27031  rlimcnp2  27032  dchrisum0lem2a  27582  pntleml  27676  pnt  27679  joiniooico  32977  icorempo  37846  icoreresf  37847  isbasisrelowl  37853  icoreelrn  37856  relowlpssretop  37859  asindmre  38203  icof  45796  snunioo1  46089  elicores  46110  dmico  46140  liminfgord  46329  volicorescl  47128  iccdisj2  49519