Theorem dmico

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

	Ref	Expression
Assertion	dmico	$$⊢\mathrm{dom}\left[.\right)={ℝ}^{*}\times {ℝ}^{*}$$

Proof

Step	Hyp	Ref	Expression
1		df-ico	$$⊢\left[.\right)=\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}\right)$$
2	1	ixxf	$$⊢\left[.\right):{ℝ}^{*}\times {ℝ}^{*}⟶𝒫{ℝ}^{*}$$
3	2	fdmi	$$⊢\mathrm{dom}\left[.\right)={ℝ}^{*}\times {ℝ}^{*}$$