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 biimpi ⊢ ( Disj 𝑦 ∈ 𝑥 𝑦 → Disj 𝑤 ∈ 𝑥 𝑤 )
37 36 adantl ⊢ ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → Disj 𝑤 ∈ 𝑥 𝑤 )
38 37 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ ¬ 𝑥 = ∅ ) → Disj 𝑤 ∈ 𝑥 𝑤 )
39 31 33 38 nnfoctbdj ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ ¬ 𝑥 = ∅ ) → ∃ 𝑒 ( 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) )
40 simpl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ∧ ( 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) ) → ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) )
41 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ∧ ( 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) ) → 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) )
42 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ∧ ( 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) ) → Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) )
43 founiiun0 ⊢ ( 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) → ∪ 𝑥 = ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) )
44 43 fveq2d ⊢ ( 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( 𝑀 ‘ ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) )
45 44 ad2antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( 𝑀 ‘ ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) )
46 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → 𝜑 )
47 fof ⊢ ( 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) → 𝑒 : ℕ ⟶ ( 𝑥 ∪ { ∅ } ) )
48 47 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) → 𝑒 : ℕ ⟶ ( 𝑥 ∪ { ∅ } ) )
49 elpwi ⊢ ( 𝑥 ∈ 𝒫 dom 𝑀 → 𝑥 ⊆ dom 𝑀 )
50 49 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → 𝑥 ⊆ dom 𝑀 )
51 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → dom 𝑀 = 𝑆 )
52 50 51 sseqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → 𝑥 ⊆ 𝑆 )
53 0sal ⊢ ( 𝑆 ∈ SAlg → ∅ ∈ 𝑆 )
54 1 53 syl ⊢ ( 𝜑 → ∅ ∈ 𝑆 )
55 snssi ⊢ ( ∅ ∈ 𝑆 → { ∅ } ⊆ 𝑆 )
56 54 55 syl ⊢ ( 𝜑 → { ∅ } ⊆ 𝑆 )
57 56 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → { ∅ } ⊆ 𝑆 )
58 52 57 unssd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → ( 𝑥 ∪ { ∅ } ) ⊆ 𝑆 )
59 58 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) → ( 𝑥 ∪ { ∅ } ) ⊆ 𝑆 )
60 48 59 fssd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) → 𝑒 : ℕ ⟶ 𝑆 )
61 60 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → 𝑒 : ℕ ⟶ 𝑆 )
62 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) )
63 46 61 62 4 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → ( 𝑀 ‘ ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑀 ‘ ( 𝑒 ‘ 𝑛 ) ) ) ) )
64 63 adantllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → ( 𝑀 ‘ ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑀 ‘ ( 𝑒 ‘ 𝑛 ) ) ) ) )
65 2 feqmptd ⊢ ( 𝜑 → 𝑀 = ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ 𝑦 ) ) )
66 65 reseq1d ⊢ ( 𝜑 → ( 𝑀 ↾ 𝑥 ) = ( ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ 𝑦 ) ) ↾ 𝑥 ) )
67 66 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → ( 𝑀 ↾ 𝑥 ) = ( ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ 𝑦 ) ) ↾ 𝑥 ) )
68 67 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ∅ ∈ 𝑥 ) → ( 𝑀 ↾ 𝑥 ) = ( ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ 𝑦 ) ) ↾ 𝑥 ) )
69 52 resmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → ( ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ 𝑦 ) ) ↾ 𝑥 ) = ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) )
70 69 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ∅ ∈ 𝑥 ) → ( ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ 𝑦 ) ) ↾ 𝑥 ) = ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) )
71 snssi ⊢ ( ∅ ∈ 𝑥 → { ∅ } ⊆ 𝑥 )
72 ssequn2 ⊢ ( { ∅ } ⊆ 𝑥 ↔ ( 𝑥 ∪ { ∅ } ) = 𝑥 )
73 71 72 sylib ⊢ ( ∅ ∈ 𝑥 → ( 𝑥 ∪ { ∅ } ) = 𝑥 )
74 73 eqcomd ⊢ ( ∅ ∈ 𝑥 → 𝑥 = ( 𝑥 ∪ { ∅ } ) )
75 74 mpteq1d ⊢ ( ∅ ∈ 𝑥 → ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) = ( 𝑦 ∈ ( 𝑥 ∪ { ∅ } ) ↦ ( 𝑀 ‘ 𝑦 ) ) )
76 75 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ∅ ∈ 𝑥 ) → ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) = ( 𝑦 ∈ ( 𝑥 ∪ { ∅ } ) ↦ ( 𝑀 ‘ 𝑦 ) ) )
77 68 70 76 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ∅ ∈ 𝑥 ) → ( 𝑀 ↾ 𝑥 ) = ( 𝑦 ∈ ( 𝑥 ∪ { ∅ } ) ↦ ( 𝑀 ‘ 𝑦 ) ) )
78 77 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ∅ ∈ 𝑥 ) → ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) = ( Σ^ ‘ ( 𝑦 ∈ ( 𝑥 ∪ { ∅ } ) ↦ ( 𝑀 ‘ 𝑦 ) ) ) )
79 nfv ⊢ Ⅎ 𝑦 ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ¬ ∅ ∈ 𝑥 )
80 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ¬ ∅ ∈ 𝑥 ) → 𝑥 ∈ 𝒫 dom 𝑀 )
81 p0ex ⊢ { ∅ } ∈ V
82 81 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ¬ ∅ ∈ 𝑥 ) → { ∅ } ∈ V )
83 disjsn ⊢ ( ( 𝑥 ∩ { ∅ } ) = ∅ ↔ ¬ ∅ ∈ 𝑥 )
84 83 biimpri ⊢ ( ¬ ∅ ∈ 𝑥 → ( 𝑥 ∩ { ∅ } ) = ∅ )
85 84 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ¬ ∅ ∈ 𝑥 ) → ( 𝑥 ∩ { ∅ } ) = ∅ )
86 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑦 ∈ 𝑥 ) → 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) )
87 52 sselda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑆 )
88 86 87 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑀 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) )
89 88 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ¬ ∅ ∈ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑀 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) )
90 elsni ⊢ ( 𝑦 ∈ { ∅ } → 𝑦 = ∅ )
91 90 fveq2d ⊢ ( 𝑦 ∈ { ∅ } → ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ ∅ ) )
92 91 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { ∅ } ) → ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ ∅ ) )
93 2 54 ffvelcdmd ⊢ ( 𝜑 → ( 𝑀 ‘ ∅ ) ∈ ( 0 [,] +∞ ) )
94 93 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { ∅ } ) → ( 𝑀 ‘ ∅ ) ∈ ( 0 [,] +∞ ) )
95 92 94 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { ∅ } ) → ( 𝑀 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) )
96 95 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ¬ ∅ ∈ 𝑥 ) ∧ 𝑦 ∈ { ∅ } ) → ( 𝑀 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) )
97 79 80 82 85 89 96 sge0splitmpt ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ¬ ∅ ∈ 𝑥 ) → ( Σ^ ‘ ( 𝑦 ∈ ( 𝑥 ∪ { ∅ } ) ↦ ( 𝑀 ‘ 𝑦 ) ) ) = ( ( Σ^ ‘ ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) ) +𝑒 ( Σ^ ‘ ( 𝑦 ∈ { ∅ } ↦ ( 𝑀 ‘ 𝑦 ) ) ) ) )
98 fveq2 ⊢ ( 𝑦 = ∅ → ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ ∅ ) )
99 98 adantl ⊢ ( ( 𝜑 ∧ 𝑦 = ∅ ) → ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ ∅ ) )
100 3 adantr ⊢ ( ( 𝜑 ∧ 𝑦 = ∅ ) → ( 𝑀 ‘ ∅ ) = 0 )
101 99 100 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 = ∅ ) → ( 𝑀 ‘ 𝑦 ) = 0 )
102 90 101 sylan2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { ∅ } ) → ( 𝑀 ‘ 𝑦 ) = 0 )
103 102 mpteq2dva ⊢ ( 𝜑 → ( 𝑦 ∈ { ∅ } ↦ ( 𝑀 ‘ 𝑦 ) ) = ( 𝑦 ∈ { ∅ } ↦ 0 ) )
104 103 fveq2d ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑦 ∈ { ∅ } ↦ ( 𝑀 ‘ 𝑦 ) ) ) = ( Σ^ ‘ ( 𝑦 ∈ { ∅ } ↦ 0 ) ) )
105 nfv ⊢ Ⅎ 𝑦 𝜑
106 81 a1i ⊢ ( 𝜑 → { ∅ } ∈ V )
107 105 106 sge0z ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑦 ∈ { ∅ } ↦ 0 ) ) = 0 )
108 104 107 eqtrd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑦 ∈ { ∅ } ↦ ( 𝑀 ‘ 𝑦 ) ) ) = 0 )
109 108 oveq2d ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) ) +𝑒 ( Σ^ ‘ ( 𝑦 ∈ { ∅ } ↦ ( 𝑀 ‘ 𝑦 ) ) ) ) = ( ( Σ^ ‘ ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) ) +𝑒 0 ) )
110 109 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ¬ ∅ ∈ 𝑥 ) → ( ( Σ^ ‘ ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) ) +𝑒 ( Σ^ ‘ ( 𝑦 ∈ { ∅ } ↦ ( 𝑀 ‘ 𝑦 ) ) ) ) = ( ( Σ^ ‘ ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) ) +𝑒 0 ) )
111 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → 𝑥 ∈ 𝒫 dom 𝑀 )
112 67 69 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → ( 𝑀 ↾ 𝑥 ) = ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) )
113 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) )
114 113 52 fssresd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → ( 𝑀 ↾ 𝑥 ) : 𝑥 ⟶ ( 0 [,] +∞ ) )
115 112 114 feq1dd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) : 𝑥 ⟶ ( 0 [,] +∞ ) )
116 111 115 sge0xrcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → ( Σ^ ‘ ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) ) ∈ ℝ* )
117 116 xaddridd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → ( ( Σ^ ‘ ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) ) +𝑒 0 ) = ( Σ^ ‘ ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) ) )
118 112 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) = ( Σ^ ‘ ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) ) )
119 118 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → ( Σ^ ‘ ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) )
120 117 119 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → ( ( Σ^ ‘ ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) ) +𝑒 0 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) )
121 120 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ¬ ∅ ∈ 𝑥 ) → ( ( Σ^ ‘ ( 𝑦 ∈ 𝑥 ↦ ( 𝑀 ‘ 𝑦 ) ) ) +𝑒 0 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) )
122 97 110 121 3eqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ¬ ∅ ∈ 𝑥 ) → ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) = ( Σ^ ‘ ( 𝑦 ∈ ( 𝑥 ∪ { ∅ } ) ↦ ( 𝑀 ‘ 𝑦 ) ) ) )
123 78 122 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) = ( Σ^ ‘ ( 𝑦 ∈ ( 𝑥 ∪ { ∅ } ) ↦ ( 𝑀 ‘ 𝑦 ) ) ) )
124 123 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) = ( Σ^ ‘ ( 𝑦 ∈ ( 𝑥 ∪ { ∅ } ) ↦ ( 𝑀 ‘ 𝑦 ) ) ) )
125 nfv ⊢ Ⅎ 𝑦 ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) )
126 nfv ⊢ Ⅎ 𝑛 ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) )
127 nfdisj1 ⊢ Ⅎ 𝑛 Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 )
128 126 127 nfan ⊢ Ⅎ 𝑛 ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) )
129 fveq2 ⊢ ( 𝑦 = ( 𝑒 ‘ 𝑛 ) → ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ ( 𝑒 ‘ 𝑛 ) ) )
130 nnex ⊢ ℕ ∈ V
131 130 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → ℕ ∈ V )
132 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) )
133 eqidd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑒 ‘ 𝑛 ) = ( 𝑒 ‘ 𝑛 ) )
134 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑦 ∈ ( 𝑥 ∪ { ∅ } ) ) → 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) )
135 58 sselda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑦 ∈ ( 𝑥 ∪ { ∅ } ) ) → 𝑦 ∈ 𝑆 )
136 134 135 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑦 ∈ ( 𝑥 ∪ { ∅ } ) ) → ( 𝑀 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) )
137 136 ad4ant14 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ( 𝑥 ∪ { ∅ } ) ) → ( 𝑀 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) )
138 46 101 sylan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) ∧ 𝑦 = ∅ ) → ( 𝑀 ‘ 𝑦 ) = 0 )
139 125 128 129 131 132 62 133 137 138 sge0fodjrn ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → ( Σ^ ‘ ( 𝑦 ∈ ( 𝑥 ∪ { ∅ } ) ↦ ( 𝑀 ‘ 𝑦 ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑀 ‘ ( 𝑒 ‘ 𝑛 ) ) ) ) )
140 124 139 eqtr2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑀 ‘ ( 𝑒 ‘ 𝑛 ) ) ) ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) )
141 140 adantllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑀 ‘ ( 𝑒 ‘ 𝑛 ) ) ) ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) )
142 45 64 141 3eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ∧ 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) )
143 40 41 42 142 syl21anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ∧ ( 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) )
144 143 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( ( 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) ) )
145 144 exlimdv ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( ∃ 𝑒 ( 𝑒 : ℕ –onto→ ( 𝑥 ∪ { ∅ } ) ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) ) )
146 30 39 145 sylc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ ¬ 𝑥 = ∅ ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) )
147 27 146 pm2.61dan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) )
148 147 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀 ) → ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) ) )
149 148 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝒫 dom 𝑀 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) ) )
150 9 3 149 jca31 ⊢ ( 𝜑 → ( ( ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑀 ∈ SAlg ) ∧ ( 𝑀 ‘ ∅ ) = 0 ) ∧ ∀ 𝑥 ∈ 𝒫 dom 𝑀 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) ) ) )
151 ismea ⊢ ( 𝑀 ∈ Meas ↔ ( ( ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑀 ∈ SAlg ) ∧ ( 𝑀 ‘ ∅ ) = 0 ) ∧ ∀ 𝑥 ∈ 𝒫 dom 𝑀 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) ) ) )
152 150 151 sylibr ⊢ ( 𝜑 → 𝑀 ∈ Meas )