Theorem eliooxr

Description: A nonempty open interval spans an interval of extended reals. (Contributed by NM, 17-Aug-2008)

	Ref	Expression
Assertion	eliooxr	|- ( A e. ( B (,) C ) -> ( B e. RR* /\ C e. RR* ) )

Proof

Step	Hyp	Ref	Expression
1		ne0i	|- ( A e. ( B (,) C ) -> ( B (,) C ) =/= (/) )
2		ndmioo	|- ( -. ( B e. RR* /\ C e. RR* ) -> ( B (,) C ) = (/) )
3	2	necon1ai	|- ( ( B (,) C ) =/= (/) -> ( B e. RR* /\ C e. RR* ) )
4	1 3	syl	|- ( A e. ( B (,) C ) -> ( B e. RR* /\ C e. RR* ) )