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

Definition df-ioo 10922
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 10918 . 2  class  (,)
2 vx . . 3  set  x
3 vy . . 3  set  y
4 cxr 9121 . . 3  class  RR*
52cv 1652 . . . . . 6  class  x
6 vz . . . . . . 7  set  z
76cv 1652 . . . . . 6  class  z
8 clt 9122 . . . . . 6  class  <
95, 7, 8wbr 4214 . . . . 5  wff  x  < 
z
103cv 1652 . . . . . 6  class  y
117, 10, 8wbr 4214 . . . . 5  wff  z  < 
y
129, 11wa 360 . . . 4  wff  ( x  <  z  /\  z  <  y )
1312, 6, 4crab 2711 . . 3  class  { z  e.  RR*  |  (
x  <  z  /\  z  <  y ) }
142, 3, 4, 4, 13cmpt2 6085 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  < 
y ) } )
151, 14wceq 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:  iooex  10941  iooval  10942  ndmioo  10945  elioo3g  10947  iooin  10952  iooss1  10953  iooss2  10954  elioo1  10958  iccssioo  10981  ioossicc  10998  ioof  11004  snunioo  11025  ioodisj  11028  ioojoin  11029  ioopnfsup  11247  leordtval  17279  icopnfcld  18804  iocmnfcld  18805  bndth  18985  ioombl  19461  ioorf  19467  ioorinv2  19469  ismbf3d  19548  dvfsumrlimge0  19916  dvfsumrlim2  19918  tanord1  20441  dvloglem  20541  rlimcnp  20806  rlimcnp2  20807  dchrisum0lem2a  21213  pnt  21310  ioossico  24133  iocssioo  24134  icossioo  24135  ioossioo  24136  joiniooico  24137  tpr2rico  24312  ftc1cnnclem  26280  ftc1anclem7  26288  ftc1anclem8  26289  ftc1anc  26290  ftc2nc  26291
  Copyright terms: Public domain W3C validator