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 12737
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 12733 . 2 class [,)
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 10666 . . 3 class *
52cv 1529 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1529 . . . . . 6 class 𝑧
8 cle 10668 . . . . . 6 class
95, 7, 8wbr 5062 . . . . 5 wff 𝑥𝑧
103cv 1529 . . . . . 6 class 𝑦
11 clt 10667 . . . . . 6 class <
127, 10, 11wbr 5062 . . . . 5 wff 𝑧 < 𝑦
139, 12wa 396 . . . 4 wff (𝑥𝑧𝑧 < 𝑦)
1413, 6, 4crab 3146 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)}
152, 3, 4, 4, 14cmpo 7153 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)})
161, 15wceq 1530 1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  icoval  12769  elico1  12774  elicore  12782  icossico  12799  iccssico  12801  iccssico2  12803  icossxr  12814  icossicc  12817  ioossico  12819  icossioo  12821  icoun  12854  snunioo  12857  snunico  12858  ioojoin  12862  icopnfsup  13226  limsupgord  14822  leordtval2  21736  icomnfordt  21740  lecldbas  21743  mnfnei  21745  icopnfcld  23291  xrtgioo  23329  ioombl  24081  dvfsumrlimge0  24542  dvfsumrlim2  24544  psercnlem2  24927  tanord1  25034  rlimcnp  25457  rlimcnp2  25458  dchrisum0lem2a  26007  pntleml  26101  pnt  26104  joiniooico  30410  icorempo  34501  icoreresf  34502  isbasisrelowl  34508  icoreelrn  34511  relowlpssretop  34514  asindmre  34844  icof  41343  snunioo1  41649  elicores  41670  dmico  41702  liminfgord  41896  volicorescl  42697
  Copyright terms: Public domain W3C validator