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

Definition df-ioo 10876
Description: Define the set of open intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
Assertion
Ref Expression
df-ioo  |-  (,)  =  ( 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-ioo
StepHypRef Expression
1 cioo 10872 . 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 clt 9076 . . . . . 6  class  <
95, 7, 8wbr 4172 . . . . 5  wff  x  < 
z
103cv 1648 . . . . . 6  class  y
117, 10, 8wbr 4172 . . . . 5  wff  z  < 
y
129, 11wa 359 . . . 4  wff  ( x  <  z  /\  z  <  y )
1312, 6, 4crab 2670 . . 3  class  { z  e.  RR*  |  (
x  <  z  /\  z  <  y ) }
142, 3, 4, 4, 13cmpt2 6042 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  < 
y ) } )
151, 14wceq 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:  iooex  10895  iooval  10896  ndmioo  10899  elioo3g  10901  iooin  10906  iooss1  10907  iooss2  10908  elioo1  10912  iccssioo  10935  ioossicc  10952  ioof  10958  snunioo  10979  ioodisj  10982  ioojoin  10983  ioopnfsup  11200  leordtval  17231  icopnfcld  18755  iocmnfcld  18756  bndth  18936  ioombl  19412  ioorf  19418  ioorinv2  19420  ismbf3d  19499  dvfsumrlimge0  19867  dvfsumrlim2  19869  tanord1  20392  dvloglem  20492  rlimcnp  20757  rlimcnp2  20758  dchrisum0lem2a  21164  pnt  21261  ioossico  24084  iocssioo  24085  icossioo  24086  ioossioo  24087  joiniooico  24088  tpr2rico  24263  ftc1cnnclem  26177
  Copyright terms: Public domain W3C validator