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	$$⊢\bigcup \mathrm{dom}M=O$$
Assertion	braew	$$⊢M\in \bigcup \mathrm{ran}\mathrm{measures}\to \left(\left\{x\in O|\phi \right\}M\mathrm{-ae.}\leftrightarrow M\left(\left\{x\in O|\neg \phi \right\}\right)=0\right)$$

Proof

Step	Hyp	Ref	Expression
1		braew.1	$$⊢\bigcup \mathrm{dom}M=O$$
2		dmexg	$$⊢M\in \bigcup \mathrm{ran}\mathrm{measures}\to \mathrm{dom}M\in \mathrm{V}$$
3	2	uniexd	$$⊢M\in \bigcup \mathrm{ran}\mathrm{measures}\to \bigcup \mathrm{dom}M\in \mathrm{V}$$
4	1 3	eqeltrrid	$$⊢M\in \bigcup \mathrm{ran}\mathrm{measures}\to O\in \mathrm{V}$$
5		rabexg	$$⊢O\in \mathrm{V}\to \left\{x\in O|\phi \right\}\in \mathrm{V}$$
6	4 5	syl	$$⊢M\in \bigcup \mathrm{ran}\mathrm{measures}\to \left\{x\in O|\phi \right\}\in \mathrm{V}$$
7		simpr	$$⊢\left(a=\left\{x\in O|\phi \right\}\wedge m=M\right)\to m=M$$
8	7	dmeqd	$$⊢\left(a=\left\{x\in O|\phi \right\}\wedge m=M\right)\to \mathrm{dom}m=\mathrm{dom}M$$
9	8	unieqd	$$⊢\left(a=\left\{x\in O|\phi \right\}\wedge m=M\right)\to \bigcup \mathrm{dom}m=\bigcup \mathrm{dom}M$$
10		simpl	$$⊢\left(a=\left\{x\in O|\phi \right\}\wedge m=M\right)\to a=\left\{x\in O|\phi \right\}$$
11	9 10	difeq12d	$$⊢\left(a=\left\{x\in O|\phi \right\}\wedge m=M\right)\to \bigcup \mathrm{dom}m\setminus a=\bigcup \mathrm{dom}M\setminus \left\{x\in O|\phi \right\}$$
12	7 11	fveq12d	$$⊢\left(a=\left\{x\in O|\phi \right\}\wedge m=M\right)\to m\left(\bigcup \mathrm{dom}m\setminus a\right)=M\left(\bigcup \mathrm{dom}M\setminus \left\{x\in O|\phi \right\}\right)$$
13	12	eqeq1d	$$⊢\left(a=\left\{x\in O|\phi \right\}\wedge m=M\right)\to \left(m\left(\bigcup \mathrm{dom}m\setminus a\right)=0\leftrightarrow M\left(\bigcup \mathrm{dom}M\setminus \left\{x\in O|\phi \right\}\right)=0\right)$$
14		df-ae	$$⊢\mathrm{ae}=\left\{⟨a,m⟩|m\left(\bigcup \mathrm{dom}m\setminus a\right)=0\right\}$$
15	13 14	brabga	$$⊢\left(\left\{x\in O|\phi \right\}\in \mathrm{V}\wedge M\in \bigcup \mathrm{ran}\mathrm{measures}\right)\to \left(\left\{x\in O|\phi \right\}M\mathrm{-ae.}\leftrightarrow M\left(\bigcup \mathrm{dom}M\setminus \left\{x\in O|\phi \right\}\right)=0\right)$$
16	6 15	mpancom	$$⊢M\in \bigcup \mathrm{ran}\mathrm{measures}\to \left(\left\{x\in O|\phi \right\}M\mathrm{-ae.}\leftrightarrow M\left(\bigcup \mathrm{dom}M\setminus \left\{x\in O|\phi \right\}\right)=0\right)$$
17	1	difeq1i	$$⊢\bigcup \mathrm{dom}M\setminus \left\{x\in O|\phi \right\}=O\setminus \left\{x\in O|\phi \right\}$$
18		notrab	$$⊢O\setminus \left\{x\in O|\phi \right\}=\left\{x\in O|\neg \phi \right\}$$
19	17 18	eqtri	$$⊢\bigcup \mathrm{dom}M\setminus \left\{x\in O|\phi \right\}=\left\{x\in O|\neg \phi \right\}$$
20	19	fveq2i	$$⊢M\left(\bigcup \mathrm{dom}M\setminus \left\{x\in O|\phi \right\}\right)=M\left(\left\{x\in O|\neg \phi \right\}\right)$$
21	20	eqeq1i	$$⊢M\left(\bigcup \mathrm{dom}M\setminus \left\{x\in O|\phi \right\}\right)=0\leftrightarrow M\left(\left\{x\in O|\neg \phi \right\}\right)=0$$
22	16 21	bitrdi	$$⊢M\in \bigcup \mathrm{ran}\mathrm{measures}\to \left(\left\{x\in O|\phi \right\}M\mathrm{-ae.}\leftrightarrow M\left(\left\{x\in O|\neg \phi \right\}\right)=0\right)$$