Metamath Proof Explorer

Theorem measinb

Description: Building a measure restricted to the intersection with a given set. (Contributed by Thierry Arnoux, 25-Dec-2016)

Ref Expression
Assertion measinb ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) → ( 𝑥 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) ∈ ( measures ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 simpll ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑀 ∈ ( measures ‘ 𝑆 ) )
2 measbase ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑆 ∈ ∪ ran sigAlgebra )
3 2 ad2antrr ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑆 ∈ ∪ ran sigAlgebra )
4 simpr ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 )
5 simplr ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ 𝑆 )
6 inelsiga ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑥 ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ) → ( 𝑥 ∩ 𝐴 ) ∈ 𝑆 )
7 3 4 5 6 syl3anc ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ∩ 𝐴 ) ∈ 𝑆 )
8 measvxrge0 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑥 ∩ 𝐴 ) ∈ 𝑆 ) → ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ( 0 [,] +∞ ) )
9 1 7 8 syl2anc ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ( 0 [,] +∞ ) )
10 9 fmpttd ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) → ( 𝑥 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) : 𝑆 ⟶ ( 0 [,] +∞ ) )
11 eqidd ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) → ( 𝑥 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) = ( 𝑥 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) )
12 ineq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 ∩ 𝐴 ) = ( ∅ ∩ 𝐴 ) )
13 0in ⊢ ( ∅ ∩ 𝐴 ) = ∅
14 12 13 eqtrdi ⊢ ( 𝑥 = ∅ → ( 𝑥 ∩ 𝐴 ) = ∅ )
15 14 fveq2d ⊢ ( 𝑥 = ∅ → ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) = ( 𝑀 ‘ ∅ ) )
16 15 adantl ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑥 = ∅ ) → ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) = ( 𝑀 ‘ ∅ ) )
17 measvnul ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → ( 𝑀 ‘ ∅ ) = 0 )
18 17 ad2antrr ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑥 = ∅ ) → ( 𝑀 ‘ ∅ ) = 0 )
19 16 18 eqtrd ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑥 = ∅ ) → ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) = 0 )
20 2 adantr ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) → 𝑆 ∈ ∪ ran sigAlgebra )
21 0elsiga ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ∅ ∈ 𝑆 )
22 20 21 syl ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) → ∅ ∈ 𝑆 )
23 0red ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) → 0 ∈ ℝ )
24 11 19 22 23 fvmptd ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) → ( ( 𝑥 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) ‘ ∅ ) = 0 )
25 measinblem ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝒫 𝑆 ) ∧ ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) ) → ( 𝑀 ‘ ( ∪ 𝑧 ∩ 𝐴 ) ) = Σ* 𝑦 ∈ 𝑧 ( 𝑀 ‘ ( 𝑦 ∩ 𝐴 ) ) )
26 eqidd ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝒫 𝑆 ) ∧ ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) ) → ( 𝑥 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) = ( 𝑥 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) )
27 ineq1 ⊢ ( 𝑥 = ∪ 𝑧 → ( 𝑥 ∩ 𝐴 ) = ( ∪ 𝑧 ∩ 𝐴 ) )
28 27 adantl ⊢ ( ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝒫 𝑆 ) ∧ ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) ) ∧ 𝑥 = ∪ 𝑧 ) → ( 𝑥 ∩ 𝐴 ) = ( ∪ 𝑧 ∩ 𝐴 ) )
29 28 fveq2d ⊢ ( ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝒫 𝑆 ) ∧ ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) ) ∧ 𝑥 = ∪ 𝑧 ) → ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) = ( 𝑀 ‘ ( ∪ 𝑧 ∩ 𝐴 ) ) )
30 simplll ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝒫 𝑆 ) ∧ ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) ) → 𝑀 ∈ ( measures ‘ 𝑆 ) )
31 30 2 syl ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝒫 𝑆 ) ∧ ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) ) → 𝑆 ∈ ∪ ran sigAlgebra )
32 simplr ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝒫 𝑆 ) ∧ ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) ) → 𝑧 ∈ 𝒫 𝑆 )
33 simprl ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝒫 𝑆 ) ∧ ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) ) → 𝑧 ≼ ω )
34 sigaclcu ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑧 ∈ 𝒫 𝑆 ∧ 𝑧 ≼ ω ) → ∪ 𝑧 ∈ 𝑆 )
35 31 32 33 34 syl3anc ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝒫 𝑆 ) ∧ ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) ) → ∪ 𝑧 ∈ 𝑆 )
36 simpllr ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝒫 𝑆 ) ∧ ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) ) → 𝐴 ∈ 𝑆 )
37 inelsiga ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∪ 𝑧 ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ) → ( ∪ 𝑧 ∩ 𝐴 ) ∈ 𝑆 )
38 31 35 36 37 syl3anc ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝒫 𝑆 ) ∧ ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) ) → ( ∪ 𝑧 ∩ 𝐴 ) ∈ 𝑆 )
39 measvxrge0 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( ∪ 𝑧 ∩ 𝐴 ) ∈ 𝑆 ) → ( 𝑀 ‘ ( ∪ 𝑧 ∩ 𝐴 ) ) ∈ ( 0 [,] +∞ ) )
40 30 38 39 syl2anc ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝒫 𝑆 ) ∧ ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) ) → ( 𝑀 ‘ ( ∪ 𝑧 ∩ 𝐴 ) ) ∈ ( 0 [,] +∞ ) )
41 26 29 35 40 fvmptd ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝒫 𝑆 ) ∧ ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) ) → ( ( 𝑥 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) ‘ ∪ 𝑧 ) = ( 𝑀 ‘ ( ∪ 𝑧 ∩ 𝐴 ) ) )
42 eqidd ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝒫 𝑆 ) ∧ 𝑦 ∈ 𝑧 ) → ( 𝑥 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) = ( 𝑥 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) )
43 ineq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∩ 𝐴 ) = ( 𝑦 ∩ 𝐴 ) )
44 43 adantl ⊢ ( ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝒫 𝑆 ) ∧ 𝑦 ∈ 𝑧 ) ∧ 𝑥 = 𝑦 ) → ( 𝑥 ∩ 𝐴 ) = ( 𝑦 ∩ 𝐴 ) )
45 44 fveq2d ⊢ ( ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝒫 𝑆 ) ∧ 𝑦 ∈ 𝑧 ) ∧ 𝑥 = 𝑦 ) → ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) = ( 𝑀 ‘ ( 𝑦 ∩ 𝐴 ) ) )
46 elpwi ⊢ ( 𝑧 ∈ 𝒫 𝑆 → 𝑧 ⊆ 𝑆 )
47 46 ad2antlr ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝒫 𝑆 ) ∧ 𝑦 ∈ 𝑧 ) → 𝑧 ⊆ 𝑆 )
48 simpr ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝒫 𝑆 ) ∧ 𝑦 ∈ 𝑧 ) → 𝑦 ∈ 𝑧 )
49 47 48 sseldd ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝒫 𝑆 ) ∧ 𝑦 ∈ 𝑧 ) → 𝑦 ∈ 𝑆 )
50 simplll ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝒫 𝑆 ) ∧ 𝑦 ∈ 𝑧 ) → 𝑀 ∈ ( measures ‘ 𝑆 ) )
51 50 2 syl ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝒫 𝑆 ) ∧ 𝑦 ∈ 𝑧 ) → 𝑆 ∈ ∪ ran sigAlgebra )
52 simpllr ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝒫 𝑆 ) ∧ 𝑦 ∈ 𝑧 ) → 𝐴 ∈ 𝑆 )
53 inelsiga ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑦 ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ) → ( 𝑦 ∩ 𝐴 ) ∈ 𝑆 )
54 51 49 52 53 syl3anc ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝒫 𝑆 ) ∧ 𝑦 ∈ 𝑧 ) → ( 𝑦 ∩ 𝐴 ) ∈ 𝑆 )
55 measvxrge0 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑦 ∩ 𝐴 ) ∈ 𝑆 ) → ( 𝑀 ‘ ( 𝑦 ∩ 𝐴 ) ) ∈ ( 0 [,] +∞ ) )
56 50 54 55 syl2anc ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝒫 𝑆 ) ∧ 𝑦 ∈ 𝑧 ) → ( 𝑀 ‘ ( 𝑦 ∩ 𝐴 ) ) ∈ ( 0 [,] +∞ ) )
57 42 45 49 56 fvmptd ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝒫 𝑆 ) ∧ 𝑦 ∈ 𝑧 ) → ( ( 𝑥 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) ‘ 𝑦 ) = ( 𝑀 ‘ ( 𝑦 ∩ 𝐴 ) ) )
58 57 esumeq2dv ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝒫 𝑆 ) → Σ* 𝑦 ∈ 𝑧 ( ( 𝑥 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) ‘ 𝑦 ) = Σ* 𝑦 ∈ 𝑧 ( 𝑀 ‘ ( 𝑦 ∩ 𝐴 ) ) )
59 58 adantr ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝒫 𝑆 ) ∧ ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) ) → Σ* 𝑦 ∈ 𝑧 ( ( 𝑥 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) ‘ 𝑦 ) = Σ* 𝑦 ∈ 𝑧 ( 𝑀 ‘ ( 𝑦 ∩ 𝐴 ) ) )
60 25 41 59 3eqtr4d ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝒫 𝑆 ) ∧ ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) ) → ( ( 𝑥 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) ‘ ∪ 𝑧 ) = Σ* 𝑦 ∈ 𝑧 ( ( 𝑥 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) ‘ 𝑦 ) )
61 60 ex ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝒫 𝑆 ) → ( ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) → ( ( 𝑥 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) ‘ ∪ 𝑧 ) = Σ* 𝑦 ∈ 𝑧 ( ( 𝑥 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) ‘ 𝑦 ) ) )
62 61 ralrimiva ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) → ∀ 𝑧 ∈ 𝒫 𝑆 ( ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) → ( ( 𝑥 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) ‘ ∪ 𝑧 ) = Σ* 𝑦 ∈ 𝑧 ( ( 𝑥 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) ‘ 𝑦 ) ) )
63 ismeas ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( ( 𝑥 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) ∈ ( measures ‘ 𝑆 ) ↔ ( ( 𝑥 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( ( 𝑥 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) ‘ ∅ ) = 0 ∧ ∀ 𝑧 ∈ 𝒫 𝑆 ( ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) → ( ( 𝑥 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) ‘ ∪ 𝑧 ) = Σ* 𝑦 ∈ 𝑧 ( ( 𝑥 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) ‘ 𝑦 ) ) ) ) )
64 20 63 syl ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) → ( ( 𝑥 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) ∈ ( measures ‘ 𝑆 ) ↔ ( ( 𝑥 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( ( 𝑥 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) ‘ ∅ ) = 0 ∧ ∀ 𝑧 ∈ 𝒫 𝑆 ( ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) → ( ( 𝑥 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) ‘ ∪ 𝑧 ) = Σ* 𝑦 ∈ 𝑧 ( ( 𝑥 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) ‘ 𝑦 ) ) ) ) )
65 10 24 62 64 mpbir3and ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) → ( 𝑥 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) ∈ ( measures ‘ 𝑆 ) )