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

Definition df-ioo 9891
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 9887 . 2  class  (,)
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cxr 7990 . . 3  class  RR*
52cv 1352 . . . . . 6  class  x
6 vz . . . . . . 7  setvar  z
76cv 1352 . . . . . 6  class  z
8 clt 7991 . . . . . 6  class  <
95, 7, 8wbr 4003 . . . . 5  wff  x  < 
z
103cv 1352 . . . . . 6  class  y
117, 10, 8wbr 4003 . . . . 5  wff  z  < 
y
129, 11wa 104 . . . 4  wff  ( x  <  z  /\  z  <  y )
1312, 6, 4crab 2459 . . 3  class  { z  e.  RR*  |  (
x  <  z  /\  z  <  y ) }
142, 3, 4, 4, 13cmpo 5876 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  < 
y ) } )
151, 14wceq 1353 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  9906  iooval  9907  elioo3g  9909  elioo1  9910  iooss1  9915  iooss2  9916  eliooxr  9926  iccssioo  9941  ioossicc  9958  ioossico  9961  iocssioo  9962  icossioo  9963  ioossioo  9964  ioof  9970  ioodisj  9992
  Copyright terms: Public domain W3C validator