Metamath Proof Explorer

Theorem measvuni

Description: The measure of a countable disjoint union is the sum of the measures. This theorem uses a collection rather than a set of subsets of S . (Contributed by Thierry Arnoux, 7-Mar-2017)

Ref Expression
Assertion measvuni ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→M⁡⋃x∈AB=∑*x∈AM⁡B

Proof

Step Hyp Ref Expression
1 simp1 ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→M∈measures⁡S
2 rabid ⊢x∈x∈A|B∈∅↔x∈A∧B∈∅
3 2 simprbi ⊢x∈x∈A|B∈∅→B∈∅
4 3 adantl ⊢M∈measures⁡S∧x∈x∈A|B∈∅→B∈∅
5 4 ralrimiva ⊢M∈measures⁡S→∀x∈x∈A|B∈∅B∈∅
6 5 3ad2ant1 ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→∀x∈x∈A|B∈∅B∈∅
7 ssrab2 ⊢x∈A|B∈∅⊆A
8 ssct ⊢x∈A|B∈∅⊆A∧A≼ω→x∈A|B∈∅≼ω
9 7 8 mpan ⊢A≼ω→x∈A|B∈∅≼ω
10 9 adantr ⊢A≼ω∧Disjx∈AB→x∈A|B∈∅≼ω
11 10 3ad2ant3 ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→x∈A|B∈∅≼ω
12 simp3r ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→Disjx∈AB
13 nfrab1 ⊢Ⅎ_xx∈A|B∈∅
14 nfcv ⊢Ⅎ_xA
15 13 14 disjss1f ⊢x∈A|B∈∅⊆A→Disjx∈AB→Disjx∈x∈A|B∈∅B
16 7 12 15 mpsyl ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→Disjx∈x∈A|B∈∅B
17 13 measvunilem0 ⊢M∈measures⁡S∧∀x∈x∈A|B∈∅B∈∅∧x∈A|B∈∅≼ω∧Disjx∈x∈A|B∈∅B→M⁡⋃x∈x∈A|B∈∅B=∑*x∈x∈A|B∈∅M⁡B
18 1 6 11 16 17 syl112anc ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→M⁡⋃x∈x∈A|B∈∅B=∑*x∈x∈A|B∈∅M⁡B
19 rabid ⊢x∈x∈A|B∈S∖∅↔x∈A∧B∈S∖∅
20 19 simprbi ⊢x∈x∈A|B∈S∖∅→B∈S∖∅
21 20 adantl ⊢M∈measures⁡S∧x∈x∈A|B∈S∖∅→B∈S∖∅
22 21 ralrimiva ⊢M∈measures⁡S→∀x∈x∈A|B∈S∖∅B∈S∖∅
23 22 3ad2ant1 ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→∀x∈x∈A|B∈S∖∅B∈S∖∅
24 ssrab2 ⊢x∈A|B∈S∖∅⊆A
25 ssct ⊢x∈A|B∈S∖∅⊆A∧A≼ω→x∈A|B∈S∖∅≼ω
26 24 25 mpan ⊢A≼ω→x∈A|B∈S∖∅≼ω
27 26 adantr ⊢A≼ω∧Disjx∈AB→x∈A|B∈S∖∅≼ω
28 27 3ad2ant3 ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→x∈A|B∈S∖∅≼ω
29 nfrab1 ⊢Ⅎ_xx∈A|B∈S∖∅
30 29 14 disjss1f ⊢x∈A|B∈S∖∅⊆A→Disjx∈AB→Disjx∈x∈A|B∈S∖∅B
31 24 12 30 mpsyl ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→Disjx∈x∈A|B∈S∖∅B
32 29 measvunilem ⊢M∈measures⁡S∧∀x∈x∈A|B∈S∖∅B∈S∖∅∧x∈A|B∈S∖∅≼ω∧Disjx∈x∈A|B∈S∖∅B→M⁡⋃x∈x∈A|B∈S∖∅B=∑*x∈x∈A|B∈S∖∅M⁡B
33 1 23 28 31 32 syl112anc ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→M⁡⋃x∈x∈A|B∈S∖∅B=∑*x∈x∈A|B∈S∖∅M⁡B
34 18 33 oveq12d ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→M⁡⋃x∈x∈A|B∈∅B+𝑒M⁡⋃x∈x∈A|B∈S∖∅B=∑*x∈x∈A|B∈∅M⁡B+𝑒∑*x∈x∈A|B∈S∖∅M⁡B
35 nfv ⊢ℲxM∈measures⁡S
36 nfra1 ⊢Ⅎx∀x∈AB∈S
37 nfv ⊢ℲxA≼ω
38 nfdisj1 ⊢ℲxDisjx∈AB
39 37 38 nfan ⊢ℲxA≼ω∧Disjx∈AB
40 35 36 39 nf3an ⊢ℲxM∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB
41 13 29 nfun ⊢Ⅎ_xx∈A|B∈∅∪x∈A|B∈S∖∅
42 simp2 ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→∀x∈AB∈S
43 rabid2 ⊢A=x∈A|B∈S↔∀x∈AB∈S
44 42 43 sylibr ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→A=x∈A|B∈S
45 elun ⊢B∈∅∪S∖∅↔B∈∅∨B∈S∖∅
46 measbase ⊢M∈measures⁡S→S∈⋃ran⁡sigAlgebra
47 0elsiga ⊢S∈⋃ran⁡sigAlgebra→∅∈S
48 snssi ⊢∅∈S→∅⊆S
49 46 47 48 3syl ⊢M∈measures⁡S→∅⊆S
50 undif ⊢∅⊆S↔∅∪S∖∅=S
51 49 50 sylib ⊢M∈measures⁡S→∅∪S∖∅=S
52 51 eleq2d ⊢M∈measures⁡S→B∈∅∪S∖∅↔B∈S
53 45 52 bitr3id ⊢M∈measures⁡S→B∈∅∨B∈S∖∅↔B∈S
54 53 rabbidv ⊢M∈measures⁡S→x∈A|B∈∅∨B∈S∖∅=x∈A|B∈S
55 54 3ad2ant1 ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→x∈A|B∈∅∨B∈S∖∅=x∈A|B∈S
56 44 55 eqtr4d ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→A=x∈A|B∈∅∨B∈S∖∅
57 unrab ⊢x∈A|B∈∅∪x∈A|B∈S∖∅=x∈A|B∈∅∨B∈S∖∅
58 56 57 eqtr4di ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→A=x∈A|B∈∅∪x∈A|B∈S∖∅
59 eqidd ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→B=B
60 40 14 41 58 59 iuneq12df ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→⋃x∈AB=⋃x∈x∈A|B∈∅∪x∈A|B∈S∖∅B
61 60 fveq2d ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→M⁡⋃x∈AB=M⁡⋃x∈x∈A|B∈∅∪x∈A|B∈S∖∅B
62 iunxun ⊢⋃x∈x∈A|B∈∅∪x∈A|B∈S∖∅B=⋃x∈x∈A|B∈∅B∪⋃x∈x∈A|B∈S∖∅B
63 62 fveq2i ⊢M⁡⋃x∈x∈A|B∈∅∪x∈A|B∈S∖∅B=M⁡⋃x∈x∈A|B∈∅B∪⋃x∈x∈A|B∈S∖∅B
64 61 63 eqtrdi ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→M⁡⋃x∈AB=M⁡⋃x∈x∈A|B∈∅B∪⋃x∈x∈A|B∈S∖∅B
65 46 3ad2ant1 ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→S∈⋃ran⁡sigAlgebra
66 47 adantr ⊢S∈⋃ran⁡sigAlgebra∧B∈∅→∅∈S
67 elsni ⊢B∈∅→B=∅
68 67 eleq1d ⊢B∈∅→B∈S↔∅∈S
69 68 adantl ⊢S∈⋃ran⁡sigAlgebra∧B∈∅→B∈S↔∅∈S
70 66 69 mpbird ⊢S∈⋃ran⁡sigAlgebra∧B∈∅→B∈S
71 46 3 70 syl2an ⊢M∈measures⁡S∧x∈x∈A|B∈∅→B∈S
72 71 ralrimiva ⊢M∈measures⁡S→∀x∈x∈A|B∈∅B∈S
73 72 3ad2ant1 ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→∀x∈x∈A|B∈∅B∈S
74 13 sigaclcuni ⊢S∈⋃ran⁡sigAlgebra∧∀x∈x∈A|B∈∅B∈S∧x∈A|B∈∅≼ω→⋃x∈x∈A|B∈∅B∈S
75 65 73 11 74 syl3anc ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→⋃x∈x∈A|B∈∅B∈S
76 21 eldifad ⊢M∈measures⁡S∧x∈x∈A|B∈S∖∅→B∈S
77 76 ralrimiva ⊢M∈measures⁡S→∀x∈x∈A|B∈S∖∅B∈S
78 77 3ad2ant1 ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→∀x∈x∈A|B∈S∖∅B∈S
79 29 sigaclcuni ⊢S∈⋃ran⁡sigAlgebra∧∀x∈x∈A|B∈S∖∅B∈S∧x∈A|B∈S∖∅≼ω→⋃x∈x∈A|B∈S∖∅B∈S
80 65 78 28 79 syl3anc ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→⋃x∈x∈A|B∈S∖∅B∈S
81 3 67 syl ⊢x∈x∈A|B∈∅→B=∅
82 81 iuneq2i ⊢⋃x∈x∈A|B∈∅B=⋃x∈x∈A|B∈∅∅
83 iun0 ⊢⋃x∈x∈A|B∈∅∅=∅
84 82 83 eqtri ⊢⋃x∈x∈A|B∈∅B=∅
85 ineq1 ⊢⋃x∈x∈A|B∈∅B=∅→⋃x∈x∈A|B∈∅B∩⋃x∈x∈A|B∈S∖∅B=∅∩⋃x∈x∈A|B∈S∖∅B
86 0in ⊢∅∩⋃x∈x∈A|B∈S∖∅B=∅
87 85 86 eqtrdi ⊢⋃x∈x∈A|B∈∅B=∅→⋃x∈x∈A|B∈∅B∩⋃x∈x∈A|B∈S∖∅B=∅
88 84 87 mp1i ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→⋃x∈x∈A|B∈∅B∩⋃x∈x∈A|B∈S∖∅B=∅
89 measun ⊢M∈measures⁡S∧⋃x∈x∈A|B∈∅B∈S∧⋃x∈x∈A|B∈S∖∅B∈S∧⋃x∈x∈A|B∈∅B∩⋃x∈x∈A|B∈S∖∅B=∅→M⁡⋃x∈x∈A|B∈∅B∪⋃x∈x∈A|B∈S∖∅B=M⁡⋃x∈x∈A|B∈∅B+𝑒M⁡⋃x∈x∈A|B∈S∖∅B
90 1 75 80 88 89 syl121anc ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→M⁡⋃x∈x∈A|B∈∅B∪⋃x∈x∈A|B∈S∖∅B=M⁡⋃x∈x∈A|B∈∅B+𝑒M⁡⋃x∈x∈A|B∈S∖∅B
91 64 90 eqtrd ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→M⁡⋃x∈AB=M⁡⋃x∈x∈A|B∈∅B+𝑒M⁡⋃x∈x∈A|B∈S∖∅B
92 40 58 esumeq1d ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→∑*x∈AM⁡B=∑*x∈x∈A|B∈∅∪x∈A|B∈S∖∅M⁡B
93 ctex ⊢x∈A|B∈∅≼ω→x∈A|B∈∅∈V
94 11 93 syl ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→x∈A|B∈∅∈V
95 ctex ⊢x∈A|B∈S∖∅≼ω→x∈A|B∈S∖∅∈V
96 28 95 syl ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→x∈A|B∈S∖∅∈V
97 inrab ⊢x∈A|B∈∅∩x∈A|B∈S∖∅=x∈A|B∈∅∧B∈S∖∅
98 noel ⊢¬B∈∅
99 disjdif ⊢∅∩S∖∅=∅
100 99 eleq2i ⊢B∈∅∩S∖∅↔B∈∅
101 98 100 mtbir ⊢¬B∈∅∩S∖∅
102 elin ⊢B∈∅∩S∖∅↔B∈∅∧B∈S∖∅
103 101 102 mtbi ⊢¬B∈∅∧B∈S∖∅
104 103 rgenw ⊢∀x∈A¬B∈∅∧B∈S∖∅
105 rabeq0 ⊢x∈A|B∈∅∧B∈S∖∅=∅↔∀x∈A¬B∈∅∧B∈S∖∅
106 104 105 mpbir ⊢x∈A|B∈∅∧B∈S∖∅=∅
107 97 106 eqtri ⊢x∈A|B∈∅∩x∈A|B∈S∖∅=∅
108 107 a1i ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→x∈A|B∈∅∩x∈A|B∈S∖∅=∅
109 1 adantr ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB∧x∈x∈A|B∈∅→M∈measures⁡S
110 1 71 sylan ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB∧x∈x∈A|B∈∅→B∈S
111 measvxrge0 ⊢M∈measures⁡S∧B∈S→M⁡B∈0+∞
112 109 110 111 syl2anc ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB∧x∈x∈A|B∈∅→M⁡B∈0+∞
113 1 adantr ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB∧x∈x∈A|B∈S∖∅→M∈measures⁡S
114 20 adantl ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB∧x∈x∈A|B∈S∖∅→B∈S∖∅
115 114 eldifad ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB∧x∈x∈A|B∈S∖∅→B∈S
116 113 115 111 syl2anc ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB∧x∈x∈A|B∈S∖∅→M⁡B∈0+∞
117 40 13 29 94 96 108 112 116 esumsplit ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→∑*x∈x∈A|B∈∅∪x∈A|B∈S∖∅M⁡B=∑*x∈x∈A|B∈∅M⁡B+𝑒∑*x∈x∈A|B∈S∖∅M⁡B
118 92 117 eqtrd ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→∑*x∈AM⁡B=∑*x∈x∈A|B∈∅M⁡B+𝑒∑*x∈x∈A|B∈S∖∅M⁡B
119 34 91 118 3eqtr4d ⊢M∈measures⁡S∧∀x∈AB∈S∧A≼ω∧Disjx∈AB→M⁡⋃x∈AB=∑*x∈AM⁡B