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 [,) = ( ℝ* × ℝ* )