ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-ioo Unicode version

Definition df-ioo 9643
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 9639 . 2  class  (,)
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cxr 7767 . . 3  class  RR*
52cv 1315 . . . . . 6  class  x
6 vz . . . . . . 7  setvar  z
76cv 1315 . . . . . 6  class  z
8 clt 7768 . . . . . 6  class  <
95, 7, 8wbr 3899 . . . . 5  wff  x  < 
z
103cv 1315 . . . . . 6  class  y
117, 10, 8wbr 3899 . . . . 5  wff  z  < 
y
129, 11wa 103 . . . 4  wff  ( x  <  z  /\  z  <  y )
1312, 6, 4crab 2397 . . 3  class  { z  e.  RR*  |  (
x  <  z  /\  z  <  y ) }
142, 3, 4, 4, 13cmpo 5744 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  < 
y ) } )
151, 14wceq 1316 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  9658  iooval  9659  elioo3g  9661  elioo1  9662  iooss1  9667  iooss2  9668  eliooxr  9678  iccssioo  9693  ioossicc  9710  ioossico  9713  iocssioo  9714  icossioo  9715  ioossioo  9716  ioof  9722  ioodisj  9744
  Copyright terms: Public domain W3C validator