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 12052
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 12048 . 2 class [,)
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 9952 . . 3 class *
52cv 1474 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1474 . . . . . 6 class 𝑧
8 cle 9954 . . . . . 6 class
95, 7, 8wbr 4583 . . . . 5 wff 𝑥𝑧
103cv 1474 . . . . . 6 class 𝑦
11 clt 9953 . . . . . 6 class <
127, 10, 11wbr 4583 . . . . 5 wff 𝑧 < 𝑦
139, 12wa 383 . . . 4 wff (𝑥𝑧𝑧 < 𝑦)
1413, 6, 4crab 2900 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)}
152, 3, 4, 4, 14cmpt2 6551 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)})
161, 15wceq 1475 1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  icoval  12084  elico1  12089  elicore  12097  icossico  12114  iccssico  12116  iccssico2  12118  icossxr  12129  icossicc  12131  ioossico  12133  icossioo  12135  icoun  12167  snunioo  12169  snunico  12170  ioojoin  12174  icopnfsup  12526  limsupgord  14051  leordtval2  20826  icomnfordt  20830  lecldbas  20833  mnfnei  20835  icopnfcld  22381  xrtgioo  22417  ioombl  23140  dvfsumrlimge0  23597  dvfsumrlim2  23599  psercnlem2  23982  tanord1  24087  rlimcnp  24492  rlimcnp2  24493  dchrisum0lem2a  25006  pntleml  25100  pnt  25103  joiniooico  28926  icorempt2  32375  icoreresf  32376  isbasisrelowl  32382  icoreelrn  32385  relowlpssretop  32388  asindmre  32665  icof  38406  snunioo1  38585  elicores  38607  volicorescl  39443
  Copyright terms: Public domain W3C validator