| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ixx.1 |
|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } ) |
| 2 |
|
breq1 |
|- ( x = A -> ( x R z <-> A R z ) ) |
| 3 |
2
|
anbi1d |
|- ( x = A -> ( ( x R z /\ z S y ) <-> ( A R z /\ z S y ) ) ) |
| 4 |
3
|
rabbidv |
|- ( x = A -> { z e. RR* | ( x R z /\ z S y ) } = { z e. RR* | ( A R z /\ z S y ) } ) |
| 5 |
|
breq2 |
|- ( y = B -> ( z S y <-> z S B ) ) |
| 6 |
5
|
anbi2d |
|- ( y = B -> ( ( A R z /\ z S y ) <-> ( A R z /\ z S B ) ) ) |
| 7 |
6
|
rabbidv |
|- ( y = B -> { z e. RR* | ( A R z /\ z S y ) } = { z e. RR* | ( A R z /\ z S B ) } ) |
| 8 |
|
xrex |
|- RR* e. _V |
| 9 |
8
|
rabex |
|- { z e. RR* | ( A R z /\ z S B ) } e. _V |
| 10 |
4 7 1 9
|
ovmpo |
|- ( ( A e. RR* /\ B e. RR* ) -> ( A O B ) = { z e. RR* | ( A R z /\ z S B ) } ) |