Description: The open interval function's value is empty outside of its domain. (Contributed by NM, 21-Jun-2007) (Revised by Mario Carneiro, 28-Apr-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ndmioo | |- ( -. ( A e. RR* /\ B e. RR* ) -> ( A (,) B ) = (/) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-ioo | |- (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } ) |
|
| 2 | 1 | ixxf | |- (,) : ( RR* X. RR* ) --> ~P RR* |
| 3 | 2 | fdmi | |- dom (,) = ( RR* X. RR* ) |
| 4 | 3 | ndmov | |- ( -. ( A e. RR* /\ B e. RR* ) -> ( A (,) B ) = (/) ) |