Description: The set of closed intervals of extended reals maps to subsets of extended reals. (Contributed by FL, 14-Jun-2007) (Revised by Mario Carneiro, 3-Nov-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | iccf | |- [,] : ( RR* X. RR* ) --> ~P RR* |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-icc | |- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } ) |
|
| 2 | 1 | ixxf | |- [,] : ( RR* X. RR* ) --> ~P RR* |