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 12395
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 12391 . 2 class [,)
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 10354 . . 3 class *
52cv 1636 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1636 . . . . . 6 class 𝑧
8 cle 10356 . . . . . 6 class
95, 7, 8wbr 4844 . . . . 5 wff 𝑥𝑧
103cv 1636 . . . . . 6 class 𝑦
11 clt 10355 . . . . . 6 class <
127, 10, 11wbr 4844 . . . . 5 wff 𝑧 < 𝑦
139, 12wa 384 . . . 4 wff (𝑥𝑧𝑧 < 𝑦)
1413, 6, 4crab 3100 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)}
152, 3, 4, 4, 14cmpt2 6872 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)})
161, 15wceq 1637 1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  icoval  12427  elico1  12432  elicore  12440  icossico  12457  iccssico  12459  iccssico2  12461  icossxr  12472  icossicc  12475  ioossico  12477  icossioo  12479  icoun  12513  snunioo  12517  snunico  12518  ioojoin  12522  icopnfsup  12884  limsupgord  14422  leordtval2  21226  icomnfordt  21230  lecldbas  21233  mnfnei  21235  icopnfcld  22780  xrtgioo  22818  ioombl  23542  dvfsumrlimge0  24003  dvfsumrlim2  24005  psercnlem2  24388  tanord1  24494  rlimcnp  24902  rlimcnp2  24903  dchrisum0lem2a  25416  pntleml  25510  pnt  25513  joiniooico  29859  icorempt2  33510  icoreresf  33511  isbasisrelowl  33517  icoreelrn  33520  relowlpssretop  33523  asindmre  33802  icof  39892  snunioo1  40213  elicores  40234  dmico  40266  liminfgord  40460  volicorescl  41243
  Copyright terms: Public domain W3C validator