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

Definition df-ioo 10813
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 10809 . 2  class  (,)
2 vx . . 3  set  x
3 vy . . 3  set  y
4 cxr 9013 . . 3  class  RR*
52cv 1646 . . . . . 6  class  x
6 vz . . . . . . 7  set  z
76cv 1646 . . . . . 6  class  z
8 clt 9014 . . . . . 6  class  <
95, 7, 8wbr 4125 . . . . 5  wff  x  < 
z
103cv 1646 . . . . . 6  class  y
117, 10, 8wbr 4125 . . . . 5  wff  z  < 
y
129, 11wa 358 . . . 4  wff  ( x  <  z  /\  z  <  y )
1312, 6, 4crab 2632 . . 3  class  { z  e.  RR*  |  (
x  <  z  /\  z  <  y ) }
142, 3, 4, 4, 13cmpt2 5983 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  < 
y ) } )
151, 14wceq 1647 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  10832  iooval  10833  ndmioo  10836  elioo3g  10838  iooin  10843  iooss1  10844  iooss2  10845  elioo1  10849  iccssioo  10872  ioossicc  10888  ioof  10894  snunioo  10915  ioodisj  10918  ioojoin  10919  ioopnfsup  11132  leordtval  17160  icopnfcld  18490  iocmnfcld  18491  bndth  18671  ioombl  19137  ioorf  19143  ioorinv2  19145  ismbf3d  19224  dvfsumrlimge0  19592  dvfsumrlim2  19594  tanord1  20117  dvloglem  20217  rlimcnp  20482  rlimcnp2  20483  dchrisum0lem2a  20889  pnt  20986  ioossico  23531  iocssioo  23532  icossioo  23533  ioossioo  23535  joiniooico  23536  tpr2rico  23665  ftc1cnnclem  25696
  Copyright terms: Public domain W3C validator