This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )