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

Proof

Step	Hyp	Ref	Expression
1		df-ioo	⊢ (,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) } )
2	1	ixxf	⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ*
3	2	fdmi	⊢ dom (,) = ( ℝ* × ℝ* )
4	3	ndmov	⊢ ( ¬ ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 (,) 𝐵 ) = ∅ )