MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ico Structured version   Visualization version   GIF version

Definition df-ico 13393
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
StepHypRef Expression
1 cico 13389 . 2 class [,)
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 11294 . . 3 class *
52cv 1539 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1539 . . . . . 6 class 𝑧
8 cle 11296 . . . . . 6 class
95, 7, 8wbr 5143 . . . . 5 wff 𝑥𝑧
103cv 1539 . . . . . 6 class 𝑦
11 clt 11295 . . . . . 6 class <
127, 10, 11wbr 5143 . . . . 5 wff 𝑧 < 𝑦
139, 12wa 395 . . . 4 wff (𝑥𝑧𝑧 < 𝑦)
1413, 6, 4crab 3436 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)}
152, 3, 4, 4, 14cmpo 7433 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)})
161, 15wceq 1540 1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  icoval  13425  elico1  13430  elicore  13439  icossico  13457  iccssico  13459  iccssico2  13461  icossxr  13472  icossicc  13476  ioossico  13478  icossioo  13480  icoun  13515  snunioo  13518  snunico  13519  ioojoin  13523  icopnfsup  13905  limsupgord  15508  leordtval2  23220  icomnfordt  23224  lecldbas  23227  mnfnei  23229  icopnfcld  24788  xrtgioo  24828  ioombl  25600  dvfsumrlimge0  26071  dvfsumrlim2  26073  psercnlem2  26468  tanord1  26579  rlimcnp  27008  rlimcnp2  27009  dchrisum0lem2a  27561  pntleml  27655  pnt  27658  joiniooico  32776  icorempo  37352  icoreresf  37353  isbasisrelowl  37359  icoreelrn  37362  relowlpssretop  37365  asindmre  37710  icof  45224  snunioo1  45525  elicores  45546  dmico  45578  liminfgord  45769  volicorescl  46568  iccdisj2  48795
  Copyright terms: Public domain W3C validator