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 dom 𝑀 = 𝑂
Assertion braew ( 𝑀 ran measures → ( { 𝑥𝑂𝜑 } a.e. 𝑀 ↔ ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜑 } ) = 0 ) )

Proof

Step Hyp Ref Expression
1 braew.1 dom 𝑀 = 𝑂
2 dmexg ( 𝑀 ran measures → dom 𝑀 ∈ V )
3 2 uniexd ( 𝑀 ran measures → dom 𝑀 ∈ V )
4 1 3 eqeltrrid ( 𝑀 ran measures → 𝑂 ∈ V )
5 rabexg ( 𝑂 ∈ V → { 𝑥𝑂𝜑 } ∈ V )
6 4 5 syl ( 𝑀 ran measures → { 𝑥𝑂𝜑 } ∈ V )
7 simpr ( ( 𝑎 = { 𝑥𝑂𝜑 } ∧ 𝑚 = 𝑀 ) → 𝑚 = 𝑀 )
8 7 dmeqd ( ( 𝑎 = { 𝑥𝑂𝜑 } ∧ 𝑚 = 𝑀 ) → dom 𝑚 = dom 𝑀 )
9 8 unieqd ( ( 𝑎 = { 𝑥𝑂𝜑 } ∧ 𝑚 = 𝑀 ) → dom 𝑚 = dom 𝑀 )
10 simpl ( ( 𝑎 = { 𝑥𝑂𝜑 } ∧ 𝑚 = 𝑀 ) → 𝑎 = { 𝑥𝑂𝜑 } )
11 9 10 difeq12d ( ( 𝑎 = { 𝑥𝑂𝜑 } ∧ 𝑚 = 𝑀 ) → ( dom 𝑚𝑎 ) = ( dom 𝑀 ∖ { 𝑥𝑂𝜑 } ) )
12 7 11 fveq12d ( ( 𝑎 = { 𝑥𝑂𝜑 } ∧ 𝑚 = 𝑀 ) → ( 𝑚 ‘ ( dom 𝑚𝑎 ) ) = ( 𝑀 ‘ ( dom 𝑀 ∖ { 𝑥𝑂𝜑 } ) ) )
13 12 eqeq1d ( ( 𝑎 = { 𝑥𝑂𝜑 } ∧ 𝑚 = 𝑀 ) → ( ( 𝑚 ‘ ( dom 𝑚𝑎 ) ) = 0 ↔ ( 𝑀 ‘ ( dom 𝑀 ∖ { 𝑥𝑂𝜑 } ) ) = 0 ) )
14 df-ae a.e. = { ⟨ 𝑎 , 𝑚 ⟩ ∣ ( 𝑚 ‘ ( dom 𝑚𝑎 ) ) = 0 }
15 13 14 brabga ( ( { 𝑥𝑂𝜑 } ∈ V ∧ 𝑀 ran measures ) → ( { 𝑥𝑂𝜑 } a.e. 𝑀 ↔ ( 𝑀 ‘ ( dom 𝑀 ∖ { 𝑥𝑂𝜑 } ) ) = 0 ) )
16 6 15 mpancom ( 𝑀 ran measures → ( { 𝑥𝑂𝜑 } a.e. 𝑀 ↔ ( 𝑀 ‘ ( dom 𝑀 ∖ { 𝑥𝑂𝜑 } ) ) = 0 ) )
17 1 difeq1i ( dom 𝑀 ∖ { 𝑥𝑂𝜑 } ) = ( 𝑂 ∖ { 𝑥𝑂𝜑 } )
18 notrab ( 𝑂 ∖ { 𝑥𝑂𝜑 } ) = { 𝑥𝑂 ∣ ¬ 𝜑 }
19 17 18 eqtri ( dom 𝑀 ∖ { 𝑥𝑂𝜑 } ) = { 𝑥𝑂 ∣ ¬ 𝜑 }
20 19 fveq2i ( 𝑀 ‘ ( dom 𝑀 ∖ { 𝑥𝑂𝜑 } ) ) = ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜑 } )
21 20 eqeq1i ( ( 𝑀 ‘ ( dom 𝑀 ∖ { 𝑥𝑂𝜑 } ) ) = 0 ↔ ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜑 } ) = 0 )
22 16 21 syl6bb ( 𝑀 ran measures → ( { 𝑥𝑂𝜑 } a.e. 𝑀 ↔ ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜑 } ) = 0 ) )