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

Definition df-ico 10657
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 10653 . 2  class  [,)
2 vx . . 3  set  x
3 vy . . 3  set  y
4 cxr 8862 . . 3  class  RR*
52cv 1623 . . . . . 6  class  x
6 vz . . . . . . 7  set  z
76cv 1623 . . . . . 6  class  z
8 cle 8864 . . . . . 6  class  <_
95, 7, 8wbr 4025 . . . . 5  wff  x  <_ 
z
103cv 1623 . . . . . 6  class  y
11 clt 8863 . . . . . 6  class  <
127, 10, 11wbr 4025 . . . . 5  wff  z  < 
y
139, 12wa 360 . . . 4  wff  ( x  <_  z  /\  z  <  y )
1413, 6, 4crab 2549 . . 3  class  { z  e.  RR*  |  (
x  <_  z  /\  z  <  y ) }
152, 3, 4, 4, 14cmpt2 5822 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  < 
y ) } )
161, 15wceq 1624 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  10689  elico1  10694  iccssico  10716  iccssico2  10718  icossxr  10729  icoun  10755  snunioo  10757  snunico  10758  ioojoin  10761  icopnfsup  10964  limsupgord  11941  leordtval2  16937  icomnfordt  16941  lecldbas  16944  mnfnei  16946  icopnfcld  18272  xrtgioo  18307  ioombl  18917  itg2mulclem  19096  itg2mulc  19097  dvfsumrlimge0  19372  dvfsumrlim2  19374  psercnlem2  19795  tanord1  19894  rlimcnp  20255  rlimcnp2  20256  dchrisum0lem2a  20661  pntleml  20755  pnt  20758  icof  25040
  Copyright terms: Public domain W3C validator