Metamath Proof Explorer


Theorem meadjiun

Description: The measure of the disjoint union of a countable set is the extended sum of the measures. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses meadjiun.1 𝑘 𝜑
meadjiun.m ( 𝜑𝑀 ∈ Meas )
meadjiun.s 𝑆 = dom 𝑀
meadjiun.b ( ( 𝜑𝑘𝐴 ) → 𝐵𝑆 )
meadjiun.a ( 𝜑𝐴 ≼ ω )
meadjiun.dj ( 𝜑Disj 𝑘𝐴 𝐵 )
Assertion meadjiun ( 𝜑 → ( 𝑀 𝑘𝐴 𝐵 ) = ( Σ^ ‘ ( 𝑘𝐴 ↦ ( 𝑀𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 meadjiun.1 𝑘 𝜑
2 meadjiun.m ( 𝜑𝑀 ∈ Meas )
3 meadjiun.s 𝑆 = dom 𝑀
4 meadjiun.b ( ( 𝜑𝑘𝐴 ) → 𝐵𝑆 )
5 meadjiun.a ( 𝜑𝐴 ≼ ω )
6 meadjiun.dj ( 𝜑Disj 𝑘𝐴 𝐵 )
7 4 ex ( 𝜑 → ( 𝑘𝐴𝐵𝑆 ) )
8 1 7 ralrimi ( 𝜑 → ∀ 𝑘𝐴 𝐵𝑆 )
9 dfiun3g ( ∀ 𝑘𝐴 𝐵𝑆 𝑘𝐴 𝐵 = ran ( 𝑘𝐴𝐵 ) )
10 8 9 syl ( 𝜑 𝑘𝐴 𝐵 = ran ( 𝑘𝐴𝐵 ) )
11 10 fveq2d ( 𝜑 → ( 𝑀 𝑘𝐴 𝐵 ) = ( 𝑀 ran ( 𝑘𝐴𝐵 ) ) )
12 eqid ( 𝑘𝐴𝐵 ) = ( 𝑘𝐴𝐵 )
13 1 12 4 rnmptssd ( 𝜑 → ran ( 𝑘𝐴𝐵 ) ⊆ 𝑆 )
14 1stcrestlem ( 𝐴 ≼ ω → ran ( 𝑘𝐴𝐵 ) ≼ ω )
15 5 14 syl ( 𝜑 → ran ( 𝑘𝐴𝐵 ) ≼ ω )
16 12 disjrnmpt2 ( Disj 𝑘𝐴 𝐵Disj 𝑥 ∈ ran ( 𝑘𝐴𝐵 ) 𝑥 )
17 6 16 syl ( 𝜑Disj 𝑥 ∈ ran ( 𝑘𝐴𝐵 ) 𝑥 )
18 2 3 13 15 17 meadjuni ( 𝜑 → ( 𝑀 ran ( 𝑘𝐴𝐵 ) ) = ( Σ^ ‘ ( 𝑀 ↾ ran ( 𝑘𝐴𝐵 ) ) ) )
19 reldom Rel ≼
20 brrelex1 ( ( Rel ≼ ∧ 𝐴 ≼ ω ) → 𝐴 ∈ V )
21 19 20 mpan ( 𝐴 ≼ ω → 𝐴 ∈ V )
22 5 21 syl ( 𝜑𝐴 ∈ V )
23 1 4 12 fmptdf ( 𝜑 → ( 𝑘𝐴𝐵 ) : 𝐴𝑆 )
24 fveq2 ( 𝑗 = 𝑖 → ( ( 𝑘𝐴𝐵 ) ‘ 𝑗 ) = ( ( 𝑘𝐴𝐵 ) ‘ 𝑖 ) )
25 24 neeq1d ( 𝑗 = 𝑖 → ( ( ( 𝑘𝐴𝐵 ) ‘ 𝑗 ) ≠ ∅ ↔ ( ( 𝑘𝐴𝐵 ) ‘ 𝑖 ) ≠ ∅ ) )
26 25 cbvrabv { 𝑗𝐴 ∣ ( ( 𝑘𝐴𝐵 ) ‘ 𝑗 ) ≠ ∅ } = { 𝑖𝐴 ∣ ( ( 𝑘𝐴𝐵 ) ‘ 𝑖 ) ≠ ∅ }
27 simpr ( ( 𝜑𝑖𝐴 ) → 𝑖𝐴 )
28 nfv 𝑘 𝑖𝐴
29 1 28 nfan 𝑘 ( 𝜑𝑖𝐴 )
30 nfcv 𝑘 𝑖
31 30 nfcsb1 𝑘 𝑖 / 𝑘 𝐵
32 nfcv 𝑘 𝑆
33 31 32 nfel 𝑘 𝑖 / 𝑘 𝐵𝑆
34 29 33 nfim 𝑘 ( ( 𝜑𝑖𝐴 ) → 𝑖 / 𝑘 𝐵𝑆 )
35 eleq1w ( 𝑘 = 𝑖 → ( 𝑘𝐴𝑖𝐴 ) )
36 35 anbi2d ( 𝑘 = 𝑖 → ( ( 𝜑𝑘𝐴 ) ↔ ( 𝜑𝑖𝐴 ) ) )
37 csbeq1a ( 𝑘 = 𝑖𝐵 = 𝑖 / 𝑘 𝐵 )
38 37 eleq1d ( 𝑘 = 𝑖 → ( 𝐵𝑆 𝑖 / 𝑘 𝐵𝑆 ) )
39 36 38 imbi12d ( 𝑘 = 𝑖 → ( ( ( 𝜑𝑘𝐴 ) → 𝐵𝑆 ) ↔ ( ( 𝜑𝑖𝐴 ) → 𝑖 / 𝑘 𝐵𝑆 ) ) )
40 34 39 4 chvarfv ( ( 𝜑𝑖𝐴 ) → 𝑖 / 𝑘 𝐵𝑆 )
41 30 31 37 12 fvmptf ( ( 𝑖𝐴 𝑖 / 𝑘 𝐵𝑆 ) → ( ( 𝑘𝐴𝐵 ) ‘ 𝑖 ) = 𝑖 / 𝑘 𝐵 )
42 27 40 41 syl2anc ( ( 𝜑𝑖𝐴 ) → ( ( 𝑘𝐴𝐵 ) ‘ 𝑖 ) = 𝑖 / 𝑘 𝐵 )
43 42 disjeq2dv ( 𝜑 → ( Disj 𝑖𝐴 ( ( 𝑘𝐴𝐵 ) ‘ 𝑖 ) ↔ Disj 𝑖𝐴 𝑖 / 𝑘 𝐵 ) )
44 nfcv 𝑖 𝐵
45 44 31 37 cbvdisj ( Disj 𝑘𝐴 𝐵Disj 𝑖𝐴 𝑖 / 𝑘 𝐵 )
46 45 bicomi ( Disj 𝑖𝐴 𝑖 / 𝑘 𝐵Disj 𝑘𝐴 𝐵 )
47 46 a1i ( 𝜑 → ( Disj 𝑖𝐴 𝑖 / 𝑘 𝐵Disj 𝑘𝐴 𝐵 ) )
48 43 47 bitrd ( 𝜑 → ( Disj 𝑖𝐴 ( ( 𝑘𝐴𝐵 ) ‘ 𝑖 ) ↔ Disj 𝑘𝐴 𝐵 ) )
49 6 48 mpbird ( 𝜑Disj 𝑖𝐴 ( ( 𝑘𝐴𝐵 ) ‘ 𝑖 ) )
50 2 3 22 23 26 49 meadjiunlem ( 𝜑 → ( Σ^ ‘ ( 𝑀 ↾ ran ( 𝑘𝐴𝐵 ) ) ) = ( Σ^ ‘ ( 𝑀 ∘ ( 𝑘𝐴𝐵 ) ) ) )
51 44 31 37 cbvmpt ( 𝑘𝐴𝐵 ) = ( 𝑖𝐴 𝑖 / 𝑘 𝐵 )
52 51 coeq2i ( 𝑀 ∘ ( 𝑘𝐴𝐵 ) ) = ( 𝑀 ∘ ( 𝑖𝐴 𝑖 / 𝑘 𝐵 ) )
53 52 a1i ( 𝜑 → ( 𝑀 ∘ ( 𝑘𝐴𝐵 ) ) = ( 𝑀 ∘ ( 𝑖𝐴 𝑖 / 𝑘 𝐵 ) ) )
54 eqidd ( 𝜑 → ( 𝑖𝐴 𝑖 / 𝑘 𝐵 ) = ( 𝑖𝐴 𝑖 / 𝑘 𝐵 ) )
55 2 3 meaf ( 𝜑𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) )
56 55 feqmptd ( 𝜑𝑀 = ( 𝑦𝑆 ↦ ( 𝑀𝑦 ) ) )
57 fveq2 ( 𝑦 = 𝑖 / 𝑘 𝐵 → ( 𝑀𝑦 ) = ( 𝑀 𝑖 / 𝑘 𝐵 ) )
58 40 54 56 57 fmptco ( 𝜑 → ( 𝑀 ∘ ( 𝑖𝐴 𝑖 / 𝑘 𝐵 ) ) = ( 𝑖𝐴 ↦ ( 𝑀 𝑖 / 𝑘 𝐵 ) ) )
59 nfcv 𝑖 ( 𝑀𝐵 )
60 nfcv 𝑘 𝑀
61 60 31 nffv 𝑘 ( 𝑀 𝑖 / 𝑘 𝐵 )
62 37 fveq2d ( 𝑘 = 𝑖 → ( 𝑀𝐵 ) = ( 𝑀 𝑖 / 𝑘 𝐵 ) )
63 59 61 62 cbvmpt ( 𝑘𝐴 ↦ ( 𝑀𝐵 ) ) = ( 𝑖𝐴 ↦ ( 𝑀 𝑖 / 𝑘 𝐵 ) )
64 63 eqcomi ( 𝑖𝐴 ↦ ( 𝑀 𝑖 / 𝑘 𝐵 ) ) = ( 𝑘𝐴 ↦ ( 𝑀𝐵 ) )
65 64 a1i ( 𝜑 → ( 𝑖𝐴 ↦ ( 𝑀 𝑖 / 𝑘 𝐵 ) ) = ( 𝑘𝐴 ↦ ( 𝑀𝐵 ) ) )
66 53 58 65 3eqtrd ( 𝜑 → ( 𝑀 ∘ ( 𝑘𝐴𝐵 ) ) = ( 𝑘𝐴 ↦ ( 𝑀𝐵 ) ) )
67 66 fveq2d ( 𝜑 → ( Σ^ ‘ ( 𝑀 ∘ ( 𝑘𝐴𝐵 ) ) ) = ( Σ^ ‘ ( 𝑘𝐴 ↦ ( 𝑀𝐵 ) ) ) )
68 50 67 eqtrd ( 𝜑 → ( Σ^ ‘ ( 𝑀 ↾ ran ( 𝑘𝐴𝐵 ) ) ) = ( Σ^ ‘ ( 𝑘𝐴 ↦ ( 𝑀𝐵 ) ) ) )
69 11 18 68 3eqtrd ( 𝜑 → ( 𝑀 𝑘𝐴 𝐵 ) = ( Σ^ ‘ ( 𝑘𝐴 ↦ ( 𝑀𝐵 ) ) ) )