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

Definition df-ico 10751
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 10747 . 2  class  [,)
2 vx . . 3  set  x
3 vy . . 3  set  y
4 cxr 8953 . . 3  class  RR*
52cv 1641 . . . . . 6  class  x
6 vz . . . . . . 7  set  z
76cv 1641 . . . . . 6  class  z
8 cle 8955 . . . . . 6  class  <_
95, 7, 8wbr 4102 . . . . 5  wff  x  <_ 
z
103cv 1641 . . . . . 6  class  y
11 clt 8954 . . . . . 6  class  <
127, 10, 11wbr 4102 . . . . 5  wff  z  < 
y
139, 12wa 358 . . . 4  wff  ( x  <_  z  /\  z  <  y )
1413, 6, 4crab 2623 . . 3  class  { z  e.  RR*  |  (
x  <_  z  /\  z  <  y ) }
152, 3, 4, 4, 14cmpt2 5944 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  < 
y ) } )
161, 15wceq 1642 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  10783  elico1  10788  iccssico  10810  iccssico2  10812  icossxr  10823  icoun  10849  snunioo  10851  snunico  10852  ioojoin  10855  icopnfsup  11058  limsupgord  12036  leordtval2  17042  icomnfordt  17046  lecldbas  17049  mnfnei  17051  icopnfcld  18373  xrtgioo  18408  ioombl  19020  itg2mulclem  19199  itg2mulc  19200  dvfsumrlimge0  19475  dvfsumrlim2  19477  psercnlem2  19901  tanord1  20000  rlimcnp  20365  rlimcnp2  20366  dchrisum0lem2a  20772  pntleml  20866  pnt  20869  icossicc  23327  ioossico  23329  icossioo  23331  icossico  23332  joiniooico  23334  itg2addnc  25494
  Copyright terms: Public domain W3C validator