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

Definition df-ico 10927
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 10923 . 2  class  [,)
2 vx . . 3  set  x
3 vy . . 3  set  y
4 cxr 9124 . . 3  class  RR*
52cv 1652 . . . . . 6  class  x
6 vz . . . . . . 7  set  z
76cv 1652 . . . . . 6  class  z
8 cle 9126 . . . . . 6  class  <_
95, 7, 8wbr 4215 . . . . 5  wff  x  <_ 
z
103cv 1652 . . . . . 6  class  y
11 clt 9125 . . . . . 6  class  <
127, 10, 11wbr 4215 . . . . 5  wff  z  < 
y
139, 12wa 360 . . . 4  wff  ( x  <_  z  /\  z  <  y )
1413, 6, 4crab 2711 . . 3  class  { z  e.  RR*  |  (
x  <_  z  /\  z  <  y ) }
152, 3, 4, 4, 14cmpt2 6086 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  < 
y ) } )
161, 15wceq 1653 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  10959  elico1  10964  icossico  10985  iccssico  10987  iccssico2  10989  icossxr  11000  icoun  11026  snunioo  11028  snunico  11029  ioojoin  11032  icopnfsup  11251  limsupgord  12271  leordtval2  17281  icomnfordt  17285  lecldbas  17288  mnfnei  17290  icopnfcld  18807  xrtgioo  18842  ioombl  19464  itg2mulclem  19641  itg2mulc  19642  dvfsumrlimge0  19919  dvfsumrlim2  19921  psercnlem2  20345  tanord1  20444  rlimcnp  20809  rlimcnp2  20810  dchrisum0lem2a  21216  pntleml  21310  pnt  21313  icossicc  24134  ioossico  24136  icossioo  24138  joiniooico  24140
  Copyright terms: Public domain W3C validator