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

Definition df-ico 10914
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 10910 . 2  class  [,)
2 vx . . 3  set  x
3 vy . . 3  set  y
4 cxr 9111 . . 3  class  RR*
52cv 1651 . . . . . 6  class  x
6 vz . . . . . . 7  set  z
76cv 1651 . . . . . 6  class  z
8 cle 9113 . . . . . 6  class  <_
95, 7, 8wbr 4204 . . . . 5  wff  x  <_ 
z
103cv 1651 . . . . . 6  class  y
11 clt 9112 . . . . . 6  class  <
127, 10, 11wbr 4204 . . . . 5  wff  z  < 
y
139, 12wa 359 . . . 4  wff  ( x  <_  z  /\  z  <  y )
1413, 6, 4crab 2701 . . 3  class  { z  e.  RR*  |  (
x  <_  z  /\  z  <  y ) }
152, 3, 4, 4, 14cmpt2 6075 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  < 
y ) } )
161, 15wceq 1652 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  10946  elico1  10951  icossico  10972  iccssico  10974  iccssico2  10976  icossxr  10987  icoun  11013  snunioo  11015  snunico  11016  ioojoin  11019  icopnfsup  11238  limsupgord  12258  leordtval2  17268  icomnfordt  17272  lecldbas  17275  mnfnei  17277  icopnfcld  18794  xrtgioo  18829  ioombl  19451  itg2mulclem  19630  itg2mulc  19631  dvfsumrlimge0  19906  dvfsumrlim2  19908  psercnlem2  20332  tanord1  20431  rlimcnp  20796  rlimcnp2  20797  dchrisum0lem2a  21203  pntleml  21297  pnt  21300  icossicc  24121  ioossico  24123  icossioo  24125  joiniooico  24127
  Copyright terms: Public domain W3C validator