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

Definition df-ico 9924
Description: Define the set of closed-below, open-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
Assertion
Ref Expression
df-ico  |-  [,)  =  ( 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-ico
StepHypRef Expression
1 cico 9920 . 2  class  [,)
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cxr 8021 . . 3  class  RR*
52cv 1363 . . . . . 6  class  x
6 vz . . . . . . 7  setvar  z
76cv 1363 . . . . . 6  class  z
8 cle 8023 . . . . . 6  class  <_
95, 7, 8wbr 4018 . . . . 5  wff  x  <_ 
z
103cv 1363 . . . . . 6  class  y
11 clt 8022 . . . . . 6  class  <
127, 10, 11wbr 4018 . . . . 5  wff  z  < 
y
139, 12wa 104 . . . 4  wff  ( x  <_  z  /\  z  <  y )
1413, 6, 4crab 2472 . . 3  class  { z  e.  RR*  |  (
x  <_  z  /\  z  <  y ) }
152, 3, 4, 4, 14cmpo 5898 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  < 
y ) } )
161, 15wceq 1364 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:  icoval  9949  elico1  9953  icossico  9973  iccssico  9975  iccssico2  9977  icossxr  9988  icossicc  9990  ioossico  9992  icossioo  9994  elicore  10297
  Copyright terms: Public domain W3C validator