# 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 ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to {M}\left(\bigcup _{{x}\in {A}}{B}\right)=\underset{{x}\in {A}}{{\sum }^{*}}{M}\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 simp1 ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to {M}\in \mathrm{measures}\left({S}\right)$
2 rabid ${⊢}{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}↔\left({x}\in {A}\wedge {B}\in \left\{\varnothing \right\}\right)$
3 2 simprbi ${⊢}{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\to {B}\in \left\{\varnothing \right\}$
4 3 adantl ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge {x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\right)\to {B}\in \left\{\varnothing \right\}$
5 4 ralrimiva ${⊢}{M}\in \mathrm{measures}\left({S}\right)\to \forall {x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\phantom{\rule{.4em}{0ex}}{B}\in \left\{\varnothing \right\}$
6 5 3ad2ant1 ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to \forall {x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\phantom{\rule{.4em}{0ex}}{B}\in \left\{\varnothing \right\}$
7 ssrab2 ${⊢}\left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\subseteq {A}$
8 ssct ${⊢}\left(\left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\subseteq {A}\wedge {A}\preccurlyeq \mathrm{\omega }\right)\to \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\preccurlyeq \mathrm{\omega }$
9 7 8 mpan ${⊢}{A}\preccurlyeq \mathrm{\omega }\to \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\preccurlyeq \mathrm{\omega }$
10 9 adantr ${⊢}\left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\to \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\preccurlyeq \mathrm{\omega }$
11 10 3ad2ant3 ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\preccurlyeq \mathrm{\omega }$
12 simp3r ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to \underset{{x}\in {A}}{Disj}{B}$
13 nfrab1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}$
14 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
15 13 14 disjss1f ${⊢}\left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\subseteq {A}\to \left(\underset{{x}\in {A}}{Disj}{B}\to \underset{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}}{Disj}{B}\right)$
16 7 12 15 mpsyl ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to \underset{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}}{Disj}{B}$
17 13 measvunilem0 ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\phantom{\rule{.4em}{0ex}}{B}\in \left\{\varnothing \right\}\wedge \left(\left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}}{Disj}{B}\right)\right)\to {M}\left(\bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}}{B}\right)=\underset{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}}{{\sum }^{*}}{M}\left({B}\right)$
18 1 6 11 16 17 syl112anc ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to {M}\left(\bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}}{B}\right)=\underset{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}}{{\sum }^{*}}{M}\left({B}\right)$
19 rabid ${⊢}{x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}↔\left({x}\in {A}\wedge {B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right)$
20 19 simprbi ${⊢}{x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}\to {B}\in \left({S}\setminus \left\{\varnothing \right\}\right)$
21 20 adantl ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge {x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}\right)\to {B}\in \left({S}\setminus \left\{\varnothing \right\}\right)$
22 21 ralrimiva ${⊢}{M}\in \mathrm{measures}\left({S}\right)\to \forall {x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}\phantom{\rule{.4em}{0ex}}{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)$
23 22 3ad2ant1 ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to \forall {x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}\phantom{\rule{.4em}{0ex}}{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)$
24 ssrab2 ${⊢}\left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}\subseteq {A}$
25 ssct ${⊢}\left(\left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}\subseteq {A}\wedge {A}\preccurlyeq \mathrm{\omega }\right)\to \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}\preccurlyeq \mathrm{\omega }$
26 24 25 mpan ${⊢}{A}\preccurlyeq \mathrm{\omega }\to \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}\preccurlyeq \mathrm{\omega }$
27 26 adantr ${⊢}\left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\to \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}\preccurlyeq \mathrm{\omega }$
28 27 3ad2ant3 ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}\preccurlyeq \mathrm{\omega }$
29 nfrab1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}$
30 29 14 disjss1f ${⊢}\left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}\subseteq {A}\to \left(\underset{{x}\in {A}}{Disj}{B}\to \underset{{x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{Disj}{B}\right)$
31 24 12 30 mpsyl ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to \underset{{x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{Disj}{B}$
32 29 measvunilem ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}\phantom{\rule{.4em}{0ex}}{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\wedge \left(\left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{Disj}{B}\right)\right)\to {M}\left(\bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{B}\right)=\underset{{x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{{\sum }^{*}}{M}\left({B}\right)$
33 1 23 28 31 32 syl112anc ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to {M}\left(\bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{B}\right)=\underset{{x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{{\sum }^{*}}{M}\left({B}\right)$
34 18 33 oveq12d ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to {M}\left(\bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}}{B}\right){+}_{𝑒}{M}\left(\bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{B}\right)=\underset{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}}{{\sum }^{*}}{M}\left({B}\right){+}_{𝑒}\underset{{x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{{\sum }^{*}}{M}\left({B}\right)$
35 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{M}\in \mathrm{measures}\left({S}\right)$
36 nfra1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}$
37 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{A}\preccurlyeq \mathrm{\omega }$
38 nfdisj1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\underset{{x}\in {A}}{Disj}{B}$
39 37 38 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)$
40 35 36 39 nf3an ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)$
41 13 29 nfun ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left(\left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\cup \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}\right)$
42 simp2 ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}$
43 rabid2 ${⊢}{A}=\left\{{x}\in {A}|{B}\in {S}\right\}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}$
44 42 43 sylibr ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to {A}=\left\{{x}\in {A}|{B}\in {S}\right\}$
45 elun ${⊢}{B}\in \left(\left\{\varnothing \right\}\cup \left({S}\setminus \left\{\varnothing \right\}\right)\right)↔\left({B}\in \left\{\varnothing \right\}\vee {B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right)$
46 measbase ${⊢}{M}\in \mathrm{measures}\left({S}\right)\to {S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
47 0elsiga ${⊢}{S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \varnothing \in {S}$
48 snssi ${⊢}\varnothing \in {S}\to \left\{\varnothing \right\}\subseteq {S}$
49 46 47 48 3syl ${⊢}{M}\in \mathrm{measures}\left({S}\right)\to \left\{\varnothing \right\}\subseteq {S}$
50 undif ${⊢}\left\{\varnothing \right\}\subseteq {S}↔\left\{\varnothing \right\}\cup \left({S}\setminus \left\{\varnothing \right\}\right)={S}$
51 49 50 sylib ${⊢}{M}\in \mathrm{measures}\left({S}\right)\to \left\{\varnothing \right\}\cup \left({S}\setminus \left\{\varnothing \right\}\right)={S}$
52 51 eleq2d ${⊢}{M}\in \mathrm{measures}\left({S}\right)\to \left({B}\in \left(\left\{\varnothing \right\}\cup \left({S}\setminus \left\{\varnothing \right\}\right)\right)↔{B}\in {S}\right)$
53 45 52 syl5bbr ${⊢}{M}\in \mathrm{measures}\left({S}\right)\to \left(\left({B}\in \left\{\varnothing \right\}\vee {B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right)↔{B}\in {S}\right)$
54 53 rabbidv ${⊢}{M}\in \mathrm{measures}\left({S}\right)\to \left\{{x}\in {A}|\left({B}\in \left\{\varnothing \right\}\vee {B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right)\right\}=\left\{{x}\in {A}|{B}\in {S}\right\}$
55 54 3ad2ant1 ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to \left\{{x}\in {A}|\left({B}\in \left\{\varnothing \right\}\vee {B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right)\right\}=\left\{{x}\in {A}|{B}\in {S}\right\}$
56 44 55 eqtr4d ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to {A}=\left\{{x}\in {A}|\left({B}\in \left\{\varnothing \right\}\vee {B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right)\right\}$
57 unrab ${⊢}\left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\cup \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}=\left\{{x}\in {A}|\left({B}\in \left\{\varnothing \right\}\vee {B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right)\right\}$
58 56 57 syl6eqr ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to {A}=\left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\cup \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}$
59 eqidd ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to {B}={B}$
60 40 14 41 58 59 iuneq12df ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to \bigcup _{{x}\in {A}}{B}=\bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\cup \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{B}$
61 60 fveq2d ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to {M}\left(\bigcup _{{x}\in {A}}{B}\right)={M}\left(\bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\cup \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{B}\right)$
62 iunxun ${⊢}\bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\cup \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{B}=\bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}}{B}\cup \bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{B}$
63 62 fveq2i ${⊢}{M}\left(\bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\cup \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{B}\right)={M}\left(\bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}}{B}\cup \bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{B}\right)$
64 61 63 syl6eq ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to {M}\left(\bigcup _{{x}\in {A}}{B}\right)={M}\left(\bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}}{B}\cup \bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{B}\right)$
65 46 3ad2ant1 ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to {S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
66 47 adantr ${⊢}\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge {B}\in \left\{\varnothing \right\}\right)\to \varnothing \in {S}$
67 elsni ${⊢}{B}\in \left\{\varnothing \right\}\to {B}=\varnothing$
68 67 eleq1d ${⊢}{B}\in \left\{\varnothing \right\}\to \left({B}\in {S}↔\varnothing \in {S}\right)$
69 68 adantl ${⊢}\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge {B}\in \left\{\varnothing \right\}\right)\to \left({B}\in {S}↔\varnothing \in {S}\right)$
70 66 69 mpbird ${⊢}\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge {B}\in \left\{\varnothing \right\}\right)\to {B}\in {S}$
71 46 3 70 syl2an ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge {x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\right)\to {B}\in {S}$
72 71 ralrimiva ${⊢}{M}\in \mathrm{measures}\left({S}\right)\to \forall {x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\phantom{\rule{.4em}{0ex}}{B}\in {S}$
73 72 3ad2ant1 ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to \forall {x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\phantom{\rule{.4em}{0ex}}{B}\in {S}$
74 13 sigaclcuni ${⊢}\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge \forall {x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\preccurlyeq \mathrm{\omega }\right)\to \bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}}{B}\in {S}$
75 65 73 11 74 syl3anc ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to \bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}}{B}\in {S}$
76 21 eldifad ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge {x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}\right)\to {B}\in {S}$
77 76 ralrimiva ${⊢}{M}\in \mathrm{measures}\left({S}\right)\to \forall {x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}\phantom{\rule{.4em}{0ex}}{B}\in {S}$
78 77 3ad2ant1 ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to \forall {x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}\phantom{\rule{.4em}{0ex}}{B}\in {S}$
79 29 sigaclcuni ${⊢}\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge \forall {x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}\preccurlyeq \mathrm{\omega }\right)\to \bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{B}\in {S}$
80 65 78 28 79 syl3anc ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to \bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{B}\in {S}$
81 3 67 syl ${⊢}{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\to {B}=\varnothing$
82 81 iuneq2i ${⊢}\bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}}{B}=\bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}}\varnothing$
83 iun0 ${⊢}\bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}}\varnothing =\varnothing$
84 82 83 eqtri ${⊢}\bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}}{B}=\varnothing$
85 ineq1 ${⊢}\bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}}{B}=\varnothing \to \bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}}{B}\cap \bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{B}=\varnothing \cap \bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{B}$
86 0in ${⊢}\varnothing \cap \bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{B}=\varnothing$
87 85 86 syl6eq ${⊢}\bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}}{B}=\varnothing \to \bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}}{B}\cap \bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{B}=\varnothing$
88 84 87 mp1i ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to \bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}}{B}\cap \bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{B}=\varnothing$
89 measun ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \left(\bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}}{B}\in {S}\wedge \bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{B}\in {S}\right)\wedge \bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}}{B}\cap \bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{B}=\varnothing \right)\to {M}\left(\bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}}{B}\cup \bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{B}\right)={M}\left(\bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}}{B}\right){+}_{𝑒}{M}\left(\bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{B}\right)$
90 1 75 80 88 89 syl121anc ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to {M}\left(\bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}}{B}\cup \bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{B}\right)={M}\left(\bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}}{B}\right){+}_{𝑒}{M}\left(\bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{B}\right)$
91 64 90 eqtrd ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to {M}\left(\bigcup _{{x}\in {A}}{B}\right)={M}\left(\bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}}{B}\right){+}_{𝑒}{M}\left(\bigcup _{{x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{B}\right)$
92 40 58 esumeq1d ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to \underset{{x}\in {A}}{{\sum }^{*}}{M}\left({B}\right)=\underset{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\cup \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{{\sum }^{*}}{M}\left({B}\right)$
93 ctex ${⊢}\left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\preccurlyeq \mathrm{\omega }\to \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\in \mathrm{V}$
94 11 93 syl ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\in \mathrm{V}$
95 ctex ${⊢}\left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}\preccurlyeq \mathrm{\omega }\to \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}\in \mathrm{V}$
96 28 95 syl ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}\in \mathrm{V}$
97 inrab ${⊢}\left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\cap \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}=\left\{{x}\in {A}|\left({B}\in \left\{\varnothing \right\}\wedge {B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right)\right\}$
98 noel ${⊢}¬{B}\in \varnothing$
99 disjdif ${⊢}\left\{\varnothing \right\}\cap \left({S}\setminus \left\{\varnothing \right\}\right)=\varnothing$
100 99 eleq2i ${⊢}{B}\in \left(\left\{\varnothing \right\}\cap \left({S}\setminus \left\{\varnothing \right\}\right)\right)↔{B}\in \varnothing$
101 98 100 mtbir ${⊢}¬{B}\in \left(\left\{\varnothing \right\}\cap \left({S}\setminus \left\{\varnothing \right\}\right)\right)$
102 elin ${⊢}{B}\in \left(\left\{\varnothing \right\}\cap \left({S}\setminus \left\{\varnothing \right\}\right)\right)↔\left({B}\in \left\{\varnothing \right\}\wedge {B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right)$
103 101 102 mtbi ${⊢}¬\left({B}\in \left\{\varnothing \right\}\wedge {B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right)$
104 103 rgenw ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬\left({B}\in \left\{\varnothing \right\}\wedge {B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right)$
105 rabeq0 ${⊢}\left\{{x}\in {A}|\left({B}\in \left\{\varnothing \right\}\wedge {B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right)\right\}=\varnothing ↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬\left({B}\in \left\{\varnothing \right\}\wedge {B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right)$
106 104 105 mpbir ${⊢}\left\{{x}\in {A}|\left({B}\in \left\{\varnothing \right\}\wedge {B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right)\right\}=\varnothing$
107 97 106 eqtri ${⊢}\left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\cap \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}=\varnothing$
108 107 a1i ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\cap \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}=\varnothing$
109 1 adantr ${⊢}\left(\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\wedge {x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\right)\to {M}\in \mathrm{measures}\left({S}\right)$
110 1 71 sylan ${⊢}\left(\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\wedge {x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\right)\to {B}\in {S}$
111 measvxrge0 ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge {B}\in {S}\right)\to {M}\left({B}\right)\in \left[0,\mathrm{+\infty }\right]$
112 109 110 111 syl2anc ${⊢}\left(\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\wedge {x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\right)\to {M}\left({B}\right)\in \left[0,\mathrm{+\infty }\right]$
113 1 adantr ${⊢}\left(\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\wedge {x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}\right)\to {M}\in \mathrm{measures}\left({S}\right)$
114 20 adantl ${⊢}\left(\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\wedge {x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}\right)\to {B}\in \left({S}\setminus \left\{\varnothing \right\}\right)$
115 114 eldifad ${⊢}\left(\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\wedge {x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}\right)\to {B}\in {S}$
116 113 115 111 syl2anc ${⊢}\left(\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\wedge {x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}\right)\to {M}\left({B}\right)\in \left[0,\mathrm{+\infty }\right]$
117 40 13 29 94 96 108 112 116 esumsplit ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to \underset{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}\cup \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{{\sum }^{*}}{M}\left({B}\right)=\underset{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}}{{\sum }^{*}}{M}\left({B}\right){+}_{𝑒}\underset{{x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{{\sum }^{*}}{M}\left({B}\right)$
118 92 117 eqtrd ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to \underset{{x}\in {A}}{{\sum }^{*}}{M}\left({B}\right)=\underset{{x}\in \left\{{x}\in {A}|{B}\in \left\{\varnothing \right\}\right\}}{{\sum }^{*}}{M}\left({B}\right){+}_{𝑒}\underset{{x}\in \left\{{x}\in {A}|{B}\in \left({S}\setminus \left\{\varnothing \right\}\right)\right\}}{{\sum }^{*}}{M}\left({B}\right)$
119 34 91 118 3eqtr4d ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{B}\right)\right)\to {M}\left(\bigcup _{{x}\in {A}}{B}\right)=\underset{{x}\in {A}}{{\sum }^{*}}{M}\left({B}\right)$