Theorem ndmioo

Description: The open interval function's value is empty outside of its domain. (Contributed by NM, 21-Jun-2007) (Revised by Mario Carneiro, 28-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		df-ioo	$$⊢\left(.\right)=\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼\left\{z\in {ℝ}^{*}|\left(x<z\wedge z<y\right)\right\}\right)$$
2	1	ixxf	$$⊢\left(.\right):{ℝ}^{*}\times {ℝ}^{*}⟶𝒫{ℝ}^{*}$$
3	2	fdmi	$$⊢\mathrm{dom}\left(.\right)={ℝ}^{*}\times {ℝ}^{*}$$
4	3	ndmov	$$⊢\neg \left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A,B\right)=\varnothing$$