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 V M ran measures R ~ae M = f g | f dom R dom M g dom R dom M x dom M | f x R g x M-ae.

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 dom m = dom M
6 2 5 oveq12d r = R m = M dom r dom m = dom R dom M
7 6 eleq2d r = R m = M f dom r dom m f dom R dom M
8 6 eleq2d r = R m = M g dom r dom m g dom R dom M
9 7 8 anbi12d r = R m = M f dom r dom m g dom r dom m f dom R dom M g dom R 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 dom m | f x r g x = x dom M | f x R g x
12 11 3 breq12d r = R m = M x dom m | f x r g x m-ae. x dom M | f x R g x M-ae.
13 9 12 anbi12d r = R m = M f dom r dom m g dom r dom m x dom m | f x r g x m-ae. f dom R dom M g dom R dom M x dom M | f x R g x M-ae.
14 13 opabbidv r = R m = M f g | f dom r dom m g dom r dom m x dom m | f x r g x m-ae. = f g | f dom R dom M g dom R dom M x dom M | f x R g x M-ae.
15 df-fae ~ae = r V , m ran measures f g | f dom r dom m g dom r dom m x dom m | f x r g x m-ae.
16 ovex dom R dom M V
17 16 16 xpex dom R dom M × dom R dom M V
18 opabssxp f g | f dom R dom M g dom R dom M x dom M | f x R g x M-ae. dom R dom M × dom R dom M
19 17 18 ssexi f g | f dom R dom M g dom R dom M x dom M | f x R g x M-ae. V
20 14 15 19 ovmpoa R V M ran measures R ~ae M = f g | f dom R dom M g dom R dom M x dom M | f x R g x M-ae.