Metamath Proof Explorer


Theorem ndmico

Description: The closed-below, open-above interval function's value is empty outside of its domain. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Assertion ndmico
|- ( -. ( A e. RR* /\ B e. RR* ) -> ( A [,) B ) = (/) )

Proof

Step Hyp Ref Expression
1 dmico
 |-  dom [,) = ( RR* X. RR* )
2 1 ndmov
 |-  ( -. ( A e. RR* /\ B e. RR* ) -> ( A [,) B ) = (/) )