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 12820
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 12816 . 2 class [,)
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 10745 . . 3 class *
52cv 1541 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1541 . . . . . 6 class 𝑧
8 cle 10747 . . . . . 6 class
95, 7, 8wbr 5027 . . . . 5 wff 𝑥𝑧
103cv 1541 . . . . . 6 class 𝑦
11 clt 10746 . . . . . 6 class <
127, 10, 11wbr 5027 . . . . 5 wff 𝑧 < 𝑦
139, 12wa 399 . . . 4 wff (𝑥𝑧𝑧 < 𝑦)
1413, 6, 4crab 3057 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)}
152, 3, 4, 4, 14cmpo 7166 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)})
161, 15wceq 1542 1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  icoval  12852  elico1  12857  elicore  12866  icossico  12884  iccssico  12886  iccssico2  12888  icossxr  12899  icossicc  12903  ioossico  12905  icossioo  12907  icoun  12942  snunioo  12945  snunico  12946  ioojoin  12950  icopnfsup  13317  limsupgord  14912  leordtval2  21956  icomnfordt  21960  lecldbas  21963  mnfnei  21965  icopnfcld  23513  xrtgioo  23551  ioombl  24310  dvfsumrlimge0  24774  dvfsumrlim2  24776  psercnlem2  25163  tanord1  25273  rlimcnp  25695  rlimcnp2  25696  dchrisum0lem2a  26245  pntleml  26339  pnt  26342  joiniooico  30662  icorempo  35134  icoreresf  35135  isbasisrelowl  35141  icoreelrn  35144  relowlpssretop  35147  asindmre  35472  icof  42281  snunioo1  42574  elicores  42595  dmico  42627  liminfgord  42821  volicorescl  43617  iccdisj2  45698
  Copyright terms: Public domain W3C validator