Metamath Proof Explorer

Theorem dmico

Description: The domain of the closed-below, open-above interval function. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Assertion dmico 
|- dom [,) = ( RR* X. RR* )

Proof

Step Hyp Ref Expression
1 df-ico 
 |-  [,) = ( 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* )