Metamath Proof Explorer

Theorem ixxin

Description: Intersection of two intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013)

Ref Expression
Hypotheses ixx.1 
|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )
ixxin.2 
|- ( ( A e. RR* /\ C e. RR* /\ z e. RR* ) -> ( if ( A <_ C , C , A ) R z <-> ( A R z /\ C R z ) ) )
ixxin.3 
|- ( ( z e. RR* /\ B e. RR* /\ D e. RR* ) -> ( z S if ( B <_ D , B , D ) <-> ( z S B /\ z S D ) ) )
Assertion ixxin 
|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) -> ( ( A O B ) i^i ( C O D ) ) = ( if ( A <_ C , C , A ) O if ( B <_ D , B , D ) ) )

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 ixxin.2 
 |-  ( ( A e. RR* /\ C e. RR* /\ z e. RR* ) -> ( if ( A <_ C , C , A ) R z <-> ( A R z /\ C R z ) ) )
3 ixxin.3 
 |-  ( ( z e. RR* /\ B e. RR* /\ D e. RR* ) -> ( z S if ( B <_ D , B , D ) <-> ( z S B /\ z S D ) ) )
4 inrab 
 |-  ( { z e. RR* | ( A R z /\ z S B ) } i^i { z e. RR* | ( C R z /\ z S D ) } ) = { z e. RR* | ( ( A R z /\ z S B ) /\ ( C R z /\ z S D ) ) }
5 1 ixxval 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A O B ) = { z e. RR* | ( A R z /\ z S B ) } )
6 1 ixxval 
 |-  ( ( C e. RR* /\ D e. RR* ) -> ( C O D ) = { z e. RR* | ( C R z /\ z S D ) } )
7 5 6 ineqan12d 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) -> ( ( A O B ) i^i ( C O D ) ) = ( { z e. RR* | ( A R z /\ z S B ) } i^i { z e. RR* | ( C R z /\ z S D ) } ) )
8 2 ad4ant124 
 |-  ( ( ( ( A e. RR* /\ C e. RR* ) /\ ( B e. RR* /\ D e. RR* ) ) /\ z e. RR* ) -> ( if ( A <_ C , C , A ) R z <-> ( A R z /\ C R z ) ) )
9 3 3expb 
 |-  ( ( z e. RR* /\ ( B e. RR* /\ D e. RR* ) ) -> ( z S if ( B <_ D , B , D ) <-> ( z S B /\ z S D ) ) )
10 9 ancoms 
 |-  ( ( ( B e. RR* /\ D e. RR* ) /\ z e. RR* ) -> ( z S if ( B <_ D , B , D ) <-> ( z S B /\ z S D ) ) )
11 10 adantll 
 |-  ( ( ( ( A e. RR* /\ C e. RR* ) /\ ( B e. RR* /\ D e. RR* ) ) /\ z e. RR* ) -> ( z S if ( B <_ D , B , D ) <-> ( z S B /\ z S D ) ) )
12 8 11 anbi12d 
 |-  ( ( ( ( A e. RR* /\ C e. RR* ) /\ ( B e. RR* /\ D e. RR* ) ) /\ z e. RR* ) -> ( ( if ( A <_ C , C , A ) R z /\ z S if ( B <_ D , B , D ) ) <-> ( ( A R z /\ C R z ) /\ ( z S B /\ z S D ) ) ) )
13 an4 
 |-  ( ( ( A R z /\ z S B ) /\ ( C R z /\ z S D ) ) <-> ( ( A R z /\ C R z ) /\ ( z S B /\ z S D ) ) )
14 12 13 bitr4di 
 |-  ( ( ( ( A e. RR* /\ C e. RR* ) /\ ( B e. RR* /\ D e. RR* ) ) /\ z e. RR* ) -> ( ( if ( A <_ C , C , A ) R z /\ z S if ( B <_ D , B , D ) ) <-> ( ( A R z /\ z S B ) /\ ( C R z /\ z S D ) ) ) )
15 14 rabbidva 
 |-  ( ( ( A e. RR* /\ C e. RR* ) /\ ( B e. RR* /\ D e. RR* ) ) -> { z e. RR* | ( if ( A <_ C , C , A ) R z /\ z S if ( B <_ D , B , D ) ) } = { z e. RR* | ( ( A R z /\ z S B ) /\ ( C R z /\ z S D ) ) } )
16 15 an4s 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) -> { z e. RR* | ( if ( A <_ C , C , A ) R z /\ z S if ( B <_ D , B , D ) ) } = { z e. RR* | ( ( A R z /\ z S B ) /\ ( C R z /\ z S D ) ) } )
17 4 7 16 3eqtr4a 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) -> ( ( A O B ) i^i ( C O D ) ) = { z e. RR* | ( if ( A <_ C , C , A ) R z /\ z S if ( B <_ D , B , D ) ) } )
18 ifcl 
 |-  ( ( C e. RR* /\ A e. RR* ) -> if ( A <_ C , C , A ) e. RR* )
19 18 ancoms 
 |-  ( ( A e. RR* /\ C e. RR* ) -> if ( A <_ C , C , A ) e. RR* )
20 ifcl 
 |-  ( ( B e. RR* /\ D e. RR* ) -> if ( B <_ D , B , D ) e. RR* )
21 1 ixxval 
 |-  ( ( if ( A <_ C , C , A ) e. RR* /\ if ( B <_ D , B , D ) e. RR* ) -> ( if ( A <_ C , C , A ) O if ( B <_ D , B , D ) ) = { z e. RR* | ( if ( A <_ C , C , A ) R z /\ z S if ( B <_ D , B , D ) ) } )
22 19 20 21 syl2an 
 |-  ( ( ( A e. RR* /\ C e. RR* ) /\ ( B e. RR* /\ D e. RR* ) ) -> ( if ( A <_ C , C , A ) O if ( B <_ D , B , D ) ) = { z e. RR* | ( if ( A <_ C , C , A ) R z /\ z S if ( B <_ D , B , D ) ) } )
23 22 an4s 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) -> ( if ( A <_ C , C , A ) O if ( B <_ D , B , D ) ) = { z e. RR* | ( if ( A <_ C , C , A ) R z /\ z S if ( B <_ D , B , D ) ) } )
24 17 23 eqtr4d 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) -> ( ( A O B ) i^i ( C O D ) ) = ( if ( A <_ C , C , A ) O if ( B <_ D , B , D ) ) )