Theorem relfae

Description: The 'almost everywhere' builder for functions produces relations. (Contributed by Thierry Arnoux, 22-Oct-2017)

	Ref	Expression
Assertion	relfae	|- ( ( R e. _V /\ M e. U. ran measures ) -> Rel ( R ~ae M ) )

Proof

Step	Hyp	Ref	Expression
1		relopabv	|- Rel { <. 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 ) }
2		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 ) } )
3	2	releqd	|- ( ( R e. _V /\ M e. U. ran measures ) -> ( Rel ( R ~ae M ) <-> Rel { <. 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 ) } ) )
4	1 3	mpbiri	|- ( ( R e. _V /\ M e. U. ran measures ) -> Rel ( R ~ae M ) )