Metamath Proof Explorer

Theorem ismeannd

Description: Sufficient condition to prove that M is a measure. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses ismeannd.sal ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
ismeannd.mf ⊢ ( 𝜑 → 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) )
ismeannd.m0 ⊢ ( 𝜑 → ( 𝑀 ‘ ∅ ) = 0 )
ismeannd.iun ⊢ ( ( 𝜑 ∧ 𝑒 : ℕ ⟶ 𝑆 ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → ( 𝑀 ‘ ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑀 ‘ ( 𝑒 ‘ 𝑛 ) ) ) ) )
Assertion ismeannd ( 𝜑 → 𝑀 ∈ Meas )

Proof

Step Hyp Ref Expression
1 ismeannd.sal ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
2 ismeannd.mf ⊢ ( 𝜑 → 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) )
3 ismeannd.m0 ⊢ ( 𝜑 → ( 𝑀 ‘ ∅ ) = 0 )
4 ismeannd.iun ⊢ ( ( 𝜑 ∧ 𝑒 : ℕ ⟶ 𝑆 ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → ( 𝑀 ‘ ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑀 ‘ ( 𝑒 ‘ 𝑛 ) ) ) ) )
5 2 fdmd ⊢ ( 𝜑 → dom 𝑀 = 𝑆 )
6 5 feq2d ⊢ ( 𝜑 → ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ↔ 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) ) )
7 2 6 mpbird ⊢ ( 𝜑 → 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) )
8 5 1 eqeltrd ⊢ ( 𝜑 → dom 𝑀 ∈ SAlg )
9 7 8 jca ⊢ ( 𝜑 → ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑀 ∈ SAlg ) )
10 unieq ⊢ ( 𝑥 = ∅ → ∪ 𝑥 = ∪ ∅ )
11 uni0 ⊢ ∪ ∅ = ∅
12 11 a1i ⊢ ( 𝑥 = ∅ → ∪ ∅ = ∅ )
13 10 12 eqtrd ⊢ ( 𝑥 = ∅ → ∪ 𝑥 = ∅ )
14 13 fveq2d ⊢ ( 𝑥 = ∅ → ( 𝑀 ‘ ∪ 𝑥 ) = ( 𝑀 ‘ ∅ ) )
15 14 3 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑥 = ∅ ) → ( 𝑀 ‘ ∪ 𝑥 ) = 0 )
16 reseq2 ⊢ ( 𝑥 = ∅ → ( 𝑀 ↾ 𝑥 ) = ( 𝑀 ↾ ∅ ) )
17 res0 ⊢ ( 𝑀 ↾ ∅ ) = ∅
18 17 a1i ⊢ ( 𝑥 = ∅ → ( 𝑀 ↾ ∅ ) = ∅ )
19 16 18 eqtrd ⊢ ( 𝑥 = ∅ → ( 𝑀 ↾ 𝑥 ) = ∅ )
20 19 fveq2d ⊢ ( 𝑥 = ∅ → ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) = ( Σ^ ‘ ∅ ) )
21 20 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = ∅ ) → ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) = ( Σ^ ‘ ∅ ) )
22 sge00 ⊢ ( Σ^ ‘ ∅ ) = 0
23 22 a1i ⊢ ( ( 𝜑 ∧ 𝑥 = ∅ ) → ( Σ^ ‘ ∅ ) = 0 )
24 21 23 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 = ∅ ) → ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) = 0 )
25 15 24 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 = ∅ ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) )
26 25 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑥 = ∅ ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) )
27 26 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑥 = ∅ ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) )
28 simpll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ ¬ 𝑥 = ∅ ) → ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) )
29 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ ¬ 𝑥 = ∅ ) → Disj 𝑦 ∈ 𝑥 𝑦 )
30 28 29 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ ¬ 𝑥 = ∅ ) → ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) )
31 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ ¬ 𝑥 = ∅ ) → 𝑥 ≼ ω )
32 neqne ⊢ ( ¬ 𝑥 = ∅ → 𝑥 ≠ ∅ )
33 32 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ ¬ 𝑥 = ∅ ) → 𝑥 ≠ ∅ )
34 id ⊢ ( 𝑦 = 𝑤 → 𝑦 = 𝑤 )
35 34 cbvdisjv ⊢ ( Disj 𝑦 ∈ 𝑥 𝑦 ↔ Disj 𝑤 ∈ 𝑥 𝑤 )
36 35 bilani ⊢ ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → Disj 𝑤 ∈ 𝑥 𝑤 )
37 36 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ ¬ 𝑥 = ∅ ) → Disj 𝑤 ∈ 𝑥 𝑤 )
38 31 33 37 nnfoctbdj ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ ¬ 𝑥 = ∅ ) → ∃ 𝑒 ( 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) )
39 simpl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ∧ ( 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) ) → ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) )
40 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ∧ ( 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) ) → 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) )
41 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ∧ ( 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) ) → Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) )
42 founiiun0 ⊢ ( 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) → ∪ 𝑥 = ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) )
43 42 fveq2d ⊢ ( 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( 𝑀 ‘ ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) )
44 43 ad2antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( 𝑀 ‘ ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) )
45 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → 𝜑 )
46 fof ⊢ ( 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) → 𝑒 : ℕ ⟶ ( 𝑥 ∪ { ∅ } ) )
47 46 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) → 𝑒 : ℕ ⟶ ( 𝑥 ∪ { ∅ } ) )
48 elpwi ⊢ ( 𝑥 ∈ 𝒫 dom 𝑀 → 𝑥 ⊆ dom 𝑀 )
49 48 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → 𝑥 ⊆ dom 𝑀 )
50 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → dom 𝑀 = 𝑆 )
51 49 50 sseqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → 𝑥 ⊆ 𝑆 )
52 0sal ⊢ ( 𝑆 ∈ SAlg → ∅ ∈ 𝑆 )
53 1 52 syl ⊢ ( 𝜑 → ∅ ∈ 𝑆 )
54 snssi ⊢ ( ∅ ∈ 𝑆 → { ∅ } ⊆ 𝑆 )
55 53 54 syl ⊢ ( 𝜑 → { ∅ } ⊆ 𝑆 )
56 55 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → { ∅ } ⊆ 𝑆 )
57 51 56 unssd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → ( 𝑥 ∪ { ∅ } ) ⊆ 𝑆 )
58 57 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) → ( 𝑥 ∪ { ∅ } ) ⊆ 𝑆 )
59 47 58 fssd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) → 𝑒 : ℕ ⟶ 𝑆 )
60 59 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → 𝑒 : ℕ ⟶ 𝑆 )
61 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) )
62 45 60 61 4 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → ( 𝑀 ‘ ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑀 ‘ ( 𝑒 ‘ 𝑛 ) ) ) ) )
63 62 adantllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → ( 𝑀 ‘ ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑀 ‘ ( 𝑒 ‘ 𝑛 ) ) ) ) )
64 2 feqmptd ⊢ ( 𝜑 → 𝑀 = ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ 𝑦 ) ) )
65 64 reseq1d ⊢ ( 𝜑 → ( 𝑀 ↾ 𝑥 ) = ( ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ 𝑦 ) ) ↾ 𝑥 ) )
66 65 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → ( 𝑀 ↾ 𝑥 ) = ( ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ 𝑦 ) ) ↾ 𝑥 ) )
67 66 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ∅ ∈ 𝑥 ) → ( 𝑀 ↾ 𝑥 ) = ( ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ 𝑦 ) ) ↾ 𝑥 ) )
68 51 resmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → ( ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ 𝑦 ) ) ↾ 𝑥 ) = ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) )
69 68 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ∅ ∈ 𝑥 ) → ( ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ 𝑦 ) ) ↾ 𝑥 ) = ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) )
70 snssi ⊢ ( ∅ ∈ 𝑥 → { ∅ } ⊆ 𝑥 )
71 ssequn2 ⊢ ( { ∅ } ⊆ 𝑥 ↔ ( 𝑥 ∪ { ∅ } ) = 𝑥 )
72 70 71 sylib ⊢ ( ∅ ∈ 𝑥 → ( 𝑥 ∪ { ∅ } ) = 𝑥 )
73 72 eqcomd ⊢ ( ∅ ∈ 𝑥 → 𝑥 = ( 𝑥 ∪ { ∅ } ) )
74 73 mpteq1d ⊢ ( ∅ ∈ 𝑥 → ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) = ( 𝑦 ∈ ( 𝑥 ∪ { ∅ } ) ↦ ( 𝑀 ‘ 𝑦 ) ) )
75 74 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ∅ ∈ 𝑥 ) → ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) = ( 𝑦 ∈ ( 𝑥 ∪ { ∅ } ) ↦ ( 𝑀 ‘ 𝑦 ) ) )
76 67 69 75 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ∅ ∈ 𝑥 ) → ( 𝑀 ↾ 𝑥 ) = ( 𝑦 ∈ ( 𝑥 ∪ { ∅ } ) ↦ ( 𝑀 ‘ 𝑦 ) ) )
77 76 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ∅ ∈ 𝑥 ) → ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) = ( Σ^ ‘ ( 𝑦 ∈ ( 𝑥 ∪ { ∅ } ) ↦ ( 𝑀 ‘ 𝑦 ) ) ) )
78 nfv ⊢ Ⅎ 𝑦 ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ¬ ∅ ∈ 𝑥 )
79 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ¬ ∅ ∈ 𝑥 ) → 𝑥 ∈ 𝒫 dom 𝑀 )
80 p0ex ⊢ { ∅ } ∈ V
81 80 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ¬ ∅ ∈ 𝑥 ) → { ∅ } ∈ V )
82 disjsn ⊢ ( ( 𝑥 ∩ { ∅ } ) = ∅ ↔ ¬ ∅ ∈ 𝑥 )
83 82 bilanri ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ¬ ∅ ∈ 𝑥 ) → ( 𝑥 ∩ { ∅ } ) = ∅ )
84 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑦 ∈ 𝑥 ) → 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) )
85 51 sselda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑆 )
86 84 85 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑀 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) )
87 86 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ¬ ∅ ∈ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑀 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) )
88 elsni ⊢ ( 𝑦 ∈ { ∅ } → 𝑦 = ∅ )
89 88 fveq2d ⊢ ( 𝑦 ∈ { ∅ } → ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ ∅ ) )
90 89 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { ∅ } ) → ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ ∅ ) )
91 2 53 ffvelcdmd ⊢ ( 𝜑 → ( 𝑀 ‘ ∅ ) ∈ ( 0 [,] +∞ ) )
92 91 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { ∅ } ) → ( 𝑀 ‘ ∅ ) ∈ ( 0 [,] +∞ ) )
93 90 92 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { ∅ } ) → ( 𝑀 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) )
94 93 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ¬ ∅ ∈ 𝑥 ) ∧ 𝑦 ∈ { ∅ } ) → ( 𝑀 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) )
95 78 79 81 83 87 94 sge0splitmpt ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ¬ ∅ ∈ 𝑥 ) → ( Σ^ ‘ ( 𝑦 ∈ ( 𝑥 ∪ { ∅ } ) ↦ ( 𝑀 ‘ 𝑦 ) ) ) = ( ( Σ^ ‘ ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) ) +𝑒 ( Σ^ ‘ ( 𝑦 ∈ { ∅ } ↦ ( 𝑀 ‘ 𝑦 ) ) ) ) )
96 fveq2 ⊢ ( 𝑦 = ∅ → ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ ∅ ) )
97 96 adantl ⊢ ( ( 𝜑 ∧ 𝑦 = ∅ ) → ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ ∅ ) )
98 3 adantr ⊢ ( ( 𝜑 ∧ 𝑦 = ∅ ) → ( 𝑀 ‘ ∅ ) = 0 )
99 97 98 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 = ∅ ) → ( 𝑀 ‘ 𝑦 ) = 0 )
100 88 99 sylan2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { ∅ } ) → ( 𝑀 ‘ 𝑦 ) = 0 )
101 100 mpteq2dva ⊢ ( 𝜑 → ( 𝑦 ∈ { ∅ } ↦ ( 𝑀 ‘ 𝑦 ) ) = ( 𝑦 ∈ { ∅ } ↦ 0 ) )
102 101 fveq2d ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑦 ∈ { ∅ } ↦ ( 𝑀 ‘ 𝑦 ) ) ) = ( Σ^ ‘ ( 𝑦 ∈ { ∅ } ↦ 0 ) ) )
103 nfv ⊢ Ⅎ 𝑦 𝜑
104 80 a1i ⊢ ( 𝜑 → { ∅ } ∈ V )
105 103 104 sge0z ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑦 ∈ { ∅ } ↦ 0 ) ) = 0 )
106 102 105 eqtrd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑦 ∈ { ∅ } ↦ ( 𝑀 ‘ 𝑦 ) ) ) = 0 )
107 106 oveq2d ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) ) +𝑒 ( Σ^ ‘ ( 𝑦 ∈ { ∅ } ↦ ( 𝑀 ‘ 𝑦 ) ) ) ) = ( ( Σ^ ‘ ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) ) +𝑒 0 ) )
108 107 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ¬ ∅ ∈ 𝑥 ) → ( ( Σ^ ‘ ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) ) +𝑒 ( Σ^ ‘ ( 𝑦 ∈ { ∅ } ↦ ( 𝑀 ‘ 𝑦 ) ) ) ) = ( ( Σ^ ‘ ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) ) +𝑒 0 ) )
109 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → 𝑥 ∈ 𝒫 dom 𝑀 )
110 66 68 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → ( 𝑀 ↾ 𝑥 ) = ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) )
111 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) )
112 111 51 fssresd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → ( 𝑀 ↾ 𝑥 ) : 𝑥 ⟶ ( 0 [,] +∞ ) )
113 110 112 feq1dd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) : 𝑥 ⟶ ( 0 [,] +∞ ) )
114 109 113 sge0xrcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → ( Σ^ ‘ ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) ) ∈ ℝ* )
115 114 xaddridd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → ( ( Σ^ ‘ ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) ) +𝑒 0 ) = ( Σ^ ‘ ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) ) )
116 110 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) = ( Σ^ ‘ ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) ) )
117 116 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → ( Σ^ ‘ ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) )
118 115 117 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → ( ( Σ^ ‘ ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) ) +𝑒 0 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) )
119 118 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ¬ ∅ ∈ 𝑥 ) → ( ( Σ^ ‘ ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) ) +𝑒 0 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) )
120 95 108 119 3eqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ¬ ∅ ∈ 𝑥 ) → ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) = ( Σ^ ‘ ( 𝑦 ∈ ( 𝑥 ∪ { ∅ } ) ↦ ( 𝑀 ‘ 𝑦 ) ) ) )
121 77 120 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) = ( Σ^ ‘ ( 𝑦 ∈ ( 𝑥 ∪ { ∅ } ) ↦ ( 𝑀 ‘ 𝑦 ) ) ) )
122 121 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) = ( Σ^ ‘ ( 𝑦 ∈ ( 𝑥 ∪ { ∅ } ) ↦ ( 𝑀 ‘ 𝑦 ) ) ) )
123 nfv ⊢ Ⅎ 𝑦 ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) )
124 nfv ⊢ Ⅎ 𝑛 ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) )
125 nfdisj1 ⊢ Ⅎ 𝑛 Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 )
126 124 125 nfan ⊢ Ⅎ 𝑛 ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) )
127 fveq2 ⊢ ( 𝑦 = ( 𝑒 ‘ 𝑛 ) → ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ ( 𝑒 ‘ 𝑛 ) ) )
128 nnex ⊢ ℕ ∈ V
129 128 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → ℕ ∈ V )
130 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) )
131 eqidd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑒 ‘ 𝑛 ) = ( 𝑒 ‘ 𝑛 ) )
132 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑦 ∈ ( 𝑥 ∪ { ∅ } ) ) → 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) )
133 57 sselda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑦 ∈ ( 𝑥 ∪ { ∅ } ) ) → 𝑦 ∈ 𝑆 )
134 132 133 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑦 ∈ ( 𝑥 ∪ { ∅ } ) ) → ( 𝑀 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) )
135 134 ad4ant14 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ( 𝑥 ∪ { ∅ } ) ) → ( 𝑀 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) )
136 45 99 sylan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) ∧ 𝑦 = ∅ ) → ( 𝑀 ‘ 𝑦 ) = 0 )
137 123 126 127 129 130 61 131 135 136 sge0fodjrn ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → ( Σ^ ‘ ( 𝑦 ∈ ( 𝑥 ∪ { ∅ } ) ↦ ( 𝑀 ‘ 𝑦 ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑀 ‘ ( 𝑒 ‘ 𝑛 ) ) ) ) )
138 122 137 eqtr2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑀 ‘ ( 𝑒 ‘ 𝑛 ) ) ) ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) )
139 138 adantllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑀 ‘ ( 𝑒 ‘ 𝑛 ) ) ) ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) )
140 44 63 139 3eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) )
141 39 40 41 140 syl21anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ∧ ( 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) )
142 141 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( ( 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) ) )
143 142 exlimdv ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( ∃ 𝑒 ( 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) ) )
144 30 38 143 sylc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ ¬ 𝑥 = ∅ ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) )
145 27 144 pm2.61dan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) )
146 145 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) ) )
147 146 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝒫 dom 𝑀 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) ) )
148 9 3 147 jca31 ⊢ ( 𝜑 → ( ( ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑀 ∈ SAlg ) ∧ ( 𝑀 ‘ ∅ ) = 0 ) ∧ ∀ 𝑥 ∈ 𝒫 dom 𝑀 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) ) ) )
149 ismea ⊢ ( 𝑀 ∈ Meas ↔ ( ( ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑀 ∈ SAlg ) ∧ ( 𝑀 ‘ ∅ ) = 0 ) ∧ ∀ 𝑥 ∈ 𝒫 dom 𝑀 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) ) ) )
150 148 149 sylibr ⊢ ( 𝜑 → 𝑀 ∈ Meas )