Metamath Proof Explorer


Theorem elixx1

Description: Membership in an interval of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013)

Ref Expression
Hypothesis ixx.1
|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )
Assertion elixx1
|- ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A O B ) <-> ( C e. RR* /\ A R C /\ C S B ) ) )

Proof

Step Hyp Ref Expression
1 ixx.1
 |-  O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )
2 1 ixxval
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A O B ) = { z e. RR* | ( A R z /\ z S B ) } )
3 2 eleq2d
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A O B ) <-> C e. { z e. RR* | ( A R z /\ z S B ) } ) )
4 breq2
 |-  ( z = C -> ( A R z <-> A R C ) )
5 breq1
 |-  ( z = C -> ( z S B <-> C S B ) )
6 4 5 anbi12d
 |-  ( z = C -> ( ( A R z /\ z S B ) <-> ( A R C /\ C S B ) ) )
7 6 elrab
 |-  ( C e. { z e. RR* | ( A R z /\ z S B ) } <-> ( C e. RR* /\ ( A R C /\ C S B ) ) )
8 3anass
 |-  ( ( C e. RR* /\ A R C /\ C S B ) <-> ( C e. RR* /\ ( A R C /\ C S B ) ) )
9 7 8 bitr4i
 |-  ( C e. { z e. RR* | ( A R z /\ z S B ) } <-> ( C e. RR* /\ A R C /\ C S B ) )
10 3 9 bitrdi
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A O B ) <-> ( C e. RR* /\ A R C /\ C S B ) ) )