MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ico Structured version   Unicode version

Definition df-ico 10953
Description: Define the set of closed-below, open-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
Assertion
Ref Expression
df-ico  |-  [,)  =  ( x  e.  RR* ,  y  e.  RR*  |->  { z  e.  RR*  |  (
x  <_  z  /\  z  <  y ) } )
Distinct variable group:    x, y, z

Detailed syntax breakdown of Definition df-ico
StepHypRef Expression
1 cico 10949 . 2  class  [,)
2 vx . . 3  set  x
3 vy . . 3  set  y
4 cxr 9150 . . 3  class  RR*
52cv 1652 . . . . . 6  class  x
6 vz . . . . . . 7  set  z
76cv 1652 . . . . . 6  class  z
8 cle 9152 . . . . . 6  class  <_
95, 7, 8wbr 4237 . . . . 5  wff  x  <_ 
z
103cv 1652 . . . . . 6  class  y
11 clt 9151 . . . . . 6  class  <
127, 10, 11wbr 4237 . . . . 5  wff  z  < 
y
139, 12wa 360 . . . 4  wff  ( x  <_  z  /\  z  <  y )
1413, 6, 4crab 2715 . . 3  class  { z  e.  RR*  |  (
x  <_  z  /\  z  <  y ) }
152, 3, 4, 4, 14cmpt2 6112 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  < 
y ) } )
161, 15wceq 1653 1  wff  [,)  =  ( x  e.  RR* ,  y  e.  RR*  |->  { z  e.  RR*  |  (
x  <_  z  /\  z  <  y ) } )
Colors of variables: wff set class
This definition is referenced by:  icoval  10985  elico1  10990  icossico  11011  iccssico  11013  iccssico2  11015  icossxr  11026  icoun  11052  snunioo  11054  snunico  11055  ioojoin  11058  icopnfsup  11277  limsupgord  12297  leordtval2  17307  icomnfordt  17311  lecldbas  17314  mnfnei  17316  icopnfcld  18833  xrtgioo  18868  ioombl  19490  itg2mulclem  19667  itg2mulc  19668  dvfsumrlimge0  19945  dvfsumrlim2  19947  psercnlem2  20371  tanord1  20470  rlimcnp  20835  rlimcnp2  20836  dchrisum0lem2a  21242  pntleml  21336  pnt  21339  icossicc  24160  ioossico  24162  icossioo  24164  joiniooico  24166
  Copyright terms: Public domain W3C validator