Theorem ndmico

Description: The closed-below, open-above interval function's value is empty outside of its domain. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Assertion	ndmico	$$⊢\neg \left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left[A,B\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		dmico	$$⊢\mathrm{dom}\left[.\right)={ℝ}^{*}\times {ℝ}^{*}$$
2	1	ndmov	$$⊢\neg \left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left[A,B\right)=\varnothing$$