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

Definition df-ioo 10655
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 10651 . 2  class  (,)
2 vx . . 3  set  x
3 vy . . 3  set  y
4 cxr 8862 . . 3  class  RR*
52cv 1623 . . . . . 6  class  x
6 vz . . . . . . 7  set  z
76cv 1623 . . . . . 6  class  z
8 clt 8863 . . . . . 6  class  <
95, 7, 8wbr 4025 . . . . 5  wff  x  < 
z
103cv 1623 . . . . . 6  class  y
117, 10, 8wbr 4025 . . . . 5  wff  z  < 
y
129, 11wa 360 . . . 4  wff  ( x  <  z  /\  z  <  y )
1312, 6, 4crab 2549 . . 3  class  { z  e.  RR*  |  (
x  <  z  /\  z  <  y ) }
142, 3, 4, 4, 13cmpt2 5822 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  < 
y ) } )
151, 14wceq 1624 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  10674  iooval  10675  ndmioo  10678  elioo3g  10680  iooin  10685  iooss1  10686  iooss2  10687  elioo1  10691  iccssioo  10714  ioossicc  10730  ioof  10736  snunioo  10757  ioodisj  10760  ioojoin  10761  ioopnfsup  10963  leordtval  16938  icopnfcld  18272  iocmnfcld  18273  bndth  18451  ioombl  18917  ioorf  18923  ioorinv2  18925  ismbf3d  19004  dvfsumrlimge0  19372  dvfsumrlim2  19374  tanord1  19894  dvloglem  19990  rlimcnp  20255  rlimcnp2  20256  dchrisum0lem2a  20661  pnt  20758
  Copyright terms: Public domain W3C validator