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

Definition df-ico 10878
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 10874 . 2  class  [,)
2 vx . . 3  set  x
3 vy . . 3  set  y
4 cxr 9075 . . 3  class  RR*
52cv 1648 . . . . . 6  class  x
6 vz . . . . . . 7  set  z
76cv 1648 . . . . . 6  class  z
8 cle 9077 . . . . . 6  class  <_
95, 7, 8wbr 4172 . . . . 5  wff  x  <_ 
z
103cv 1648 . . . . . 6  class  y
11 clt 9076 . . . . . 6  class  <
127, 10, 11wbr 4172 . . . . 5  wff  z  < 
y
139, 12wa 359 . . . 4  wff  ( x  <_  z  /\  z  <  y )
1413, 6, 4crab 2670 . . 3  class  { z  e.  RR*  |  (
x  <_  z  /\  z  <  y ) }
152, 3, 4, 4, 14cmpt2 6042 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  < 
y ) } )
161, 15wceq 1649 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  10910  elico1  10915  icossico  10936  iccssico  10938  iccssico2  10940  icossxr  10951  icoun  10977  snunioo  10979  snunico  10980  ioojoin  10983  icopnfsup  11201  limsupgord  12221  leordtval2  17230  icomnfordt  17234  lecldbas  17237  mnfnei  17239  icopnfcld  18755  xrtgioo  18790  ioombl  19412  itg2mulclem  19591  itg2mulc  19592  dvfsumrlimge0  19867  dvfsumrlim2  19869  psercnlem2  20293  tanord1  20392  rlimcnp  20757  rlimcnp2  20758  dchrisum0lem2a  21164  pntleml  21258  pnt  21261  icossicc  24082  ioossico  24084  icossioo  24086  joiniooico  24088
  Copyright terms: Public domain W3C validator