# 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 dom 𝑀 = 𝑂
Assertion aean ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) → ( { 𝑥𝑂 ∣ ( 𝜑𝜓 ) } a.e. 𝑀 ↔ ( { 𝑥𝑂𝜑 } a.e. 𝑀 ∧ { 𝑥𝑂𝜓 } a.e. 𝑀 ) ) )

### Proof

Step Hyp Ref Expression
1 aean.1 dom 𝑀 = 𝑂
2 unrab ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } ) = { 𝑥𝑂 ∣ ( ¬ 𝜑 ∨ ¬ 𝜓 ) }
3 ianor ( ¬ ( 𝜑𝜓 ) ↔ ( ¬ 𝜑 ∨ ¬ 𝜓 ) )
4 3 rabbii { 𝑥𝑂 ∣ ¬ ( 𝜑𝜓 ) } = { 𝑥𝑂 ∣ ( ¬ 𝜑 ∨ ¬ 𝜓 ) }
5 2 4 eqtr4i ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } ) = { 𝑥𝑂 ∣ ¬ ( 𝜑𝜓 ) }
6 5 fveq2i ( 𝑀 ‘ ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ) = ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ ( 𝜑𝜓 ) } )
7 6 eqeq1i ( ( 𝑀 ‘ ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ) = 0 ↔ ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ ( 𝜑𝜓 ) } ) = 0 )
8 measbasedom ( 𝑀 ran measures ↔ 𝑀 ∈ ( measures ‘ dom 𝑀 ) )
9 8 biimpi ( 𝑀 ran measures → 𝑀 ∈ ( measures ‘ dom 𝑀 ) )
10 9 3ad2ant1 ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) → 𝑀 ∈ ( measures ‘ dom 𝑀 ) )
11 10 adantr ( ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) ∧ ( 𝑀 ‘ ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ) = 0 ) → 𝑀 ∈ ( measures ‘ dom 𝑀 ) )
12 simp2 ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) → { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 )
13 12 adantr ( ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) ∧ ( 𝑀 ‘ ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ) = 0 ) → { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 )
14 dmmeas ( 𝑀 ran measures → dom 𝑀 ran sigAlgebra )
15 unelsiga ( ( dom 𝑀 ran sigAlgebra ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) → ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ∈ dom 𝑀 )
16 14 15 syl3an1 ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) → ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ∈ dom 𝑀 )
17 ssun1 { 𝑥𝑂 ∣ ¬ 𝜑 } ⊆ ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } )
18 17 a1i ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) → { 𝑥𝑂 ∣ ¬ 𝜑 } ⊆ ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } ) )
19 10 12 16 18 measssd ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) → ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜑 } ) ≤ ( 𝑀 ‘ ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ) )
20 19 adantr ( ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) ∧ ( 𝑀 ‘ ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ) = 0 ) → ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜑 } ) ≤ ( 𝑀 ‘ ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ) )
21 simpr ( ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) ∧ ( 𝑀 ‘ ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ) = 0 ) → ( 𝑀 ‘ ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ) = 0 )
22 20 21 breqtrd ( ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) ∧ ( 𝑀 ‘ ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ) = 0 ) → ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜑 } ) ≤ 0 )
23 measle0 ( ( 𝑀 ∈ ( measures ‘ dom 𝑀 ) ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜑 } ) ≤ 0 ) → ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜑 } ) = 0 )
24 11 13 22 23 syl3anc ( ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) ∧ ( 𝑀 ‘ ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ) = 0 ) → ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜑 } ) = 0 )
25 simp3 ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) → { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 )
26 25 adantr ( ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) ∧ ( 𝑀 ‘ ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ) = 0 ) → { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 )
27 ssun2 { 𝑥𝑂 ∣ ¬ 𝜓 } ⊆ ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } )
28 27 a1i ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) → { 𝑥𝑂 ∣ ¬ 𝜓 } ⊆ ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } ) )
29 10 25 16 28 measssd ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) → ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ≤ ( 𝑀 ‘ ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ) )
30 29 adantr ( ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) ∧ ( 𝑀 ‘ ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ) = 0 ) → ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ≤ ( 𝑀 ‘ ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ) )
31 30 21 breqtrd ( ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) ∧ ( 𝑀 ‘ ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ) = 0 ) → ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ≤ 0 )
32 measle0 ( ( 𝑀 ∈ ( measures ‘ dom 𝑀 ) ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ∧ ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ≤ 0 ) → ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜓 } ) = 0 )
33 11 26 31 32 syl3anc ( ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) ∧ ( 𝑀 ‘ ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ) = 0 ) → ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜓 } ) = 0 )
34 24 33 jca ( ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) ∧ ( 𝑀 ‘ ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ) = 0 ) → ( ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜑 } ) = 0 ∧ ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜓 } ) = 0 ) )
35 10 adantr ( ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) ∧ ( ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜑 } ) = 0 ∧ ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜓 } ) = 0 ) ) → 𝑀 ∈ ( measures ‘ dom 𝑀 ) )
36 measbase ( 𝑀 ∈ ( measures ‘ dom 𝑀 ) → dom 𝑀 ran sigAlgebra )
37 35 36 syl ( ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) ∧ ( ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜑 } ) = 0 ∧ ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜓 } ) = 0 ) ) → dom 𝑀 ran sigAlgebra )
38 12 adantr ( ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) ∧ ( ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜑 } ) = 0 ∧ ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜓 } ) = 0 ) ) → { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 )
39 25 adantr ( ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) ∧ ( ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜑 } ) = 0 ∧ ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜓 } ) = 0 ) ) → { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 )
40 37 38 39 15 syl3anc ( ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) ∧ ( ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜑 } ) = 0 ∧ ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜓 } ) = 0 ) ) → ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ∈ dom 𝑀 )
41 35 38 39 measunl ( ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) ∧ ( ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜑 } ) = 0 ∧ ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜓 } ) = 0 ) ) → ( 𝑀 ‘ ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ) ≤ ( ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜑 } ) +𝑒 ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ) )
42 simprl ( ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) ∧ ( ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜑 } ) = 0 ∧ ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜓 } ) = 0 ) ) → ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜑 } ) = 0 )
43 simprr ( ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) ∧ ( ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜑 } ) = 0 ∧ ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜓 } ) = 0 ) ) → ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜓 } ) = 0 )
44 42 43 oveq12d ( ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) ∧ ( ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜑 } ) = 0 ∧ ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜓 } ) = 0 ) ) → ( ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜑 } ) +𝑒 ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ) = ( 0 +𝑒 0 ) )
45 0xr 0 ∈ ℝ*
46 xaddid1 ( 0 ∈ ℝ* → ( 0 +𝑒 0 ) = 0 )
47 45 46 ax-mp ( 0 +𝑒 0 ) = 0
48 44 47 eqtrdi ( ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) ∧ ( ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜑 } ) = 0 ∧ ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜓 } ) = 0 ) ) → ( ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜑 } ) +𝑒 ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ) = 0 )
49 41 48 breqtrd ( ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) ∧ ( ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜑 } ) = 0 ∧ ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜓 } ) = 0 ) ) → ( 𝑀 ‘ ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ) ≤ 0 )
50 measle0 ( ( 𝑀 ∈ ( measures ‘ dom 𝑀 ) ∧ ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ∈ dom 𝑀 ∧ ( 𝑀 ‘ ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ) ≤ 0 ) → ( 𝑀 ‘ ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ) = 0 )
51 35 40 49 50 syl3anc ( ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) ∧ ( ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜑 } ) = 0 ∧ ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜓 } ) = 0 ) ) → ( 𝑀 ‘ ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ) = 0 )
52 34 51 impbida ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) → ( ( 𝑀 ‘ ( { 𝑥𝑂 ∣ ¬ 𝜑 } ∪ { 𝑥𝑂 ∣ ¬ 𝜓 } ) ) = 0 ↔ ( ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜑 } ) = 0 ∧ ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜓 } ) = 0 ) ) )
53 7 52 bitr3id ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) → ( ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ ( 𝜑𝜓 ) } ) = 0 ↔ ( ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜑 } ) = 0 ∧ ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜓 } ) = 0 ) ) )
54 1 braew ( 𝑀 ran measures → ( { 𝑥𝑂 ∣ ( 𝜑𝜓 ) } a.e. 𝑀 ↔ ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ ( 𝜑𝜓 ) } ) = 0 ) )
55 54 3ad2ant1 ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) → ( { 𝑥𝑂 ∣ ( 𝜑𝜓 ) } a.e. 𝑀 ↔ ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ ( 𝜑𝜓 ) } ) = 0 ) )
56 1 braew ( 𝑀 ran measures → ( { 𝑥𝑂𝜑 } a.e. 𝑀 ↔ ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜑 } ) = 0 ) )
57 1 braew ( 𝑀 ran measures → ( { 𝑥𝑂𝜓 } a.e. 𝑀 ↔ ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜓 } ) = 0 ) )
58 56 57 anbi12d ( 𝑀 ran measures → ( ( { 𝑥𝑂𝜑 } a.e. 𝑀 ∧ { 𝑥𝑂𝜓 } a.e. 𝑀 ) ↔ ( ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜑 } ) = 0 ∧ ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜓 } ) = 0 ) ) )
59 58 3ad2ant1 ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) → ( ( { 𝑥𝑂𝜑 } a.e. 𝑀 ∧ { 𝑥𝑂𝜓 } a.e. 𝑀 ) ↔ ( ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜑 } ) = 0 ∧ ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜓 } ) = 0 ) ) )
60 53 55 59 3bitr4d ( ( 𝑀 ran measures ∧ { 𝑥𝑂 ∣ ¬ 𝜑 } ∈ dom 𝑀 ∧ { 𝑥𝑂 ∣ ¬ 𝜓 } ∈ dom 𝑀 ) → ( { 𝑥𝑂 ∣ ( 𝜑𝜓 ) } a.e. 𝑀 ↔ ( { 𝑥𝑂𝜑 } a.e. 𝑀 ∧ { 𝑥𝑂𝜓 } a.e. 𝑀 ) ) )