This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 (A \in ℝ^{} \land B \in ℝ^{}) \to (A, B) = \emptyset$

Proof

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