Theorem truae

Description: A truth holds almost everywhere. (Contributed by Thierry Arnoux, 20-Oct-2017)

	Ref	Expression
Hypotheses	truae.1	$$⊢\bigcup \mathrm{dom}M=O$$
	truae.2	$$⊢\phi \to M\in \bigcup \mathrm{ran}\mathrm{measures}$$
	truae.3	$$⊢\phi \to \psi$$
Assertion	truae	$$⊢\phi \to \left\{x\in O|\psi \right\}M\mathrm{-ae.}$$

Proof

Step	Hyp	Ref	Expression
1		truae.1	$$⊢\bigcup \mathrm{dom}M=O$$
2		truae.2	$$⊢\phi \to M\in \bigcup \mathrm{ran}\mathrm{measures}$$
3		truae.3	$$⊢\phi \to \psi$$
4	3	pm2.24d	$$⊢\phi \to \left(\neg \psi \to x\in \varnothing \right)$$
5	4	ralrimivw	$$⊢\phi \to \forall x\in O\left(\neg \psi \to x\in \varnothing \right)$$
6		rabss	$$⊢\left\{x\in O|\neg \psi \right\}\subseteq \varnothing \leftrightarrow \forall x\in O\left(\neg \psi \to x\in \varnothing \right)$$
7	5 6	sylibr	$$⊢\phi \to \left\{x\in O|\neg \psi \right\}\subseteq \varnothing$$
8		ss0	$$⊢\left\{x\in O|\neg \psi \right\}\subseteq \varnothing \to \left\{x\in O|\neg \psi \right\}=\varnothing$$
9	7 8	syl	$$⊢\phi \to \left\{x\in O|\neg \psi \right\}=\varnothing$$
10	9	fveq2d	$$⊢\phi \to M\left(\left\{x\in O|\neg \psi \right\}\right)=M\left(\varnothing \right)$$
11		measbasedom	$$⊢M\in \bigcup \mathrm{ran}\mathrm{measures}\leftrightarrow M\in \mathrm{measures}\left(\mathrm{dom}M\right)$$
12		measvnul	$$⊢M\in \mathrm{measures}\left(\mathrm{dom}M\right)\to M\left(\varnothing \right)=0$$
13	11 12	sylbi	$$⊢M\in \bigcup \mathrm{ran}\mathrm{measures}\to M\left(\varnothing \right)=0$$
14	2 13	syl	$$⊢\phi \to M\left(\varnothing \right)=0$$
15	10 14	eqtrd	$$⊢\phi \to M\left(\left\{x\in O|\neg \psi \right\}\right)=0$$
16	1	braew	$$⊢M\in \bigcup \mathrm{ran}\mathrm{measures}\to \left(\left\{x\in O|\psi \right\}M\mathrm{-ae.}\leftrightarrow M\left(\left\{x\in O|\neg \psi \right\}\right)=0\right)$$
17	2 16	syl	$$⊢\phi \to \left(\left\{x\in O|\psi \right\}M\mathrm{-ae.}\leftrightarrow M\left(\left\{x\in O|\neg \psi \right\}\right)=0\right)$$
18	15 17	mpbird	$$⊢\phi \to \left\{x\in O|\psi \right\}M\mathrm{-ae.}$$