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

Definition df-ico 10882
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 10878 . 2  class  [,)
2 vx . . 3  set  x
3 vy . . 3  set  y
4 cxr 9079 . . 3  class  RR*
52cv 1648 . . . . . 6  class  x
6 vz . . . . . . 7  set  z
76cv 1648 . . . . . 6  class  z
8 cle 9081 . . . . . 6  class  <_
95, 7, 8wbr 4176 . . . . 5  wff  x  <_ 
z
103cv 1648 . . . . . 6  class  y
11 clt 9080 . . . . . 6  class  <
127, 10, 11wbr 4176 . . . . 5  wff  z  < 
y
139, 12wa 359 . . . 4  wff  ( x  <_  z  /\  z  <  y )
1413, 6, 4crab 2674 . . 3  class  { z  e.  RR*  |  (
x  <_  z  /\  z  <  y ) }
152, 3, 4, 4, 14cmpt2 6046 . 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  10914  elico1  10919  icossico  10940  iccssico  10942  iccssico2  10944  icossxr  10955  icoun  10981  snunioo  10983  snunico  10984  ioojoin  10987  icopnfsup  11205  limsupgord  12225  leordtval2  17234  icomnfordt  17238  lecldbas  17241  mnfnei  17243  icopnfcld  18759  xrtgioo  18794  ioombl  19416  itg2mulclem  19595  itg2mulc  19596  dvfsumrlimge0  19871  dvfsumrlim2  19873  psercnlem2  20297  tanord1  20396  rlimcnp  20761  rlimcnp2  20762  dchrisum0lem2a  21168  pntleml  21262  pnt  21265  icossicc  24086  ioossico  24088  icossioo  24090  joiniooico  24092
  Copyright terms: Public domain W3C validator