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 . = * × *

Proof

Step Hyp Ref Expression
1 df-ico . = x * , y * z * | x z z < y
2 1 ixxf . : * × * 𝒫 *
3 2 fdmi dom . = * × *