Theorem ioon0

Description: An open interval of extended reals is nonempty iff the lower argument is less than the upper argument. (Contributed by NM, 2-Mar-2007)

	Ref	Expression
Assertion	ioon0	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 (,) 𝐵 ) ≠ ∅ ↔ 𝐴 < 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ioo0	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 (,) 𝐵 ) = ∅ ↔ 𝐵 ≤ 𝐴 ) )
2		xrlenlt	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( 𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵 ) )
3	2	ancoms	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵 ) )
4	1 3	bitr2d	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ¬ 𝐴 < 𝐵 ↔ ( 𝐴 (,) 𝐵 ) = ∅ ) )
5	4	necon1abid	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 (,) 𝐵 ) ≠ ∅ ↔ 𝐴 < 𝐵 ) )