Theorem elioo4g

Description: Membership in an open interval of extended reals. (Contributed by NM, 8-Jun-2007) (Revised by Mario Carneiro, 28-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		eliooxr	|- ( C e. ( A (,) B ) -> ( A e. RR* /\ B e. RR* ) )
2		elioore	|- ( C e. ( A (,) B ) -> C e. RR )
3	1 2	jca	|- ( C e. ( A (,) B ) -> ( ( A e. RR* /\ B e. RR* ) /\ C e. RR ) )
4		df-3an	|- ( ( A e. RR* /\ B e. RR* /\ C e. RR ) <-> ( ( A e. RR* /\ B e. RR* ) /\ C e. RR ) )
5	3 4	sylibr	|- ( C e. ( A (,) B ) -> ( A e. RR* /\ B e. RR* /\ C e. RR ) )
6		eliooord	|- ( C e. ( A (,) B ) -> ( A < C /\ C < B ) )
7	5 6	jca	|- ( C e. ( A (,) B ) -> ( ( A e. RR* /\ B e. RR* /\ C e. RR ) /\ ( A < C /\ C < B ) ) )
8		rexr	|- ( C e. RR -> C e. RR* )
9	8	3anim3i	|- ( ( A e. RR* /\ B e. RR* /\ C e. RR ) -> ( A e. RR* /\ B e. RR* /\ C e. RR* ) )
10	9	anim1i	|- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR ) /\ ( A < C /\ C < B ) ) -> ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < C /\ C < B ) ) )
11		elioo3g	|- ( C e. ( A (,) B ) <-> ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < C /\ C < B ) ) )
12	10 11	sylibr	|- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR ) /\ ( A < C /\ C < B ) ) -> C e. ( A (,) B ) )
13	7 12	impbii	|- ( C e. ( A (,) B ) <-> ( ( A e. RR* /\ B e. RR* /\ C e. RR ) /\ ( A < C /\ C < B ) ) )