Metamath Proof Explorer

Theorem faeval

Description: Value of the 'almost everywhere' relation for a given relation and measure. (Contributed by Thierry Arnoux, 22-Oct-2017)

Ref Expression
Assertion faeval 
|- ( ( R e. _V /\ M e. U. ran measures ) -> ( R ~ae M ) = { <. f , g >. | ( ( f e. ( dom R ^m U. dom M ) /\ g e. ( dom R ^m U. dom M ) ) /\ { x e. U. dom M | ( f ` x ) R ( g ` x ) } ae M ) } )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( r = R /\ m = M ) -> r = R )
2 1 dmeqd 
 |-  ( ( r = R /\ m = M ) -> dom r = dom R )
3 simpr 
 |-  ( ( r = R /\ m = M ) -> m = M )
4 3 dmeqd 
 |-  ( ( r = R /\ m = M ) -> dom m = dom M )
5 4 unieqd 
 |-  ( ( r = R /\ m = M ) -> U. dom m = U. dom M )
6 2 5 oveq12d 
 |-  ( ( r = R /\ m = M ) -> ( dom r ^m U. dom m ) = ( dom R ^m U. dom M ) )
7 6 eleq2d 
 |-  ( ( r = R /\ m = M ) -> ( f e. ( dom r ^m U. dom m ) <-> f e. ( dom R ^m U. dom M ) ) )
8 6 eleq2d 
 |-  ( ( r = R /\ m = M ) -> ( g e. ( dom r ^m U. dom m ) <-> g e. ( dom R ^m U. dom M ) ) )
9 7 8 anbi12d 
 |-  ( ( r = R /\ m = M ) -> ( ( f e. ( dom r ^m U. dom m ) /\ g e. ( dom r ^m U. dom m ) ) <-> ( f e. ( dom R ^m U. dom M ) /\ g e. ( dom R ^m U. dom M ) ) ) )
10 1 breqd 
 |-  ( ( r = R /\ m = M ) -> ( ( f ` x ) r ( g ` x ) <-> ( f ` x ) R ( g ` x ) ) )
11 5 10 rabeqbidv 
 |-  ( ( r = R /\ m = M ) -> { x e. U. dom m | ( f ` x ) r ( g ` x ) } = { x e. U. dom M | ( f ` x ) R ( g ` x ) } )
12 11 3 breq12d 
 |-  ( ( r = R /\ m = M ) -> ( { x e. U. dom m | ( f ` x ) r ( g ` x ) } ae m <-> { x e. U. dom M | ( f ` x ) R ( g ` x ) } ae M ) )
13 9 12 anbi12d 
 |-  ( ( r = R /\ m = M ) -> ( ( ( f e. ( dom r ^m U. dom m ) /\ g e. ( dom r ^m U. dom m ) ) /\ { x e. U. dom m | ( f ` x ) r ( g ` x ) } ae m ) <-> ( ( f e. ( dom R ^m U. dom M ) /\ g e. ( dom R ^m U. dom M ) ) /\ { x e. U. dom M | ( f ` x ) R ( g ` x ) } ae M ) ) )
14 13 opabbidv 
 |-  ( ( r = R /\ m = M ) -> { <. f , g >. | ( ( f e. ( dom r ^m U. dom m ) /\ g e. ( dom r ^m U. dom m ) ) /\ { x e. U. dom m | ( f ` x ) r ( g ` x ) } ae m ) } = { <. f , g >. | ( ( f e. ( dom R ^m U. dom M ) /\ g e. ( dom R ^m U. dom M ) ) /\ { x e. U. dom M | ( f ` x ) R ( g ` x ) } ae M ) } )
15 df-fae 
 |-  ~ae = ( r e. _V , m e. U. ran measures |-> { <. f , g >. | ( ( f e. ( dom r ^m U. dom m ) /\ g e. ( dom r ^m U. dom m ) ) /\ { x e. U. dom m | ( f ` x ) r ( g ` x ) } ae m ) } )
16 ovex 
 |-  ( dom R ^m U. dom M ) e. _V
17 16 16 xpex 
 |-  ( ( dom R ^m U. dom M ) X. ( dom R ^m U. dom M ) ) e. _V
18 opabssxp 
 |-  { <. f , g >. | ( ( f e. ( dom R ^m U. dom M ) /\ g e. ( dom R ^m U. dom M ) ) /\ { x e. U. dom M | ( f ` x ) R ( g ` x ) } ae M ) } C_ ( ( dom R ^m U. dom M ) X. ( dom R ^m U. dom M ) )
19 17 18 ssexi 
 |-  { <. f , g >. | ( ( f e. ( dom R ^m U. dom M ) /\ g e. ( dom R ^m U. dom M ) ) /\ { x e. U. dom M | ( f ` x ) R ( g ` x ) } ae M ) } e. _V
20 14 15 19 ovmpoa 
 |-  ( ( R e. _V /\ M e. U. ran measures ) -> ( R ~ae M ) = { <. f , g >. | ( ( f e. ( dom R ^m U. dom M ) /\ g e. ( dom R ^m U. dom M ) ) /\ { x e. U. dom M | ( f ` x ) R ( g ` x ) } ae M ) } )