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 12010
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 12006 . 2 class [,)
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 9929 . . 3 class *
52cv 1473 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1473 . . . . . 6 class 𝑧
8 cle 9931 . . . . . 6 class
95, 7, 8wbr 4577 . . . . 5 wff 𝑥𝑧
103cv 1473 . . . . . 6 class 𝑦
11 clt 9930 . . . . . 6 class <
127, 10, 11wbr 4577 . . . . 5 wff 𝑧 < 𝑦
139, 12wa 382 . . . 4 wff (𝑥𝑧𝑧 < 𝑦)
1413, 6, 4crab 2899 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)}
152, 3, 4, 4, 14cmpt2 6528 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)})
161, 15wceq 1474 1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  icoval  12042  elico1  12047  elicore  12055  icossico  12072  iccssico  12074  iccssico2  12076  icossxr  12087  icossicc  12089  ioossico  12091  icossioo  12093  icoun  12125  snunioo  12127  snunico  12128  ioojoin  12132  icopnfsup  12483  limsupgord  13999  leordtval2  20773  icomnfordt  20777  lecldbas  20780  mnfnei  20782  icopnfcld  22328  xrtgioo  22364  ioombl  23084  dvfsumrlimge0  23541  dvfsumrlim2  23543  psercnlem2  23926  tanord1  24031  rlimcnp  24436  rlimcnp2  24437  dchrisum0lem2a  24950  pntleml  25044  pnt  25047  joiniooico  28719  icorempt2  32158  icoreresf  32159  isbasisrelowl  32165  icoreelrn  32168  relowlpssretop  32171  asindmre  32448  icof  38189  snunioo1  38368  elicores  38390  volicorescl  39226
  Copyright terms: Public domain W3C validator