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

Definition df-ico 10662
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 10658 . 2  class  [,)
2 vx . . 3  set  x
3 vy . . 3  set  y
4 cxr 8866 . . 3  class  RR*
52cv 1622 . . . . . 6  class  x
6 vz . . . . . . 7  set  z
76cv 1622 . . . . . 6  class  z
8 cle 8868 . . . . . 6  class  <_
95, 7, 8wbr 4023 . . . . 5  wff  x  <_ 
z
103cv 1622 . . . . . 6  class  y
11 clt 8867 . . . . . 6  class  <
127, 10, 11wbr 4023 . . . . 5  wff  z  < 
y
139, 12wa 358 . . . 4  wff  ( x  <_  z  /\  z  <  y )
1413, 6, 4crab 2547 . . 3  class  { z  e.  RR*  |  (
x  <_  z  /\  z  <  y ) }
152, 3, 4, 4, 14cmpt2 5860 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  < 
y ) } )
161, 15wceq 1623 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  10694  elico1  10699  iccssico  10721  iccssico2  10723  icossxr  10734  icoun  10760  snunioo  10762  snunico  10763  ioojoin  10766  icopnfsup  10969  limsupgord  11946  leordtval2  16942  icomnfordt  16946  lecldbas  16949  mnfnei  16951  icopnfcld  18277  xrtgioo  18312  ioombl  18922  itg2mulclem  19101  itg2mulc  19102  dvfsumrlimge0  19377  dvfsumrlim2  19379  psercnlem2  19800  tanord1  19899  rlimcnp  20260  rlimcnp2  20261  dchrisum0lem2a  20666  pntleml  20760  pnt  20763  icossicc  23258  ioossico  23260  icossioo  23262  icossico  23263  joiniooico  23265  tpr2rico  23296  icof  25640
  Copyright terms: Public domain W3C validator