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 [,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } )
2 1 ixxf [,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ*
3 2 fdmi dom [,) = ( ℝ* × ℝ* )