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	|- ( ( A e. RR* /\ B e. RR* ) -> ( ( A (,) B ) =/= (/) <-> A < B ) )

Proof

Step	Hyp	Ref	Expression
1		ioo0	|- ( ( A e. RR* /\ B e. RR* ) -> ( ( A (,) B ) = (/) <-> B <_ A ) )
2		xrlenlt	|- ( ( B e. RR* /\ A e. RR* ) -> ( B <_ A <-> -. A < B ) )
3	2	ancoms	|- ( ( A e. RR* /\ B e. RR* ) -> ( B <_ A <-> -. A < B ) )
4	1 3	bitr2d	|- ( ( A e. RR* /\ B e. RR* ) -> ( -. A < B <-> ( A (,) B ) = (/) ) )
5	4	necon1abid	|- ( ( A e. RR* /\ B e. RR* ) -> ( ( A (,) B ) =/= (/) <-> A < B ) )