# Metamath Proof Explorer

## Theorem aean

Description: A conjunction holds almost everywhere if and only if both its terms do. (Contributed by Thierry Arnoux, 20-Oct-2017)

Ref Expression
Hypothesis aean.1 ${⊢}\bigcup \mathrm{dom}{M}={O}$
Assertion aean ${⊢}\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\to \left(\left\{{x}\in {O}|\left({\phi }\wedge {\psi }\right)\right\}{M}\mathrm{-ae.}↔\left(\left\{{x}\in {O}|{\phi }\right\}{M}\mathrm{-ae.}\wedge \left\{{x}\in {O}|{\psi }\right\}{M}\mathrm{-ae.}\right)\right)$

### Proof

Step Hyp Ref Expression
1 aean.1 ${⊢}\bigcup \mathrm{dom}{M}={O}$
2 unrab ${⊢}\left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}=\left\{{x}\in {O}|\left(¬{\phi }\vee ¬{\psi }\right)\right\}$
3 ianor ${⊢}¬\left({\phi }\wedge {\psi }\right)↔\left(¬{\phi }\vee ¬{\psi }\right)$
4 3 rabbii ${⊢}\left\{{x}\in {O}|¬\left({\phi }\wedge {\psi }\right)\right\}=\left\{{x}\in {O}|\left(¬{\phi }\vee ¬{\psi }\right)\right\}$
5 2 4 eqtr4i ${⊢}\left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}=\left\{{x}\in {O}|¬\left({\phi }\wedge {\psi }\right)\right\}$
6 5 fveq2i ${⊢}{M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}\right)={M}\left(\left\{{x}\in {O}|¬\left({\phi }\wedge {\psi }\right)\right\}\right)$
7 6 eqeq1i ${⊢}{M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}\right)=0↔{M}\left(\left\{{x}\in {O}|¬\left({\phi }\wedge {\psi }\right)\right\}\right)=0$
8 measbasedom ${⊢}{M}\in \bigcup \mathrm{ran}\mathrm{measures}↔{M}\in \mathrm{measures}\left(\mathrm{dom}{M}\right)$
9 8 biimpi ${⊢}{M}\in \bigcup \mathrm{ran}\mathrm{measures}\to {M}\in \mathrm{measures}\left(\mathrm{dom}{M}\right)$
10 9 3ad2ant1 ${⊢}\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\to {M}\in \mathrm{measures}\left(\mathrm{dom}{M}\right)$
11 10 adantr ${⊢}\left(\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\wedge {M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}\right)=0\right)\to {M}\in \mathrm{measures}\left(\mathrm{dom}{M}\right)$
12 simp2 ${⊢}\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\to \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}$
13 12 adantr ${⊢}\left(\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\wedge {M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}\right)=0\right)\to \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}$
14 dmmeas ${⊢}{M}\in \bigcup \mathrm{ran}\mathrm{measures}\to \mathrm{dom}{M}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
15 unelsiga ${⊢}\left(\mathrm{dom}{M}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\to \left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}$
16 14 15 syl3an1 ${⊢}\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\to \left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}$
17 ssun1 ${⊢}\left\{{x}\in {O}|¬{\phi }\right\}\subseteq \left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}$
18 17 a1i ${⊢}\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\to \left\{{x}\in {O}|¬{\phi }\right\}\subseteq \left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}$
19 10 12 16 18 measssd ${⊢}\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\to {M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\right)\le {M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}\right)$
20 19 adantr ${⊢}\left(\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\wedge {M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}\right)=0\right)\to {M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\right)\le {M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}\right)$
21 simpr ${⊢}\left(\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\wedge {M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}\right)=0\right)\to {M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}\right)=0$
22 20 21 breqtrd ${⊢}\left(\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\wedge {M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}\right)=0\right)\to {M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\right)\le 0$
23 measle0 ${⊢}\left({M}\in \mathrm{measures}\left(\mathrm{dom}{M}\right)\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge {M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\right)\le 0\right)\to {M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\right)=0$
24 11 13 22 23 syl3anc ${⊢}\left(\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\wedge {M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}\right)=0\right)\to {M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\right)=0$
25 simp3 ${⊢}\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\to \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}$
26 25 adantr ${⊢}\left(\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\wedge {M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}\right)=0\right)\to \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}$
27 ssun2 ${⊢}\left\{{x}\in {O}|¬{\psi }\right\}\subseteq \left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}$
28 27 a1i ${⊢}\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\to \left\{{x}\in {O}|¬{\psi }\right\}\subseteq \left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}$
29 10 25 16 28 measssd ${⊢}\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\to {M}\left(\left\{{x}\in {O}|¬{\psi }\right\}\right)\le {M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}\right)$
30 29 adantr ${⊢}\left(\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\wedge {M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}\right)=0\right)\to {M}\left(\left\{{x}\in {O}|¬{\psi }\right\}\right)\le {M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}\right)$
31 30 21 breqtrd ${⊢}\left(\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\wedge {M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}\right)=0\right)\to {M}\left(\left\{{x}\in {O}|¬{\psi }\right\}\right)\le 0$
32 measle0 ${⊢}\left({M}\in \mathrm{measures}\left(\mathrm{dom}{M}\right)\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\wedge {M}\left(\left\{{x}\in {O}|¬{\psi }\right\}\right)\le 0\right)\to {M}\left(\left\{{x}\in {O}|¬{\psi }\right\}\right)=0$
33 11 26 31 32 syl3anc ${⊢}\left(\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\wedge {M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}\right)=0\right)\to {M}\left(\left\{{x}\in {O}|¬{\psi }\right\}\right)=0$
34 24 33 jca ${⊢}\left(\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\wedge {M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}\right)=0\right)\to \left({M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\right)=0\wedge {M}\left(\left\{{x}\in {O}|¬{\psi }\right\}\right)=0\right)$
35 10 adantr ${⊢}\left(\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\wedge \left({M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\right)=0\wedge {M}\left(\left\{{x}\in {O}|¬{\psi }\right\}\right)=0\right)\right)\to {M}\in \mathrm{measures}\left(\mathrm{dom}{M}\right)$
36 measbase ${⊢}{M}\in \mathrm{measures}\left(\mathrm{dom}{M}\right)\to \mathrm{dom}{M}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
37 35 36 syl ${⊢}\left(\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\wedge \left({M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\right)=0\wedge {M}\left(\left\{{x}\in {O}|¬{\psi }\right\}\right)=0\right)\right)\to \mathrm{dom}{M}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
38 12 adantr ${⊢}\left(\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\wedge \left({M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\right)=0\wedge {M}\left(\left\{{x}\in {O}|¬{\psi }\right\}\right)=0\right)\right)\to \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}$
39 25 adantr ${⊢}\left(\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\wedge \left({M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\right)=0\wedge {M}\left(\left\{{x}\in {O}|¬{\psi }\right\}\right)=0\right)\right)\to \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}$
40 37 38 39 15 syl3anc ${⊢}\left(\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\wedge \left({M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\right)=0\wedge {M}\left(\left\{{x}\in {O}|¬{\psi }\right\}\right)=0\right)\right)\to \left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}$
41 35 38 39 measunl ${⊢}\left(\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\wedge \left({M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\right)=0\wedge {M}\left(\left\{{x}\in {O}|¬{\psi }\right\}\right)=0\right)\right)\to {M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}\right)\le {M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\right){+}_{𝑒}{M}\left(\left\{{x}\in {O}|¬{\psi }\right\}\right)$
42 simprl ${⊢}\left(\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\wedge \left({M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\right)=0\wedge {M}\left(\left\{{x}\in {O}|¬{\psi }\right\}\right)=0\right)\right)\to {M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\right)=0$
43 simprr ${⊢}\left(\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\wedge \left({M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\right)=0\wedge {M}\left(\left\{{x}\in {O}|¬{\psi }\right\}\right)=0\right)\right)\to {M}\left(\left\{{x}\in {O}|¬{\psi }\right\}\right)=0$
44 42 43 oveq12d ${⊢}\left(\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\wedge \left({M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\right)=0\wedge {M}\left(\left\{{x}\in {O}|¬{\psi }\right\}\right)=0\right)\right)\to {M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\right){+}_{𝑒}{M}\left(\left\{{x}\in {O}|¬{\psi }\right\}\right)=0{+}_{𝑒}0$
45 0xr ${⊢}0\in {ℝ}^{*}$
46 xaddid1 ${⊢}0\in {ℝ}^{*}\to 0{+}_{𝑒}0=0$
47 45 46 ax-mp ${⊢}0{+}_{𝑒}0=0$
48 44 47 syl6eq ${⊢}\left(\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\wedge \left({M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\right)=0\wedge {M}\left(\left\{{x}\in {O}|¬{\psi }\right\}\right)=0\right)\right)\to {M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\right){+}_{𝑒}{M}\left(\left\{{x}\in {O}|¬{\psi }\right\}\right)=0$
49 41 48 breqtrd ${⊢}\left(\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\wedge \left({M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\right)=0\wedge {M}\left(\left\{{x}\in {O}|¬{\psi }\right\}\right)=0\right)\right)\to {M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}\right)\le 0$
50 measle0 ${⊢}\left({M}\in \mathrm{measures}\left(\mathrm{dom}{M}\right)\wedge \left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\wedge {M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}\right)\le 0\right)\to {M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}\right)=0$
51 35 40 49 50 syl3anc ${⊢}\left(\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\wedge \left({M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\right)=0\wedge {M}\left(\left\{{x}\in {O}|¬{\psi }\right\}\right)=0\right)\right)\to {M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}\right)=0$
52 34 51 impbida ${⊢}\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\to \left({M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\cup \left\{{x}\in {O}|¬{\psi }\right\}\right)=0↔\left({M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\right)=0\wedge {M}\left(\left\{{x}\in {O}|¬{\psi }\right\}\right)=0\right)\right)$
53 7 52 syl5bbr ${⊢}\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\to \left({M}\left(\left\{{x}\in {O}|¬\left({\phi }\wedge {\psi }\right)\right\}\right)=0↔\left({M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\right)=0\wedge {M}\left(\left\{{x}\in {O}|¬{\psi }\right\}\right)=0\right)\right)$
54 1 braew ${⊢}{M}\in \bigcup \mathrm{ran}\mathrm{measures}\to \left(\left\{{x}\in {O}|\left({\phi }\wedge {\psi }\right)\right\}{M}\mathrm{-ae.}↔{M}\left(\left\{{x}\in {O}|¬\left({\phi }\wedge {\psi }\right)\right\}\right)=0\right)$
55 54 3ad2ant1 ${⊢}\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\to \left(\left\{{x}\in {O}|\left({\phi }\wedge {\psi }\right)\right\}{M}\mathrm{-ae.}↔{M}\left(\left\{{x}\in {O}|¬\left({\phi }\wedge {\psi }\right)\right\}\right)=0\right)$
56 1 braew ${⊢}{M}\in \bigcup \mathrm{ran}\mathrm{measures}\to \left(\left\{{x}\in {O}|{\phi }\right\}{M}\mathrm{-ae.}↔{M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\right)=0\right)$
57 1 braew ${⊢}{M}\in \bigcup \mathrm{ran}\mathrm{measures}\to \left(\left\{{x}\in {O}|{\psi }\right\}{M}\mathrm{-ae.}↔{M}\left(\left\{{x}\in {O}|¬{\psi }\right\}\right)=0\right)$
58 56 57 anbi12d ${⊢}{M}\in \bigcup \mathrm{ran}\mathrm{measures}\to \left(\left(\left\{{x}\in {O}|{\phi }\right\}{M}\mathrm{-ae.}\wedge \left\{{x}\in {O}|{\psi }\right\}{M}\mathrm{-ae.}\right)↔\left({M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\right)=0\wedge {M}\left(\left\{{x}\in {O}|¬{\psi }\right\}\right)=0\right)\right)$
59 58 3ad2ant1 ${⊢}\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\to \left(\left(\left\{{x}\in {O}|{\phi }\right\}{M}\mathrm{-ae.}\wedge \left\{{x}\in {O}|{\psi }\right\}{M}\mathrm{-ae.}\right)↔\left({M}\left(\left\{{x}\in {O}|¬{\phi }\right\}\right)=0\wedge {M}\left(\left\{{x}\in {O}|¬{\psi }\right\}\right)=0\right)\right)$
60 53 55 59 3bitr4d ${⊢}\left({M}\in \bigcup \mathrm{ran}\mathrm{measures}\wedge \left\{{x}\in {O}|¬{\phi }\right\}\in \mathrm{dom}{M}\wedge \left\{{x}\in {O}|¬{\psi }\right\}\in \mathrm{dom}{M}\right)\to \left(\left\{{x}\in {O}|\left({\phi }\wedge {\psi }\right)\right\}{M}\mathrm{-ae.}↔\left(\left\{{x}\in {O}|{\phi }\right\}{M}\mathrm{-ae.}\wedge \left\{{x}\in {O}|{\psi }\right\}{M}\mathrm{-ae.}\right)\right)$