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