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