Metamath Proof Explorer

Theorem elixx3g

Description: Membership in a set of open intervals of extended reals. We use the fact that an operation's value is empty outside of its domain to show A e. RR* and B e. RR* . (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 elixx3g 
|- ( C e. ( A O B ) <-> ( ( A e. RR* /\ B e. RR* /\ 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 anass 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( A R C /\ C S B ) ) <-> ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ ( A R C /\ C S B ) ) ) )
3 df-3an 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) <-> ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) )
4 3 anbi1i 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A R C /\ C S B ) ) <-> ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( A R C /\ C S B ) ) )
5 1 elixx1 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A O B ) <-> ( C e. RR* /\ A R C /\ C S B ) ) )
6 3anass 
 |-  ( ( C e. RR* /\ A R C /\ C S B ) <-> ( C e. RR* /\ ( A R C /\ C S B ) ) )
7 ibar 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( C e. RR* /\ ( A R C /\ C S B ) ) <-> ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ ( A R C /\ C S B ) ) ) ) )
8 6 7 syl5bb 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( C e. RR* /\ A R C /\ C S B ) <-> ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ ( A R C /\ C S B ) ) ) ) )
9 5 8 bitrd 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A O B ) <-> ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ ( A R C /\ C S B ) ) ) ) )
10 1 ixxf 
 |-  O : ( RR* X. RR* ) --> ~P RR*
11 10 fdmi 
 |-  dom O = ( RR* X. RR* )
12 11 ndmov 
 |-  ( -. ( A e. RR* /\ B e. RR* ) -> ( A O B ) = (/) )
13 12 eleq2d 
 |-  ( -. ( A e. RR* /\ B e. RR* ) -> ( C e. ( A O B ) <-> C e. (/) ) )
14 noel 
 |-  -. C e. (/)
15 14 pm2.21i 
 |-  ( C e. (/) -> ( A e. RR* /\ B e. RR* ) )
16 simpl 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ ( A R C /\ C S B ) ) ) -> ( A e. RR* /\ B e. RR* ) )
17 15 16 pm5.21ni 
 |-  ( -. ( A e. RR* /\ B e. RR* ) -> ( C e. (/) <-> ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ ( A R C /\ C S B ) ) ) ) )
18 13 17 bitrd 
 |-  ( -. ( A e. RR* /\ B e. RR* ) -> ( C e. ( A O B ) <-> ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ ( A R C /\ C S B ) ) ) ) )
19 9 18 pm2.61i 
 |-  ( C e. ( A O B ) <-> ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ ( A R C /\ C S B ) ) ) )
20 2 4 19 3bitr4ri 
 |-  ( C e. ( A O B ) <-> ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A R C /\ C S B ) ) )