Metamath Proof Explorer

Theorem braew

Description: 'almost everywhere' relation for a measure M and a property ph (Contributed by Thierry Arnoux, 20-Oct-2017)

Ref Expression
Hypothesis braew.1 
|- U. dom M = O
Assertion braew 
|- ( M e. U. ran measures -> ( { x e. O | ph } ae M <-> ( M ` { x e. O | -. ph } ) = 0 ) )

Proof

Step Hyp Ref Expression
1 braew.1 
 |-  U. dom M = O
2 dmexg 
 |-  ( M e. U. ran measures -> dom M e. _V )
3 2 uniexd 
 |-  ( M e. U. ran measures -> U. dom M e. _V )
4 1 3 eqeltrrid 
 |-  ( M e. U. ran measures -> O e. _V )
5 rabexg 
 |-  ( O e. _V -> { x e. O | ph } e. _V )
6 4 5 syl 
 |-  ( M e. U. ran measures -> { x e. O | ph } e. _V )
7 simpr 
 |-  ( ( a = { x e. O | ph } /\ m = M ) -> m = M )
8 7 dmeqd 
 |-  ( ( a = { x e. O | ph } /\ m = M ) -> dom m = dom M )
9 8 unieqd 
 |-  ( ( a = { x e. O | ph } /\ m = M ) -> U. dom m = U. dom M )
10 simpl 
 |-  ( ( a = { x e. O | ph } /\ m = M ) -> a = { x e. O | ph } )
11 9 10 difeq12d 
 |-  ( ( a = { x e. O | ph } /\ m = M ) -> ( U. dom m \ a ) = ( U. dom M \ { x e. O | ph } ) )
12 7 11 fveq12d 
 |-  ( ( a = { x e. O | ph } /\ m = M ) -> ( m ` ( U. dom m \ a ) ) = ( M ` ( U. dom M \ { x e. O | ph } ) ) )
13 12 eqeq1d 
 |-  ( ( a = { x e. O | ph } /\ m = M ) -> ( ( m ` ( U. dom m \ a ) ) = 0 <-> ( M ` ( U. dom M \ { x e. O | ph } ) ) = 0 ) )
14 df-ae 
 |-  ae = { <. a , m >. | ( m ` ( U. dom m \ a ) ) = 0 }
15 13 14 brabga 
 |-  ( ( { x e. O | ph } e. _V /\ M e. U. ran measures ) -> ( { x e. O | ph } ae M <-> ( M ` ( U. dom M \ { x e. O | ph } ) ) = 0 ) )
16 6 15 mpancom 
 |-  ( M e. U. ran measures -> ( { x e. O | ph } ae M <-> ( M ` ( U. dom M \ { x e. O | ph } ) ) = 0 ) )
17 1 difeq1i 
 |-  ( U. dom M \ { x e. O | ph } ) = ( O \ { x e. O | ph } )
18 notrab 
 |-  ( O \ { x e. O | ph } ) = { x e. O | -. ph }
19 17 18 eqtri 
 |-  ( U. dom M \ { x e. O | ph } ) = { x e. O | -. ph }
20 19 fveq2i 
 |-  ( M ` ( U. dom M \ { x e. O | ph } ) ) = ( M ` { x e. O | -. ph } )
21 20 eqeq1i 
 |-  ( ( M ` ( U. dom M \ { x e. O | ph } ) ) = 0 <-> ( M ` { x e. O | -. ph } ) = 0 )
22 16 21 bitrdi 
 |-  ( M e. U. ran measures -> ( { x e. O | ph } ae M <-> ( M ` { x e. O | -. ph } ) = 0 ) )