# Metamath Proof Explorer

## Theorem uniioombllem6

Description: Lemma for uniioombl . (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Hypotheses uniioombl.1 ${⊢}{\phi }\to {F}:ℕ⟶\le \cap {ℝ}^{2}$
uniioombl.2 ${⊢}{\phi }\to \underset{{x}\in ℕ}{Disj}\left(.\right)\left({F}\left({x}\right)\right)$
uniioombl.3 ${⊢}{S}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\right)\right)$
uniioombl.a ${⊢}{A}=\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)$
uniioombl.e ${⊢}{\phi }\to {vol}^{*}\left({E}\right)\in ℝ$
uniioombl.c ${⊢}{\phi }\to {C}\in {ℝ}^{+}$
uniioombl.g ${⊢}{\phi }\to {G}:ℕ⟶\le \cap {ℝ}^{2}$
uniioombl.s ${⊢}{\phi }\to {E}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)$
uniioombl.t ${⊢}{T}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right)$
uniioombl.v ${⊢}{\phi }\to sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\le {vol}^{*}\left({E}\right)+{C}$
Assertion uniioombllem6 ${⊢}{\phi }\to {vol}^{*}\left({E}\cap {A}\right)+{vol}^{*}\left({E}\setminus {A}\right)\le {vol}^{*}\left({E}\right)+4{C}$

### Proof

Step Hyp Ref Expression
1 uniioombl.1 ${⊢}{\phi }\to {F}:ℕ⟶\le \cap {ℝ}^{2}$
2 uniioombl.2 ${⊢}{\phi }\to \underset{{x}\in ℕ}{Disj}\left(.\right)\left({F}\left({x}\right)\right)$
3 uniioombl.3 ${⊢}{S}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\right)\right)$
4 uniioombl.a ${⊢}{A}=\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)$
5 uniioombl.e ${⊢}{\phi }\to {vol}^{*}\left({E}\right)\in ℝ$
6 uniioombl.c ${⊢}{\phi }\to {C}\in {ℝ}^{+}$
7 uniioombl.g ${⊢}{\phi }\to {G}:ℕ⟶\le \cap {ℝ}^{2}$
8 uniioombl.s ${⊢}{\phi }\to {E}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)$
9 uniioombl.t ${⊢}{T}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right)$
10 uniioombl.v ${⊢}{\phi }\to sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\le {vol}^{*}\left({E}\right)+{C}$
11 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
12 1zzd ${⊢}{\phi }\to 1\in ℤ$
13 eqidd ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to {T}\left({m}\right)={T}\left({m}\right)$
14 eqidd ${⊢}\left({\phi }\wedge {a}\in ℕ\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\left({a}\right)=\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\left({a}\right)$
15 eqid ${⊢}\left(\mathrm{abs}\circ -\right)\circ {G}=\left(\mathrm{abs}\circ -\right)\circ {G}$
16 15 ovolfsf ${⊢}{G}:ℕ⟶\le \cap {ℝ}^{2}\to \left(\left(\mathrm{abs}\circ -\right)\circ {G}\right):ℕ⟶\left[0,\mathrm{+\infty }\right)$
17 7 16 syl ${⊢}{\phi }\to \left(\left(\mathrm{abs}\circ -\right)\circ {G}\right):ℕ⟶\left[0,\mathrm{+\infty }\right)$
18 17 ffvelrnda ${⊢}\left({\phi }\wedge {a}\in ℕ\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\left({a}\right)\in \left[0,\mathrm{+\infty }\right)$
19 elrege0 ${⊢}\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\left({a}\right)\in \left[0,\mathrm{+\infty }\right)↔\left(\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\left({a}\right)\in ℝ\wedge 0\le \left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\left({a}\right)\right)$
20 18 19 sylib ${⊢}\left({\phi }\wedge {a}\in ℕ\right)\to \left(\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\left({a}\right)\in ℝ\wedge 0\le \left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\left({a}\right)\right)$
21 20 simpld ${⊢}\left({\phi }\wedge {a}\in ℕ\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\left({a}\right)\in ℝ$
22 20 simprd ${⊢}\left({\phi }\wedge {a}\in ℕ\right)\to 0\le \left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\left({a}\right)$
23 1 2 3 4 5 6 7 8 9 10 uniioombllem1 ${⊢}{\phi }\to sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\in ℝ$
24 15 9 ovolsf ${⊢}{G}:ℕ⟶\le \cap {ℝ}^{2}\to {T}:ℕ⟶\left[0,\mathrm{+\infty }\right)$
25 7 24 syl ${⊢}{\phi }\to {T}:ℕ⟶\left[0,\mathrm{+\infty }\right)$
26 25 frnd ${⊢}{\phi }\to \mathrm{ran}{T}\subseteq \left[0,\mathrm{+\infty }\right)$
27 icossxr ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq {ℝ}^{*}$
28 26 27 sstrdi ${⊢}{\phi }\to \mathrm{ran}{T}\subseteq {ℝ}^{*}$
29 supxrub ${⊢}\left(\mathrm{ran}{T}\subseteq {ℝ}^{*}\wedge {x}\in \mathrm{ran}{T}\right)\to {x}\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)$
30 28 29 sylan ${⊢}\left({\phi }\wedge {x}\in \mathrm{ran}{T}\right)\to {x}\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)$
31 30 ralrimiva ${⊢}{\phi }\to \forall {x}\in \mathrm{ran}{T}\phantom{\rule{.4em}{0ex}}{x}\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)$
32 25 ffnd ${⊢}{\phi }\to {T}Fnℕ$
33 breq1 ${⊢}{x}={T}\left({m}\right)\to \left({x}\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)↔{T}\left({m}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right)$
34 33 ralrn ${⊢}{T}Fnℕ\to \left(\forall {x}\in \mathrm{ran}{T}\phantom{\rule{.4em}{0ex}}{x}\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)↔\forall {m}\in ℕ\phantom{\rule{.4em}{0ex}}{T}\left({m}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right)$
35 32 34 syl ${⊢}{\phi }\to \left(\forall {x}\in \mathrm{ran}{T}\phantom{\rule{.4em}{0ex}}{x}\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)↔\forall {m}\in ℕ\phantom{\rule{.4em}{0ex}}{T}\left({m}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right)$
36 31 35 mpbid ${⊢}{\phi }\to \forall {m}\in ℕ\phantom{\rule{.4em}{0ex}}{T}\left({m}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)$
37 brralrspcev ${⊢}\left(sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\in ℝ\wedge \forall {m}\in ℕ\phantom{\rule{.4em}{0ex}}{T}\left({m}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {m}\in ℕ\phantom{\rule{.4em}{0ex}}{T}\left({m}\right)\le {x}$
38 23 36 37 syl2anc ${⊢}{\phi }\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {m}\in ℕ\phantom{\rule{.4em}{0ex}}{T}\left({m}\right)\le {x}$
39 11 9 12 14 21 22 38 isumsup2 ${⊢}{\phi }\to {T}⇝sup\left(\mathrm{ran}{T},ℝ,<\right)$
40 rge0ssre ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq ℝ$
41 26 40 sstrdi ${⊢}{\phi }\to \mathrm{ran}{T}\subseteq ℝ$
42 1nn ${⊢}1\in ℕ$
43 25 fdmd ${⊢}{\phi }\to \mathrm{dom}{T}=ℕ$
44 42 43 eleqtrrid ${⊢}{\phi }\to 1\in \mathrm{dom}{T}$
45 44 ne0d ${⊢}{\phi }\to \mathrm{dom}{T}\ne \varnothing$
46 dm0rn0 ${⊢}\mathrm{dom}{T}=\varnothing ↔\mathrm{ran}{T}=\varnothing$
47 46 necon3bii ${⊢}\mathrm{dom}{T}\ne \varnothing ↔\mathrm{ran}{T}\ne \varnothing$
48 45 47 sylib ${⊢}{\phi }\to \mathrm{ran}{T}\ne \varnothing$
49 brralrspcev ${⊢}\left(sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\in ℝ\wedge \forall {x}\in \mathrm{ran}{T}\phantom{\rule{.4em}{0ex}}{x}\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right)\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in \mathrm{ran}{T}\phantom{\rule{.4em}{0ex}}{x}\le {y}$
50 23 31 49 syl2anc ${⊢}{\phi }\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in \mathrm{ran}{T}\phantom{\rule{.4em}{0ex}}{x}\le {y}$
51 supxrre ${⊢}\left(\mathrm{ran}{T}\subseteq ℝ\wedge \mathrm{ran}{T}\ne \varnothing \wedge \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in \mathrm{ran}{T}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\to sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)=sup\left(\mathrm{ran}{T},ℝ,<\right)$
52 41 48 50 51 syl3anc ${⊢}{\phi }\to sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)=sup\left(\mathrm{ran}{T},ℝ,<\right)$
53 39 52 breqtrrd ${⊢}{\phi }\to {T}⇝sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)$
54 11 12 6 13 53 climi2 ${⊢}{\phi }\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}$
55 11 r19.2uz ${⊢}\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\to \exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}$
56 54 55 syl ${⊢}{\phi }\to \exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}$
57 1zzd ${⊢}\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\to 1\in ℤ$
58 6 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\to {C}\in {ℝ}^{+}$
59 simplrl ${⊢}\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\to {m}\in ℕ$
60 59 nnrpd ${⊢}\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\to {m}\in {ℝ}^{+}$
61 58 60 rpdivcld ${⊢}\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\to \frac{{C}}{{m}}\in {ℝ}^{+}$
62 fvex ${⊢}\left(.\right)\left({F}\left({z}\right)\right)\in \mathrm{V}$
63 62 inex1 ${⊢}\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\in \mathrm{V}$
64 63 rgenw ${⊢}\forall {z}\in ℕ\phantom{\rule{.4em}{0ex}}\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\in \mathrm{V}$
65 eqid ${⊢}\left({z}\in ℕ⟼\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)=\left({z}\in ℕ⟼\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)$
66 65 fnmpt ${⊢}\forall {z}\in ℕ\phantom{\rule{.4em}{0ex}}\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\in \mathrm{V}\to \left({z}\in ℕ⟼\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)Fnℕ$
67 64 66 mp1i ${⊢}\left(\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\wedge {n}\in ℕ\right)\to \left({z}\in ℕ⟼\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)Fnℕ$
68 elfznn ${⊢}{i}\in \left(1\dots {n}\right)\to {i}\in ℕ$
69 fvco2 ${⊢}\left(\left({z}\in ℕ⟼\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)Fnℕ\wedge {i}\in ℕ\right)\to \left({vol}^{*}\circ \left({z}\in ℕ⟼\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)\right)\left({i}\right)={vol}^{*}\left(\left({z}\in ℕ⟼\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)\left({i}\right)\right)$
70 67 68 69 syl2an ${⊢}\left(\left(\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\wedge {n}\in ℕ\right)\wedge {i}\in \left(1\dots {n}\right)\right)\to \left({vol}^{*}\circ \left({z}\in ℕ⟼\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)\right)\left({i}\right)={vol}^{*}\left(\left({z}\in ℕ⟼\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)\left({i}\right)\right)$
71 68 adantl ${⊢}\left(\left(\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\wedge {n}\in ℕ\right)\wedge {i}\in \left(1\dots {n}\right)\right)\to {i}\in ℕ$
72 2fveq3 ${⊢}{z}={i}\to \left(.\right)\left({F}\left({z}\right)\right)=\left(.\right)\left({F}\left({i}\right)\right)$
73 72 ineq1d ${⊢}{z}={i}\to \left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)=\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)$
74 fvex ${⊢}\left(.\right)\left({F}\left({i}\right)\right)\in \mathrm{V}$
75 74 inex1 ${⊢}\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\in \mathrm{V}$
76 73 65 75 fvmpt ${⊢}{i}\in ℕ\to \left({z}\in ℕ⟼\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)\left({i}\right)=\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)$
77 71 76 syl ${⊢}\left(\left(\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\wedge {n}\in ℕ\right)\wedge {i}\in \left(1\dots {n}\right)\right)\to \left({z}\in ℕ⟼\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)\left({i}\right)=\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)$
78 77 fveq2d ${⊢}\left(\left(\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\wedge {n}\in ℕ\right)\wedge {i}\in \left(1\dots {n}\right)\right)\to {vol}^{*}\left(\left({z}\in ℕ⟼\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)\left({i}\right)\right)={vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)$
79 70 78 eqtrd ${⊢}\left(\left(\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\wedge {n}\in ℕ\right)\wedge {i}\in \left(1\dots {n}\right)\right)\to \left({vol}^{*}\circ \left({z}\in ℕ⟼\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)\right)\left({i}\right)={vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)$
80 simpr ${⊢}\left(\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\wedge {n}\in ℕ\right)\to {n}\in ℕ$
81 80 11 eleqtrdi ${⊢}\left(\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\wedge {n}\in ℕ\right)\to {n}\in {ℤ}_{\ge 1}$
82 inss2 ${⊢}\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\subseteq \left(.\right)\left({G}\left({j}\right)\right)$
83 7 adantr ${⊢}\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\to {G}:ℕ⟶\le \cap {ℝ}^{2}$
84 elfznn ${⊢}{j}\in \left(1\dots {m}\right)\to {j}\in ℕ$
85 ffvelrn ${⊢}\left({G}:ℕ⟶\le \cap {ℝ}^{2}\wedge {j}\in ℕ\right)\to {G}\left({j}\right)\in \left(\le \cap {ℝ}^{2}\right)$
86 83 84 85 syl2an ${⊢}\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\to {G}\left({j}\right)\in \left(\le \cap {ℝ}^{2}\right)$
87 86 elin2d ${⊢}\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\to {G}\left({j}\right)\in {ℝ}^{2}$
88 1st2nd2 ${⊢}{G}\left({j}\right)\in {ℝ}^{2}\to {G}\left({j}\right)=⟨{1}^{st}\left({G}\left({j}\right)\right),{2}^{nd}\left({G}\left({j}\right)\right)⟩$
89 87 88 syl ${⊢}\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\to {G}\left({j}\right)=⟨{1}^{st}\left({G}\left({j}\right)\right),{2}^{nd}\left({G}\left({j}\right)\right)⟩$
90 89 fveq2d ${⊢}\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\to \left(.\right)\left({G}\left({j}\right)\right)=\left(.\right)\left(⟨{1}^{st}\left({G}\left({j}\right)\right),{2}^{nd}\left({G}\left({j}\right)\right)⟩\right)$
91 df-ov ${⊢}\left({1}^{st}\left({G}\left({j}\right)\right),{2}^{nd}\left({G}\left({j}\right)\right)\right)=\left(.\right)\left(⟨{1}^{st}\left({G}\left({j}\right)\right),{2}^{nd}\left({G}\left({j}\right)\right)⟩\right)$
92 90 91 syl6eqr ${⊢}\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\to \left(.\right)\left({G}\left({j}\right)\right)=\left({1}^{st}\left({G}\left({j}\right)\right),{2}^{nd}\left({G}\left({j}\right)\right)\right)$
93 ioossre ${⊢}\left({1}^{st}\left({G}\left({j}\right)\right),{2}^{nd}\left({G}\left({j}\right)\right)\right)\subseteq ℝ$
94 92 93 eqsstrdi ${⊢}\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\to \left(.\right)\left({G}\left({j}\right)\right)\subseteq ℝ$
95 94 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\wedge {n}\in ℕ\right)\wedge {i}\in \left(1\dots {n}\right)\right)\to \left(.\right)\left({G}\left({j}\right)\right)\subseteq ℝ$
96 92 fveq2d ${⊢}\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\to {vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\right)={vol}^{*}\left(\left({1}^{st}\left({G}\left({j}\right)\right),{2}^{nd}\left({G}\left({j}\right)\right)\right)\right)$
97 ovolfcl ${⊢}\left({G}:ℕ⟶\le \cap {ℝ}^{2}\wedge {j}\in ℕ\right)\to \left({1}^{st}\left({G}\left({j}\right)\right)\in ℝ\wedge {2}^{nd}\left({G}\left({j}\right)\right)\in ℝ\wedge {1}^{st}\left({G}\left({j}\right)\right)\le {2}^{nd}\left({G}\left({j}\right)\right)\right)$
98 83 84 97 syl2an ${⊢}\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\to \left({1}^{st}\left({G}\left({j}\right)\right)\in ℝ\wedge {2}^{nd}\left({G}\left({j}\right)\right)\in ℝ\wedge {1}^{st}\left({G}\left({j}\right)\right)\le {2}^{nd}\left({G}\left({j}\right)\right)\right)$
99 ovolioo ${⊢}\left({1}^{st}\left({G}\left({j}\right)\right)\in ℝ\wedge {2}^{nd}\left({G}\left({j}\right)\right)\in ℝ\wedge {1}^{st}\left({G}\left({j}\right)\right)\le {2}^{nd}\left({G}\left({j}\right)\right)\right)\to {vol}^{*}\left(\left({1}^{st}\left({G}\left({j}\right)\right),{2}^{nd}\left({G}\left({j}\right)\right)\right)\right)={2}^{nd}\left({G}\left({j}\right)\right)-{1}^{st}\left({G}\left({j}\right)\right)$
100 98 99 syl ${⊢}\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\to {vol}^{*}\left(\left({1}^{st}\left({G}\left({j}\right)\right),{2}^{nd}\left({G}\left({j}\right)\right)\right)\right)={2}^{nd}\left({G}\left({j}\right)\right)-{1}^{st}\left({G}\left({j}\right)\right)$
101 96 100 eqtrd ${⊢}\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\to {vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\right)={2}^{nd}\left({G}\left({j}\right)\right)-{1}^{st}\left({G}\left({j}\right)\right)$
102 98 simp2d ${⊢}\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\to {2}^{nd}\left({G}\left({j}\right)\right)\in ℝ$
103 98 simp1d ${⊢}\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\to {1}^{st}\left({G}\left({j}\right)\right)\in ℝ$
104 102 103 resubcld ${⊢}\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\to {2}^{nd}\left({G}\left({j}\right)\right)-{1}^{st}\left({G}\left({j}\right)\right)\in ℝ$
105 101 104 eqeltrd ${⊢}\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\to {vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\right)\in ℝ$
106 105 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\wedge {n}\in ℕ\right)\wedge {i}\in \left(1\dots {n}\right)\right)\to {vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\right)\in ℝ$
107 ovolsscl ${⊢}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\subseteq \left(.\right)\left({G}\left({j}\right)\right)\wedge \left(.\right)\left({G}\left({j}\right)\right)\subseteq ℝ\wedge {vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\right)\in ℝ\right)\to {vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)\in ℝ$
108 82 95 106 107 mp3an2i ${⊢}\left(\left(\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\wedge {n}\in ℕ\right)\wedge {i}\in \left(1\dots {n}\right)\right)\to {vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)\in ℝ$
109 108 recnd ${⊢}\left(\left(\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\wedge {n}\in ℕ\right)\wedge {i}\in \left(1\dots {n}\right)\right)\to {vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)\in ℂ$
110 79 81 109 fsumser ${⊢}\left(\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\wedge {n}\in ℕ\right)\to \sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)=seq1\left(+,\left({vol}^{*}\circ \left({z}\in ℕ⟼\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)\right)\right)\left({n}\right)$
111 110 eqcomd ${⊢}\left(\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\wedge {n}\in ℕ\right)\to seq1\left(+,\left({vol}^{*}\circ \left({z}\in ℕ⟼\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)\right)\right)\left({n}\right)=\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)$
112 2fveq3 ${⊢}{z}={k}\to \left(.\right)\left({F}\left({z}\right)\right)=\left(.\right)\left({F}\left({k}\right)\right)$
113 112 ineq1d ${⊢}{z}={k}\to \left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)=\left(.\right)\left({F}\left({k}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)$
114 113 cbvmptv ${⊢}\left({z}\in ℕ⟼\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)=\left({k}\in ℕ⟼\left(.\right)\left({F}\left({k}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)$
115 eqeq1 ${⊢}{z}={x}\to \left({z}=\varnothing ↔{x}=\varnothing \right)$
116 infeq1 ${⊢}{z}={x}\to sup\left({z},{ℝ}^{*},<\right)=sup\left({x},{ℝ}^{*},<\right)$
117 supeq1 ${⊢}{z}={x}\to sup\left({z},{ℝ}^{*},<\right)=sup\left({x},{ℝ}^{*},<\right)$
118 116 117 opeq12d ${⊢}{z}={x}\to ⟨sup\left({z},{ℝ}^{*},<\right),sup\left({z},{ℝ}^{*},<\right)⟩=⟨sup\left({x},{ℝ}^{*},<\right),sup\left({x},{ℝ}^{*},<\right)⟩$
119 115 118 ifbieq2d ${⊢}{z}={x}\to if\left({z}=\varnothing ,⟨0,0⟩,⟨sup\left({z},{ℝ}^{*},<\right),sup\left({z},{ℝ}^{*},<\right)⟩\right)=if\left({x}=\varnothing ,⟨0,0⟩,⟨sup\left({x},{ℝ}^{*},<\right),sup\left({x},{ℝ}^{*},<\right)⟩\right)$
120 119 cbvmptv ${⊢}\left({z}\in \mathrm{ran}\left(.\right)⟼if\left({z}=\varnothing ,⟨0,0⟩,⟨sup\left({z},{ℝ}^{*},<\right),sup\left({z},{ℝ}^{*},<\right)⟩\right)\right)=\left({x}\in \mathrm{ran}\left(.\right)⟼if\left({x}=\varnothing ,⟨0,0⟩,⟨sup\left({x},{ℝ}^{*},<\right),sup\left({x},{ℝ}^{*},<\right)⟩\right)\right)$
121 1 2 3 4 5 6 7 8 9 10 114 120 uniioombllem2 ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to seq1\left(+,\left({vol}^{*}\circ \left({z}\in ℕ⟼\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)\right)\right)⇝{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)$
122 84 121 sylan2 ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {m}\right)\right)\to seq1\left(+,\left({vol}^{*}\circ \left({z}\in ℕ⟼\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)\right)\right)⇝{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)$
123 122 adantlr ${⊢}\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\to seq1\left(+,\left({vol}^{*}\circ \left({z}\in ℕ⟼\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)\right)\right)⇝{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)$
124 11 57 61 111 123 climi2 ${⊢}\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\to \exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℤ}_{\ge {a}}\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}$
125 1z ${⊢}1\in ℤ$
126 11 rexuz3 ${⊢}1\in ℤ\to \left(\exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℤ}_{\ge {a}}\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}↔\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℤ}_{\ge {a}}\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}\right)$
127 125 126 ax-mp ${⊢}\exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℤ}_{\ge {a}}\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}↔\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℤ}_{\ge {a}}\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}$
128 124 127 sylib ${⊢}\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge {j}\in \left(1\dots {m}\right)\right)\to \exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℤ}_{\ge {a}}\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}$
129 128 ralrimiva ${⊢}\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\to \forall {j}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℤ}_{\ge {a}}\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}$
130 fzfi ${⊢}\left(1\dots {m}\right)\in \mathrm{Fin}$
131 rexfiuz ${⊢}\left(1\dots {m}\right)\in \mathrm{Fin}\to \left(\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℤ}_{\ge {a}}\phantom{\rule{.4em}{0ex}}\forall {j}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}↔\forall {j}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℤ}_{\ge {a}}\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}\right)$
132 130 131 ax-mp ${⊢}\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℤ}_{\ge {a}}\phantom{\rule{.4em}{0ex}}\forall {j}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}↔\forall {j}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℤ}_{\ge {a}}\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}$
133 129 132 sylibr ${⊢}\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\to \exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℤ}_{\ge {a}}\phantom{\rule{.4em}{0ex}}\forall {j}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}$
134 11 rexuz3 ${⊢}1\in ℤ\to \left(\exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℤ}_{\ge {a}}\phantom{\rule{.4em}{0ex}}\forall {j}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}↔\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℤ}_{\ge {a}}\phantom{\rule{.4em}{0ex}}\forall {j}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}\right)$
135 125 134 ax-mp ${⊢}\exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℤ}_{\ge {a}}\phantom{\rule{.4em}{0ex}}\forall {j}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}↔\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℤ}_{\ge {a}}\phantom{\rule{.4em}{0ex}}\forall {j}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}$
136 133 135 sylibr ${⊢}\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\to \exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℤ}_{\ge {a}}\phantom{\rule{.4em}{0ex}}\forall {j}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}$
137 11 r19.2uz ${⊢}\exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℤ}_{\ge {a}}\phantom{\rule{.4em}{0ex}}\forall {j}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {j}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}$
138 136 137 syl ${⊢}\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {j}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}$
139 1 adantr ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\wedge \left({n}\in ℕ\wedge \forall {j}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}\right)\right)\right)\to {F}:ℕ⟶\le \cap {ℝ}^{2}$
140 2 adantr ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\wedge \left({n}\in ℕ\wedge \forall {j}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}\right)\right)\right)\to \underset{{x}\in ℕ}{Disj}\left(.\right)\left({F}\left({x}\right)\right)$
141 5 adantr ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\wedge \left({n}\in ℕ\wedge \forall {j}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}\right)\right)\right)\to {vol}^{*}\left({E}\right)\in ℝ$
142 6 adantr ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\wedge \left({n}\in ℕ\wedge \forall {j}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}\right)\right)\right)\to {C}\in {ℝ}^{+}$
143 7 adantr ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\wedge \left({n}\in ℕ\wedge \forall {j}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}\right)\right)\right)\to {G}:ℕ⟶\le \cap {ℝ}^{2}$
144 8 adantr ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\wedge \left({n}\in ℕ\wedge \forall {j}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}\right)\right)\right)\to {E}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)$
145 10 adantr ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\wedge \left({n}\in ℕ\wedge \forall {j}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}\right)\right)\right)\to sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\le {vol}^{*}\left({E}\right)+{C}$
146 simprll ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\wedge \left({n}\in ℕ\wedge \forall {j}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}\right)\right)\right)\to {m}\in ℕ$
147 simprlr ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\wedge \left({n}\in ℕ\wedge \forall {j}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}\right)\right)\right)\to \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}$
148 eqid ${⊢}\bigcup \left(\left(.\right)\circ {G}\right)\left[\left(1\dots {m}\right)\right]=\bigcup \left(\left(.\right)\circ {G}\right)\left[\left(1\dots {m}\right)\right]$
149 simprrl ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\wedge \left({n}\in ℕ\wedge \forall {j}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}\right)\right)\right)\to {n}\in ℕ$
150 simprrr ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\wedge \left({n}\in ℕ\wedge \forall {j}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}\right)\right)\right)\to \forall {j}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}$
151 2fveq3 ${⊢}{i}={z}\to \left(.\right)\left({F}\left({i}\right)\right)=\left(.\right)\left({F}\left({z}\right)\right)$
152 151 ineq1d ${⊢}{i}={z}\to \left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)=\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)$
153 152 fveq2d ${⊢}{i}={z}\to {vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)={vol}^{*}\left(\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)$
154 153 cbvsumv ${⊢}\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)=\sum _{{z}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)$
155 2fveq3 ${⊢}{j}={k}\to \left(.\right)\left({G}\left({j}\right)\right)=\left(.\right)\left({G}\left({k}\right)\right)$
156 155 ineq2d ${⊢}{j}={k}\to \left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)=\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({k}\right)\right)$
157 156 fveq2d ${⊢}{j}={k}\to {vol}^{*}\left(\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)={vol}^{*}\left(\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({k}\right)\right)\right)$
158 157 sumeq2sdv ${⊢}{j}={k}\to \sum _{{z}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)=\sum _{{z}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({k}\right)\right)\right)$
159 154 158 syl5eq ${⊢}{j}={k}\to \sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)=\sum _{{z}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({k}\right)\right)\right)$
160 155 ineq1d ${⊢}{j}={k}\to \left(.\right)\left({G}\left({j}\right)\right)\cap {A}=\left(.\right)\left({G}\left({k}\right)\right)\cap {A}$
161 160 fveq2d ${⊢}{j}={k}\to {vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)={vol}^{*}\left(\left(.\right)\left({G}\left({k}\right)\right)\cap {A}\right)$
162 159 161 oveq12d ${⊢}{j}={k}\to \sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)=\sum _{{z}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({k}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({k}\right)\right)\cap {A}\right)$
163 162 fveq2d ${⊢}{j}={k}\to \left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|=\left|\sum _{{z}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({k}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({k}\right)\right)\cap {A}\right)\right|$
164 163 breq1d ${⊢}{j}={k}\to \left(\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}↔\left|\sum _{{z}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({k}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({k}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}\right)$
165 164 cbvralvw ${⊢}\forall {j}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}↔\forall {k}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{z}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({k}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({k}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}$
166 150 165 sylib ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\wedge \left({n}\in ℕ\wedge \forall {j}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}\right)\right)\right)\to \forall {k}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{z}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({z}\right)\right)\cap \left(.\right)\left({G}\left({k}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({k}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}$
167 eqid ${⊢}\bigcup \left(\left(.\right)\circ {F}\right)\left[\left(1\dots {n}\right)\right]=\bigcup \left(\left(.\right)\circ {F}\right)\left[\left(1\dots {n}\right)\right]$
168 139 140 3 4 141 142 143 144 9 145 146 147 148 149 166 167 uniioombllem5 ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\wedge \left({n}\in ℕ\wedge \forall {j}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}\right)\right)\right)\to {vol}^{*}\left({E}\cap {A}\right)+{vol}^{*}\left({E}\setminus {A}\right)\le {vol}^{*}\left({E}\right)+4{C}$
169 168 anassrs ${⊢}\left(\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\wedge \left({n}\in ℕ\wedge \forall {j}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{i}=1}^{{n}}{vol}^{*}\left(\left(.\right)\left({F}\left({i}\right)\right)\cap \left(.\right)\left({G}\left({j}\right)\right)\right)-{vol}^{*}\left(\left(.\right)\left({G}\left({j}\right)\right)\cap {A}\right)\right|<\frac{{C}}{{m}}\right)\right)\to {vol}^{*}\left({E}\cap {A}\right)+{vol}^{*}\left({E}\setminus {A}\right)\le {vol}^{*}\left({E}\right)+4{C}$
170 138 169 rexlimddv ${⊢}\left({\phi }\wedge \left({m}\in ℕ\wedge \left|{T}\left({m}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}\right)\right)\to {vol}^{*}\left({E}\cap {A}\right)+{vol}^{*}\left({E}\setminus {A}\right)\le {vol}^{*}\left({E}\right)+4{C}$
171 56 170 rexlimddv ${⊢}{\phi }\to {vol}^{*}\left({E}\cap {A}\right)+{vol}^{*}\left({E}\setminus {A}\right)\le {vol}^{*}\left({E}\right)+4{C}$