Description: The domain of the closed-below, open-above interval function. (Contributed by Glauco Siliprandi, 2-Jan-2022)
Ref | Expression | ||
---|---|---|---|
Assertion | dmico | ⊢ dom [,) = ( ℝ* × ℝ* ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ico | ⊢ [,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ) | |
2 | 1 | ixxf | ⊢ [,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ* |
3 | 2 | fdmi | ⊢ dom [,) = ( ℝ* × ℝ* ) |