Metamath Proof Explorer

Theorem ixxval

Description: Value of the interval function. (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 ixxval 
|- ( ( A e. RR* /\ B e. RR* ) -> ( A O B ) = { z e. RR* | ( A R z /\ z 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 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 ) } )