Definition df-ico 13242

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 13238	. 2 class [,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11136	. . 3 class ℝ*
5	2	cv 1539	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1539	. . . . . 6 class 𝑧
8		cle 11138	. . . . . 6 class ≤
9	5, 7, 8	wbr 5088	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1539	. . . . . 6 class 𝑦
11		clt 11137	. . . . . 6 class <
12	7, 10, 11	wbr 5088	. . . . 5 wff 𝑧 < 𝑦
13	9, 12	wa 395	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)
14	13, 6, 4	crab 3392	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7342	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
16	1, 15	wceq 1540	1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  icoval  13274  elico1  13279  elicore  13289  icossico  13307  iccssico  13309  iccssico2  13311  icossxr  13323  icossicc  13327  ioossico  13329  icossioo  13331  icoun  13366  snunioo  13369  snunico  13370  ioojoin  13374  icopnfsup  13757  limsupgord  15366  leordtval2  23081  icomnfordt  23085  lecldbas  23088  mnfnei  23090  icopnfcld  24636  xrtgioo  24676  ioombl  25447  dvfsumrlimge0  25918  dvfsumrlim2  25920  psercnlem2  26315  tanord1  26427  rlimcnp  26856  rlimcnp2  26857  dchrisum0lem2a  27409  pntleml  27503  pnt  27506  joiniooico  32709  icorempo  37342  icoreresf  37343  isbasisrelowl  37349  icoreelrn  37352  relowlpssretop  37355  asindmre  37700  icof  45213  snunioo1  45509  elicores  45530  dmico  45560  liminfgord  45749  volicorescl  46548  iccdisj2  48895