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. 𝑀 ) ) )