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	⊢ ( ¬ ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 [,) 𝐵 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		dmico	⊢ dom [,) = ( ℝ* × ℝ* )
2	1	ndmov	⊢ ( ¬ ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 [,) 𝐵 ) = ∅ )