# Metamath Proof Explorer

## Theorem carsgclctunlem2

Description: Lemma for carsgclctun . (Contributed by Thierry Arnoux, 25-May-2020)

Ref Expression
Hypotheses carsgval.1 ${⊢}{\phi }\to {O}\in {V}$
carsgval.2 ${⊢}{\phi }\to {M}:𝒫{O}⟶\left[0,\mathrm{+\infty }\right]$
carsgsiga.1 ${⊢}{\phi }\to {M}\left(\varnothing \right)=0$
carsgsiga.2 ${⊢}\left({\phi }\wedge {x}\preccurlyeq \mathrm{\omega }\wedge {x}\subseteq 𝒫{O}\right)\to {M}\left(\bigcup {x}\right)\le \underset{{y}\in {x}}{{\sum }^{*}}{M}\left({y}\right)$
carsgsiga.3 ${⊢}\left({\phi }\wedge {x}\subseteq {y}\wedge {y}\in 𝒫{O}\right)\to {M}\left({x}\right)\le {M}\left({y}\right)$
carsgclctunlem2.1 ${⊢}{\phi }\to \underset{{k}\in ℕ}{Disj}{A}$
carsgclctunlem2.2 ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {A}\in \mathrm{toCaraSiga}\left({M}\right)$
carsgclctunlem2.3 ${⊢}{\phi }\to {E}\in 𝒫{O}$
carsgclctunlem2.4 ${⊢}{\phi }\to {M}\left({E}\right)\ne \mathrm{+\infty }$
Assertion carsgclctunlem2 ${⊢}{\phi }\to {M}\left({E}\cap \bigcup _{{k}\in ℕ}{A}\right){+}_{𝑒}{M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\le {M}\left({E}\right)$

### Proof

Step Hyp Ref Expression
1 carsgval.1 ${⊢}{\phi }\to {O}\in {V}$
2 carsgval.2 ${⊢}{\phi }\to {M}:𝒫{O}⟶\left[0,\mathrm{+\infty }\right]$
3 carsgsiga.1 ${⊢}{\phi }\to {M}\left(\varnothing \right)=0$
4 carsgsiga.2 ${⊢}\left({\phi }\wedge {x}\preccurlyeq \mathrm{\omega }\wedge {x}\subseteq 𝒫{O}\right)\to {M}\left(\bigcup {x}\right)\le \underset{{y}\in {x}}{{\sum }^{*}}{M}\left({y}\right)$
5 carsgsiga.3 ${⊢}\left({\phi }\wedge {x}\subseteq {y}\wedge {y}\in 𝒫{O}\right)\to {M}\left({x}\right)\le {M}\left({y}\right)$
6 carsgclctunlem2.1 ${⊢}{\phi }\to \underset{{k}\in ℕ}{Disj}{A}$
7 carsgclctunlem2.2 ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {A}\in \mathrm{toCaraSiga}\left({M}\right)$
8 carsgclctunlem2.3 ${⊢}{\phi }\to {E}\in 𝒫{O}$
9 carsgclctunlem2.4 ${⊢}{\phi }\to {M}\left({E}\right)\ne \mathrm{+\infty }$
10 iunin2 ${⊢}\bigcup _{{k}\in ℕ}\left({E}\cap {A}\right)={E}\cap \bigcup _{{k}\in ℕ}{A}$
11 10 fveq2i ${⊢}{M}\left(\bigcup _{{k}\in ℕ}\left({E}\cap {A}\right)\right)={M}\left({E}\cap \bigcup _{{k}\in ℕ}{A}\right)$
12 iccssxr ${⊢}\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}$
13 nnex ${⊢}ℕ\in \mathrm{V}$
14 13 a1i ${⊢}{\phi }\to ℕ\in \mathrm{V}$
15 8 adantr ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {E}\in 𝒫{O}$
16 15 elpwincl1 ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {E}\cap {A}\in 𝒫{O}$
17 14 16 elpwiuncl ${⊢}{\phi }\to \bigcup _{{k}\in ℕ}\left({E}\cap {A}\right)\in 𝒫{O}$
18 2 17 ffvelrnd ${⊢}{\phi }\to {M}\left(\bigcup _{{k}\in ℕ}\left({E}\cap {A}\right)\right)\in \left[0,\mathrm{+\infty }\right]$
19 12 18 sseldi ${⊢}{\phi }\to {M}\left(\bigcup _{{k}\in ℕ}\left({E}\cap {A}\right)\right)\in {ℝ}^{*}$
20 11 19 eqeltrrid ${⊢}{\phi }\to {M}\left({E}\cap \bigcup _{{k}\in ℕ}{A}\right)\in {ℝ}^{*}$
21 2 8 ffvelrnd ${⊢}{\phi }\to {M}\left({E}\right)\in \left[0,\mathrm{+\infty }\right]$
22 12 21 sseldi ${⊢}{\phi }\to {M}\left({E}\right)\in {ℝ}^{*}$
23 8 elpwdifcl ${⊢}{\phi }\to {E}\setminus \bigcup _{{k}\in ℕ}{A}\in 𝒫{O}$
24 2 23 ffvelrnd ${⊢}{\phi }\to {M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\in \left[0,\mathrm{+\infty }\right]$
25 12 24 sseldi ${⊢}{\phi }\to {M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\in {ℝ}^{*}$
26 25 xnegcld ${⊢}{\phi }\to -{M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\in {ℝ}^{*}$
27 22 26 xaddcld ${⊢}{\phi }\to {M}\left({E}\right){+}_{𝑒}\left(-{M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\right)\in {ℝ}^{*}$
28 2 adantr ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {M}:𝒫{O}⟶\left[0,\mathrm{+\infty }\right]$
29 28 16 ffvelrnd ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {M}\left({E}\cap {A}\right)\in \left[0,\mathrm{+\infty }\right]$
30 29 ralrimiva ${⊢}{\phi }\to \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{M}\left({E}\cap {A}\right)\in \left[0,\mathrm{+\infty }\right]$
31 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}ℕ$
32 31 esumcl ${⊢}\left(ℕ\in \mathrm{V}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{M}\left({E}\cap {A}\right)\in \left[0,\mathrm{+\infty }\right]\right)\to \underset{{k}\in ℕ}{{\sum }^{*}}{M}\left({E}\cap {A}\right)\in \left[0,\mathrm{+\infty }\right]$
33 14 30 32 syl2anc ${⊢}{\phi }\to \underset{{k}\in ℕ}{{\sum }^{*}}{M}\left({E}\cap {A}\right)\in \left[0,\mathrm{+\infty }\right]$
34 12 33 sseldi ${⊢}{\phi }\to \underset{{k}\in ℕ}{{\sum }^{*}}{M}\left({E}\cap {A}\right)\in {ℝ}^{*}$
35 16 ralrimiva ${⊢}{\phi }\to \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{E}\cap {A}\in 𝒫{O}$
36 dfiun3g ${⊢}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{E}\cap {A}\in 𝒫{O}\to \bigcup _{{k}\in ℕ}\left({E}\cap {A}\right)=\bigcup \mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)$
37 35 36 syl ${⊢}{\phi }\to \bigcup _{{k}\in ℕ}\left({E}\cap {A}\right)=\bigcup \mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)$
38 37 fveq2d ${⊢}{\phi }\to {M}\left(\bigcup _{{k}\in ℕ}\left({E}\cap {A}\right)\right)={M}\left(\bigcup \mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\right)$
39 nnct ${⊢}ℕ\preccurlyeq \mathrm{\omega }$
40 mptct ${⊢}ℕ\preccurlyeq \mathrm{\omega }\to \left({k}\in ℕ⟼{E}\cap {A}\right)\preccurlyeq \mathrm{\omega }$
41 rnct ${⊢}\left({k}\in ℕ⟼{E}\cap {A}\right)\preccurlyeq \mathrm{\omega }\to \mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\preccurlyeq \mathrm{\omega }$
42 39 40 41 mp2b ${⊢}\mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\preccurlyeq \mathrm{\omega }$
43 42 a1i ${⊢}{\phi }\to \mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\preccurlyeq \mathrm{\omega }$
44 eqid ${⊢}\left({k}\in ℕ⟼{E}\cap {A}\right)=\left({k}\in ℕ⟼{E}\cap {A}\right)$
45 44 rnmptss ${⊢}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{E}\cap {A}\in 𝒫{O}\to \mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\subseteq 𝒫{O}$
46 35 45 syl ${⊢}{\phi }\to \mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\subseteq 𝒫{O}$
47 mptexg ${⊢}ℕ\in \mathrm{V}\to \left({k}\in ℕ⟼{E}\cap {A}\right)\in \mathrm{V}$
48 rnexg ${⊢}\left({k}\in ℕ⟼{E}\cap {A}\right)\in \mathrm{V}\to \mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\in \mathrm{V}$
49 13 47 48 mp2b ${⊢}\mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\in \mathrm{V}$
50 breq1 ${⊢}{x}=\mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\to \left({x}\preccurlyeq \mathrm{\omega }↔\mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\preccurlyeq \mathrm{\omega }\right)$
51 sseq1 ${⊢}{x}=\mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\to \left({x}\subseteq 𝒫{O}↔\mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\subseteq 𝒫{O}\right)$
52 50 51 3anbi23d ${⊢}{x}=\mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\to \left(\left({\phi }\wedge {x}\preccurlyeq \mathrm{\omega }\wedge {x}\subseteq 𝒫{O}\right)↔\left({\phi }\wedge \mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\preccurlyeq \mathrm{\omega }\wedge \mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\subseteq 𝒫{O}\right)\right)$
53 unieq ${⊢}{x}=\mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\to \bigcup {x}=\bigcup \mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)$
54 53 fveq2d ${⊢}{x}=\mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\to {M}\left(\bigcup {x}\right)={M}\left(\bigcup \mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\right)$
55 esumeq1 ${⊢}{x}=\mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\to \underset{{y}\in {x}}{{\sum }^{*}}{M}\left({y}\right)=\underset{{y}\in \mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)}{{\sum }^{*}}{M}\left({y}\right)$
56 54 55 breq12d ${⊢}{x}=\mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\to \left({M}\left(\bigcup {x}\right)\le \underset{{y}\in {x}}{{\sum }^{*}}{M}\left({y}\right)↔{M}\left(\bigcup \mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\right)\le \underset{{y}\in \mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)}{{\sum }^{*}}{M}\left({y}\right)\right)$
57 52 56 imbi12d ${⊢}{x}=\mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\to \left(\left(\left({\phi }\wedge {x}\preccurlyeq \mathrm{\omega }\wedge {x}\subseteq 𝒫{O}\right)\to {M}\left(\bigcup {x}\right)\le \underset{{y}\in {x}}{{\sum }^{*}}{M}\left({y}\right)\right)↔\left(\left({\phi }\wedge \mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\preccurlyeq \mathrm{\omega }\wedge \mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\subseteq 𝒫{O}\right)\to {M}\left(\bigcup \mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\right)\le \underset{{y}\in \mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)}{{\sum }^{*}}{M}\left({y}\right)\right)\right)$
58 57 4 vtoclg ${⊢}\mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\in \mathrm{V}\to \left(\left({\phi }\wedge \mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\preccurlyeq \mathrm{\omega }\wedge \mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\subseteq 𝒫{O}\right)\to {M}\left(\bigcup \mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\right)\le \underset{{y}\in \mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)}{{\sum }^{*}}{M}\left({y}\right)\right)$
59 49 58 ax-mp ${⊢}\left({\phi }\wedge \mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\preccurlyeq \mathrm{\omega }\wedge \mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\subseteq 𝒫{O}\right)\to {M}\left(\bigcup \mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\right)\le \underset{{y}\in \mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)}{{\sum }^{*}}{M}\left({y}\right)$
60 43 46 59 mpd3an23 ${⊢}{\phi }\to {M}\left(\bigcup \mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)\right)\le \underset{{y}\in \mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)}{{\sum }^{*}}{M}\left({y}\right)$
61 38 60 eqbrtrd ${⊢}{\phi }\to {M}\left(\bigcup _{{k}\in ℕ}\left({E}\cap {A}\right)\right)\le \underset{{y}\in \mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)}{{\sum }^{*}}{M}\left({y}\right)$
62 fveq2 ${⊢}{y}={E}\cap {A}\to {M}\left({y}\right)={M}\left({E}\cap {A}\right)$
63 simpr ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge {E}\cap {A}=\varnothing \right)\to {E}\cap {A}=\varnothing$
64 63 fveq2d ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge {E}\cap {A}=\varnothing \right)\to {M}\left({E}\cap {A}\right)={M}\left(\varnothing \right)$
65 3 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge {E}\cap {A}=\varnothing \right)\to {M}\left(\varnothing \right)=0$
66 64 65 eqtrd ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge {E}\cap {A}=\varnothing \right)\to {M}\left({E}\cap {A}\right)=0$
67 disjin ${⊢}\underset{{k}\in ℕ}{Disj}{A}\to \underset{{k}\in ℕ}{Disj}\left({A}\cap {E}\right)$
68 6 67 syl ${⊢}{\phi }\to \underset{{k}\in ℕ}{Disj}\left({A}\cap {E}\right)$
69 incom ${⊢}{A}\cap {E}={E}\cap {A}$
70 69 rgenw ${⊢}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\cap {E}={E}\cap {A}$
71 disjeq2 ${⊢}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\cap {E}={E}\cap {A}\to \left(\underset{{k}\in ℕ}{Disj}\left({A}\cap {E}\right)↔\underset{{k}\in ℕ}{Disj}\left({E}\cap {A}\right)\right)$
72 70 71 ax-mp ${⊢}\underset{{k}\in ℕ}{Disj}\left({A}\cap {E}\right)↔\underset{{k}\in ℕ}{Disj}\left({E}\cap {A}\right)$
73 68 72 sylib ${⊢}{\phi }\to \underset{{k}\in ℕ}{Disj}\left({E}\cap {A}\right)$
74 62 14 29 16 66 73 esumrnmpt2 ${⊢}{\phi }\to \underset{{y}\in \mathrm{ran}\left({k}\in ℕ⟼{E}\cap {A}\right)}{{\sum }^{*}}{M}\left({y}\right)=\underset{{k}\in ℕ}{{\sum }^{*}}{M}\left({E}\cap {A}\right)$
75 61 74 breqtrd ${⊢}{\phi }\to {M}\left(\bigcup _{{k}\in ℕ}\left({E}\cap {A}\right)\right)\le \underset{{k}\in ℕ}{{\sum }^{*}}{M}\left({E}\cap {A}\right)$
76 difssd ${⊢}{\phi }\to {E}\setminus \bigcup _{{k}\in ℕ}{A}\subseteq {E}$
77 1 2 76 8 5 carsgmon ${⊢}{\phi }\to {M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\le {M}\left({E}\right)$
78 21 24 77 xrge0subcld ${⊢}{\phi }\to {M}\left({E}\right){+}_{𝑒}\left(-{M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\right)\in \left[0,\mathrm{+\infty }\right]$
79 2 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}:𝒫{O}⟶\left[0,\mathrm{+\infty }\right]$
80 8 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {E}\in 𝒫{O}$
81 80 elpwincl1 ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {E}\cap \bigcup _{{k}=1}^{{n}}{A}\in 𝒫{O}$
82 79 81 ffvelrnd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right)\in \left[0,\mathrm{+\infty }\right]$
83 12 82 sseldi ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right)\in {ℝ}^{*}$
84 xrge0neqmnf ${⊢}{M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right)\in \left[0,\mathrm{+\infty }\right]\to {M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right)\ne \mathrm{-\infty }$
85 82 84 syl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right)\ne \mathrm{-\infty }$
86 80 elpwdifcl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {E}\setminus \bigcup _{{k}=1}^{{n}}{A}\in 𝒫{O}$
87 79 86 ffvelrnd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\in \left[0,\mathrm{+\infty }\right]$
88 12 87 sseldi ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\in {ℝ}^{*}$
89 xrge0neqmnf ${⊢}{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\in \left[0,\mathrm{+\infty }\right]\to {M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\ne \mathrm{-\infty }$
90 87 89 syl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\ne \mathrm{-\infty }$
91 88 xnegcld ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to -{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\in {ℝ}^{*}$
92 xnegneg ${⊢}{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\in {ℝ}^{*}\to -\left(-{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\right)={M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)$
93 88 92 syl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to -\left(-{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\right)={M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)$
94 93 adantr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge -{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)=\mathrm{-\infty }\right)\to -\left(-{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\right)={M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)$
95 xnegeq ${⊢}-{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)=\mathrm{-\infty }\to -\left(-{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\right)=-\mathrm{-\infty }$
96 95 adantl ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge -{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)=\mathrm{-\infty }\right)\to -\left(-{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\right)=-\mathrm{-\infty }$
97 xnegmnf ${⊢}-\mathrm{-\infty }=\mathrm{+\infty }$
98 96 97 syl6eq ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge -{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)=\mathrm{-\infty }\right)\to -\left(-{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\right)=\mathrm{+\infty }$
99 94 98 eqtr3d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge -{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)=\mathrm{-\infty }\right)\to {M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)=\mathrm{+\infty }$
100 99 oveq2d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge -{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)=\mathrm{-\infty }\right)\to {M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right){+}_{𝑒}{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)={M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right){+}_{𝑒}\mathrm{+\infty }$
101 simpll ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to {\phi }$
102 fz1ssnn ${⊢}\left(1\dots {n}\right)\subseteq ℕ$
103 102 a1i ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left(1\dots {n}\right)\subseteq ℕ$
104 103 sselda ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to {k}\in ℕ$
105 101 104 7 syl2anc ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to {A}\in \mathrm{toCaraSiga}\left({M}\right)$
106 105 ralrimiva ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \forall {k}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{A}\in \mathrm{toCaraSiga}\left({M}\right)$
107 dfiun3g ${⊢}\forall {k}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{A}\in \mathrm{toCaraSiga}\left({M}\right)\to \bigcup _{{k}=1}^{{n}}{A}=\bigcup \mathrm{ran}\left({k}\in \left(1\dots {n}\right)⟼{A}\right)$
108 106 107 syl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \bigcup _{{k}=1}^{{n}}{A}=\bigcup \mathrm{ran}\left({k}\in \left(1\dots {n}\right)⟼{A}\right)$
109 1 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {O}\in {V}$
110 3 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\left(\varnothing \right)=0$
111 4 3adant1r ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\preccurlyeq \mathrm{\omega }\wedge {x}\subseteq 𝒫{O}\right)\to {M}\left(\bigcup {x}\right)\le \underset{{y}\in {x}}{{\sum }^{*}}{M}\left({y}\right)$
112 fzfi ${⊢}\left(1\dots {n}\right)\in \mathrm{Fin}$
113 mptfi ${⊢}\left(1\dots {n}\right)\in \mathrm{Fin}\to \left({k}\in \left(1\dots {n}\right)⟼{A}\right)\in \mathrm{Fin}$
114 rnfi ${⊢}\left({k}\in \left(1\dots {n}\right)⟼{A}\right)\in \mathrm{Fin}\to \mathrm{ran}\left({k}\in \left(1\dots {n}\right)⟼{A}\right)\in \mathrm{Fin}$
115 112 113 114 mp2b ${⊢}\mathrm{ran}\left({k}\in \left(1\dots {n}\right)⟼{A}\right)\in \mathrm{Fin}$
116 115 a1i ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \mathrm{ran}\left({k}\in \left(1\dots {n}\right)⟼{A}\right)\in \mathrm{Fin}$
117 eqid ${⊢}\left({k}\in \left(1\dots {n}\right)⟼{A}\right)=\left({k}\in \left(1\dots {n}\right)⟼{A}\right)$
118 117 rnmptss ${⊢}\forall {k}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{A}\in \mathrm{toCaraSiga}\left({M}\right)\to \mathrm{ran}\left({k}\in \left(1\dots {n}\right)⟼{A}\right)\subseteq \mathrm{toCaraSiga}\left({M}\right)$
119 106 118 syl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \mathrm{ran}\left({k}\in \left(1\dots {n}\right)⟼{A}\right)\subseteq \mathrm{toCaraSiga}\left({M}\right)$
120 109 79 110 111 116 119 fiunelcarsg ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \bigcup \mathrm{ran}\left({k}\in \left(1\dots {n}\right)⟼{A}\right)\in \mathrm{toCaraSiga}\left({M}\right)$
121 108 120 eqeltrd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \bigcup _{{k}=1}^{{n}}{A}\in \mathrm{toCaraSiga}\left({M}\right)$
122 109 79 elcarsg ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left(\bigcup _{{k}=1}^{{n}}{A}\in \mathrm{toCaraSiga}\left({M}\right)↔\left(\bigcup _{{k}=1}^{{n}}{A}\subseteq {O}\wedge \forall {e}\in 𝒫{O}\phantom{\rule{.4em}{0ex}}{M}\left({e}\cap \bigcup _{{k}=1}^{{n}}{A}\right){+}_{𝑒}{M}\left({e}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)={M}\left({e}\right)\right)\right)$
123 121 122 mpbid ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left(\bigcup _{{k}=1}^{{n}}{A}\subseteq {O}\wedge \forall {e}\in 𝒫{O}\phantom{\rule{.4em}{0ex}}{M}\left({e}\cap \bigcup _{{k}=1}^{{n}}{A}\right){+}_{𝑒}{M}\left({e}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)={M}\left({e}\right)\right)$
124 123 simprd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \forall {e}\in 𝒫{O}\phantom{\rule{.4em}{0ex}}{M}\left({e}\cap \bigcup _{{k}=1}^{{n}}{A}\right){+}_{𝑒}{M}\left({e}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)={M}\left({e}\right)$
125 ineq1 ${⊢}{e}={E}\to {e}\cap \bigcup _{{k}=1}^{{n}}{A}={E}\cap \bigcup _{{k}=1}^{{n}}{A}$
126 125 fveq2d ${⊢}{e}={E}\to {M}\left({e}\cap \bigcup _{{k}=1}^{{n}}{A}\right)={M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right)$
127 difeq1 ${⊢}{e}={E}\to {e}\setminus \bigcup _{{k}=1}^{{n}}{A}={E}\setminus \bigcup _{{k}=1}^{{n}}{A}$
128 127 fveq2d ${⊢}{e}={E}\to {M}\left({e}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)={M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)$
129 126 128 oveq12d ${⊢}{e}={E}\to {M}\left({e}\cap \bigcup _{{k}=1}^{{n}}{A}\right){+}_{𝑒}{M}\left({e}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)={M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right){+}_{𝑒}{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)$
130 fveq2 ${⊢}{e}={E}\to {M}\left({e}\right)={M}\left({E}\right)$
131 129 130 eqeq12d ${⊢}{e}={E}\to \left({M}\left({e}\cap \bigcup _{{k}=1}^{{n}}{A}\right){+}_{𝑒}{M}\left({e}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)={M}\left({e}\right)↔{M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right){+}_{𝑒}{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)={M}\left({E}\right)\right)$
132 131 rspcv ${⊢}{E}\in 𝒫{O}\to \left(\forall {e}\in 𝒫{O}\phantom{\rule{.4em}{0ex}}{M}\left({e}\cap \bigcup _{{k}=1}^{{n}}{A}\right){+}_{𝑒}{M}\left({e}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)={M}\left({e}\right)\to {M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right){+}_{𝑒}{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)={M}\left({E}\right)\right)$
133 80 124 132 sylc ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right){+}_{𝑒}{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)={M}\left({E}\right)$
134 133 adantr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge -{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)=\mathrm{-\infty }\right)\to {M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right){+}_{𝑒}{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)={M}\left({E}\right)$
135 xaddpnf1 ${⊢}\left({M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right)\in {ℝ}^{*}\wedge {M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right)\ne \mathrm{-\infty }\right)\to {M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right){+}_{𝑒}\mathrm{+\infty }=\mathrm{+\infty }$
136 83 85 135 syl2anc ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right){+}_{𝑒}\mathrm{+\infty }=\mathrm{+\infty }$
137 136 adantr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge -{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)=\mathrm{-\infty }\right)\to {M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right){+}_{𝑒}\mathrm{+\infty }=\mathrm{+\infty }$
138 100 134 137 3eqtr3d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge -{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)=\mathrm{-\infty }\right)\to {M}\left({E}\right)=\mathrm{+\infty }$
139 9 ad2antrr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge -{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)=\mathrm{-\infty }\right)\to {M}\left({E}\right)\ne \mathrm{+\infty }$
140 139 neneqd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge -{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)=\mathrm{-\infty }\right)\to ¬{M}\left({E}\right)=\mathrm{+\infty }$
141 138 140 pm2.65da ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to ¬-{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)=\mathrm{-\infty }$
142 141 neqned ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to -{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\ne \mathrm{-\infty }$
143 xaddass ${⊢}\left(\left({M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right)\in {ℝ}^{*}\wedge {M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right)\ne \mathrm{-\infty }\right)\wedge \left({M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\in {ℝ}^{*}\wedge {M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\ne \mathrm{-\infty }\right)\wedge \left(-{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\in {ℝ}^{*}\wedge -{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\ne \mathrm{-\infty }\right)\right)\to \left({M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right){+}_{𝑒}{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\right){+}_{𝑒}\left(-{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\right)={M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right){+}_{𝑒}\left({M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right){+}_{𝑒}\left(-{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\right)\right)$
144 83 85 88 90 91 142 143 syl222anc ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right){+}_{𝑒}{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\right){+}_{𝑒}\left(-{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\right)={M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right){+}_{𝑒}\left({M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right){+}_{𝑒}\left(-{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\right)\right)$
145 xnegid ${⊢}{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\in {ℝ}^{*}\to {M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right){+}_{𝑒}\left(-{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\right)=0$
146 88 145 syl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right){+}_{𝑒}\left(-{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\right)=0$
147 146 oveq2d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right){+}_{𝑒}\left({M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right){+}_{𝑒}\left(-{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\right)\right)={M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right){+}_{𝑒}0$
148 xaddid1 ${⊢}{M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right)\in {ℝ}^{*}\to {M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right){+}_{𝑒}0={M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right)$
149 83 148 syl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right){+}_{𝑒}0={M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right)$
150 144 147 149 3eqtrd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right){+}_{𝑒}{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\right){+}_{𝑒}\left(-{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\right)={M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right)$
151 133 oveq1d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right){+}_{𝑒}{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\right){+}_{𝑒}\left(-{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\right)={M}\left({E}\right){+}_{𝑒}\left(-{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\right)$
152 108 ineq2d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {E}\cap \bigcup _{{k}=1}^{{n}}{A}={E}\cap \bigcup \mathrm{ran}\left({k}\in \left(1\dots {n}\right)⟼{A}\right)$
153 152 fveq2d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right)={M}\left({E}\cap \bigcup \mathrm{ran}\left({k}\in \left(1\dots {n}\right)⟼{A}\right)\right)$
154 mptss ${⊢}\left(1\dots {n}\right)\subseteq ℕ\to \left({k}\in \left(1\dots {n}\right)⟼{A}\right)\subseteq \left({k}\in ℕ⟼{A}\right)$
155 rnss ${⊢}\left({k}\in \left(1\dots {n}\right)⟼{A}\right)\subseteq \left({k}\in ℕ⟼{A}\right)\to \mathrm{ran}\left({k}\in \left(1\dots {n}\right)⟼{A}\right)\subseteq \mathrm{ran}\left({k}\in ℕ⟼{A}\right)$
156 102 154 155 mp2b ${⊢}\mathrm{ran}\left({k}\in \left(1\dots {n}\right)⟼{A}\right)\subseteq \mathrm{ran}\left({k}\in ℕ⟼{A}\right)$
157 156 a1i ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \mathrm{ran}\left({k}\in \left(1\dots {n}\right)⟼{A}\right)\subseteq \mathrm{ran}\left({k}\in ℕ⟼{A}\right)$
158 disjrnmpt ${⊢}\underset{{k}\in ℕ}{Disj}{A}\to \underset{{y}\in \mathrm{ran}\left({k}\in ℕ⟼{A}\right)}{Disj}{y}$
159 6 158 syl ${⊢}{\phi }\to \underset{{y}\in \mathrm{ran}\left({k}\in ℕ⟼{A}\right)}{Disj}{y}$
160 159 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \underset{{y}\in \mathrm{ran}\left({k}\in ℕ⟼{A}\right)}{Disj}{y}$
161 disjss1 ${⊢}\mathrm{ran}\left({k}\in \left(1\dots {n}\right)⟼{A}\right)\subseteq \mathrm{ran}\left({k}\in ℕ⟼{A}\right)\to \left(\underset{{y}\in \mathrm{ran}\left({k}\in ℕ⟼{A}\right)}{Disj}{y}\to \underset{{y}\in \mathrm{ran}\left({k}\in \left(1\dots {n}\right)⟼{A}\right)}{Disj}{y}\right)$
162 157 160 161 sylc ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \underset{{y}\in \mathrm{ran}\left({k}\in \left(1\dots {n}\right)⟼{A}\right)}{Disj}{y}$
163 109 79 110 111 116 119 162 80 carsgclctunlem1 ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\left({E}\cap \bigcup \mathrm{ran}\left({k}\in \left(1\dots {n}\right)⟼{A}\right)\right)=\underset{{y}\in \mathrm{ran}\left({k}\in \left(1\dots {n}\right)⟼{A}\right)}{{\sum }^{*}}{M}\left({E}\cap {y}\right)$
164 ineq2 ${⊢}{y}={A}\to {E}\cap {y}={E}\cap {A}$
165 164 fveq2d ${⊢}{y}={A}\to {M}\left({E}\cap {y}\right)={M}\left({E}\cap {A}\right)$
166 112 elexi ${⊢}\left(1\dots {n}\right)\in \mathrm{V}$
167 166 a1i ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left(1\dots {n}\right)\in \mathrm{V}$
168 101 104 29 syl2anc ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to {M}\left({E}\cap {A}\right)\in \left[0,\mathrm{+\infty }\right]$
169 inss2 ${⊢}{E}\cap {A}\subseteq {A}$
170 sseq2 ${⊢}{A}=\varnothing \to \left({E}\cap {A}\subseteq {A}↔{E}\cap {A}\subseteq \varnothing \right)$
171 169 170 mpbii ${⊢}{A}=\varnothing \to {E}\cap {A}\subseteq \varnothing$
172 ss0 ${⊢}{E}\cap {A}\subseteq \varnothing \to {E}\cap {A}=\varnothing$
173 171 172 syl ${⊢}{A}=\varnothing \to {E}\cap {A}=\varnothing$
174 173 adantl ${⊢}\left(\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {k}\in \left(1\dots {n}\right)\right)\wedge {A}=\varnothing \right)\to {E}\cap {A}=\varnothing$
175 174 fveq2d ${⊢}\left(\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {k}\in \left(1\dots {n}\right)\right)\wedge {A}=\varnothing \right)\to {M}\left({E}\cap {A}\right)={M}\left(\varnothing \right)$
176 110 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {k}\in \left(1\dots {n}\right)\right)\wedge {A}=\varnothing \right)\to {M}\left(\varnothing \right)=0$
177 175 176 eqtrd ${⊢}\left(\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {k}\in \left(1\dots {n}\right)\right)\wedge {A}=\varnothing \right)\to {M}\left({E}\cap {A}\right)=0$
178 6 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \underset{{k}\in ℕ}{Disj}{A}$
179 disjss1 ${⊢}\left(1\dots {n}\right)\subseteq ℕ\to \left(\underset{{k}\in ℕ}{Disj}{A}\to \underset{{k}=1}{\overset{{n}}{Disj}}{A}\right)$
180 103 178 179 sylc ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \underset{{k}=1}{\overset{{n}}{Disj}}{A}$
181 165 167 168 105 177 180 esumrnmpt2 ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \underset{{y}\in \mathrm{ran}\left({k}\in \left(1\dots {n}\right)⟼{A}\right)}{{\sum }^{*}}{M}\left({E}\cap {y}\right)=\underset{{k}=1}{\overset{{n}}{{\sum }^{*}}}{M}\left({E}\cap {A}\right)$
182 153 163 181 3eqtrd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\left({E}\cap \bigcup _{{k}=1}^{{n}}{A}\right)=\underset{{k}=1}{\overset{{n}}{{\sum }^{*}}}{M}\left({E}\cap {A}\right)$
183 150 151 182 3eqtr3rd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \underset{{k}=1}{\overset{{n}}{{\sum }^{*}}}{M}\left({E}\cap {A}\right)={M}\left({E}\right){+}_{𝑒}\left(-{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\right)$
184 24 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\in \left[0,\mathrm{+\infty }\right]$
185 12 184 sseldi ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\in {ℝ}^{*}$
186 185 xnegcld ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to -{M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\in {ℝ}^{*}$
187 22 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\left({E}\right)\in {ℝ}^{*}$
188 iunss1 ${⊢}\left(1\dots {n}\right)\subseteq ℕ\to \bigcup _{{k}=1}^{{n}}{A}\subseteq \bigcup _{{k}\in ℕ}{A}$
189 102 188 mp1i ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \bigcup _{{k}=1}^{{n}}{A}\subseteq \bigcup _{{k}\in ℕ}{A}$
190 189 sscond ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {E}\setminus \bigcup _{{k}\in ℕ}{A}\subseteq {E}\setminus \bigcup _{{k}=1}^{{n}}{A}$
191 5 3adant1r ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\subseteq {y}\wedge {y}\in 𝒫{O}\right)\to {M}\left({x}\right)\le {M}\left({y}\right)$
192 109 79 190 86 191 carsgmon ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\le {M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)$
193 xleneg ${⊢}\left({M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\in {ℝ}^{*}\wedge {M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\in {ℝ}^{*}\right)\to \left({M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\le {M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)↔-{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\le -{M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\right)$
194 193 biimpa ${⊢}\left(\left({M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\in {ℝ}^{*}\wedge {M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\in {ℝ}^{*}\right)\wedge {M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\le {M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\right)\to -{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\le -{M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)$
195 185 88 192 194 syl21anc ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to -{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\le -{M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)$
196 xleadd2a ${⊢}\left(\left(-{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\in {ℝ}^{*}\wedge -{M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\in {ℝ}^{*}\wedge {M}\left({E}\right)\in {ℝ}^{*}\right)\wedge -{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\le -{M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\right)\to {M}\left({E}\right){+}_{𝑒}\left(-{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\right)\le {M}\left({E}\right){+}_{𝑒}\left(-{M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\right)$
197 91 186 187 195 196 syl31anc ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\left({E}\right){+}_{𝑒}\left(-{M}\left({E}\setminus \bigcup _{{k}=1}^{{n}}{A}\right)\right)\le {M}\left({E}\right){+}_{𝑒}\left(-{M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\right)$
198 183 197 eqbrtrd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \underset{{k}=1}{\overset{{n}}{{\sum }^{*}}}{M}\left({E}\cap {A}\right)\le {M}\left({E}\right){+}_{𝑒}\left(-{M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\right)$
199 78 29 198 esumgect ${⊢}{\phi }\to \underset{{k}\in ℕ}{{\sum }^{*}}{M}\left({E}\cap {A}\right)\le {M}\left({E}\right){+}_{𝑒}\left(-{M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\right)$
200 19 34 27 75 199 xrletrd ${⊢}{\phi }\to {M}\left(\bigcup _{{k}\in ℕ}\left({E}\cap {A}\right)\right)\le {M}\left({E}\right){+}_{𝑒}\left(-{M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\right)$
201 11 200 eqbrtrrid ${⊢}{\phi }\to {M}\left({E}\cap \bigcup _{{k}\in ℕ}{A}\right)\le {M}\left({E}\right){+}_{𝑒}\left(-{M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\right)$
202 xleadd1a ${⊢}\left(\left({M}\left({E}\cap \bigcup _{{k}\in ℕ}{A}\right)\in {ℝ}^{*}\wedge {M}\left({E}\right){+}_{𝑒}\left(-{M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\right)\in {ℝ}^{*}\wedge {M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\in {ℝ}^{*}\right)\wedge {M}\left({E}\cap \bigcup _{{k}\in ℕ}{A}\right)\le {M}\left({E}\right){+}_{𝑒}\left(-{M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\right)\right)\to {M}\left({E}\cap \bigcup _{{k}\in ℕ}{A}\right){+}_{𝑒}{M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\le \left({M}\left({E}\right){+}_{𝑒}\left(-{M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\right)\right){+}_{𝑒}{M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)$
203 20 27 25 201 202 syl31anc ${⊢}{\phi }\to {M}\left({E}\cap \bigcup _{{k}\in ℕ}{A}\right){+}_{𝑒}{M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\le \left({M}\left({E}\right){+}_{𝑒}\left(-{M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\right)\right){+}_{𝑒}{M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)$
204 xrge0npcan ${⊢}\left({M}\left({E}\right)\in \left[0,\mathrm{+\infty }\right]\wedge {M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\in \left[0,\mathrm{+\infty }\right]\wedge {M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\le {M}\left({E}\right)\right)\to \left({M}\left({E}\right){+}_{𝑒}\left(-{M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\right)\right){+}_{𝑒}{M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)={M}\left({E}\right)$
205 21 24 77 204 syl3anc ${⊢}{\phi }\to \left({M}\left({E}\right){+}_{𝑒}\left(-{M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\right)\right){+}_{𝑒}{M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)={M}\left({E}\right)$
206 203 205 breqtrd ${⊢}{\phi }\to {M}\left({E}\cap \bigcup _{{k}\in ℕ}{A}\right){+}_{𝑒}{M}\left({E}\setminus \bigcup _{{k}\in ℕ}{A}\right)\le {M}\left({E}\right)$