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