# Metamath Proof Explorer

## Theorem carageniuncllem2

Description: The Caratheodory's construction is closed under countable union. Step (d) in the proof of Theorem 113C of Fremlin1 p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses carageniuncllem2.o ${⊢}{\phi }\to {O}\in \mathrm{OutMeas}$
carageniuncllem2.s ${⊢}{S}=\mathrm{CaraGen}\left({O}\right)$
carageniuncllem2.x ${⊢}{X}=\bigcup \mathrm{dom}{O}$
carageniuncllem2.a ${⊢}{\phi }\to {A}\subseteq {X}$
carageniuncllem2.re ${⊢}{\phi }\to {O}\left({A}\right)\in ℝ$
carageniuncllem2.m ${⊢}{\phi }\to {M}\in ℤ$
carageniuncllem2.z ${⊢}{Z}={ℤ}_{\ge {M}}$
carageniuncllem2.e ${⊢}{\phi }\to {E}:{Z}⟶{S}$
carageniuncllem2.y ${⊢}{\phi }\to {Y}\in {ℝ}^{+}$
carageniuncllem2.g ${⊢}{G}=\left({n}\in {Z}⟼\bigcup _{{i}={M}}^{{n}}{E}\left({i}\right)\right)$
carageniuncllem2.f ${⊢}{F}=\left({n}\in {Z}⟼{E}\left({n}\right)\setminus \bigcup _{{i}\in \left({M}..^{n}\right)}{E}\left({i}\right)\right)$
Assertion carageniuncllem2 ${⊢}{\phi }\to {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right){+}_{𝑒}{O}\left({A}\setminus \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)\le {O}\left({A}\right)+{Y}$

### Proof

Step Hyp Ref Expression
1 carageniuncllem2.o ${⊢}{\phi }\to {O}\in \mathrm{OutMeas}$
2 carageniuncllem2.s ${⊢}{S}=\mathrm{CaraGen}\left({O}\right)$
3 carageniuncllem2.x ${⊢}{X}=\bigcup \mathrm{dom}{O}$
4 carageniuncllem2.a ${⊢}{\phi }\to {A}\subseteq {X}$
5 carageniuncllem2.re ${⊢}{\phi }\to {O}\left({A}\right)\in ℝ$
6 carageniuncllem2.m ${⊢}{\phi }\to {M}\in ℤ$
7 carageniuncllem2.z ${⊢}{Z}={ℤ}_{\ge {M}}$
8 carageniuncllem2.e ${⊢}{\phi }\to {E}:{Z}⟶{S}$
9 carageniuncllem2.y ${⊢}{\phi }\to {Y}\in {ℝ}^{+}$
10 carageniuncllem2.g ${⊢}{G}=\left({n}\in {Z}⟼\bigcup _{{i}={M}}^{{n}}{E}\left({i}\right)\right)$
11 carageniuncllem2.f ${⊢}{F}=\left({n}\in {Z}⟼{E}\left({n}\right)\setminus \bigcup _{{i}\in \left({M}..^{n}\right)}{E}\left({i}\right)\right)$
12 inss1 ${⊢}{A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\subseteq {A}$
13 12 a1i ${⊢}{\phi }\to {A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\subseteq {A}$
14 1 3 4 5 13 omessre ${⊢}{\phi }\to {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)\in ℝ$
15 difssd ${⊢}{\phi }\to {A}\setminus \bigcup _{{n}\in {Z}}{E}\left({n}\right)\subseteq {A}$
16 1 3 4 5 15 omessre ${⊢}{\phi }\to {O}\left({A}\setminus \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)\in ℝ$
17 rexadd ${⊢}\left({O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)\in ℝ\wedge {O}\left({A}\setminus \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)\in ℝ\right)\to {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right){+}_{𝑒}{O}\left({A}\setminus \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)={O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)+{O}\left({A}\setminus \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)$
18 14 16 17 syl2anc ${⊢}{\phi }\to {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right){+}_{𝑒}{O}\left({A}\setminus \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)={O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)+{O}\left({A}\setminus \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)$
19 ssinss1 ${⊢}{A}\subseteq {X}\to {A}\cap {F}\left({n}\right)\subseteq {X}$
20 4 19 syl ${⊢}{\phi }\to {A}\cap {F}\left({n}\right)\subseteq {X}$
21 1 3 unidmex ${⊢}{\phi }\to {X}\in \mathrm{V}$
22 ssexg ${⊢}\left({A}\subseteq {X}\wedge {X}\in \mathrm{V}\right)\to {A}\in \mathrm{V}$
23 4 21 22 syl2anc ${⊢}{\phi }\to {A}\in \mathrm{V}$
24 inex1g ${⊢}{A}\in \mathrm{V}\to {A}\cap {F}\left({n}\right)\in \mathrm{V}$
25 23 24 syl ${⊢}{\phi }\to {A}\cap {F}\left({n}\right)\in \mathrm{V}$
26 elpwg ${⊢}{A}\cap {F}\left({n}\right)\in \mathrm{V}\to \left({A}\cap {F}\left({n}\right)\in 𝒫{X}↔{A}\cap {F}\left({n}\right)\subseteq {X}\right)$
27 25 26 syl ${⊢}{\phi }\to \left({A}\cap {F}\left({n}\right)\in 𝒫{X}↔{A}\cap {F}\left({n}\right)\subseteq {X}\right)$
28 20 27 mpbird ${⊢}{\phi }\to {A}\cap {F}\left({n}\right)\in 𝒫{X}$
29 28 adantr ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {A}\cap {F}\left({n}\right)\in 𝒫{X}$
30 eqid ${⊢}\left({n}\in {Z}⟼{A}\cap {F}\left({n}\right)\right)=\left({n}\in {Z}⟼{A}\cap {F}\left({n}\right)\right)$
31 29 30 fmptd ${⊢}{\phi }\to \left({n}\in {Z}⟼{A}\cap {F}\left({n}\right)\right):{Z}⟶𝒫{X}$
32 fveq2 ${⊢}{k}={n}\to {F}\left({k}\right)={F}\left({n}\right)$
33 32 ineq2d ${⊢}{k}={n}\to {A}\cap {F}\left({k}\right)={A}\cap {F}\left({n}\right)$
34 33 cbvmptv ${⊢}\left({k}\in {Z}⟼{A}\cap {F}\left({k}\right)\right)=\left({n}\in {Z}⟼{A}\cap {F}\left({n}\right)\right)$
35 34 feq1i ${⊢}\left({k}\in {Z}⟼{A}\cap {F}\left({k}\right)\right):{Z}⟶𝒫{X}↔\left({n}\in {Z}⟼{A}\cap {F}\left({n}\right)\right):{Z}⟶𝒫{X}$
36 35 a1i ${⊢}{\phi }\to \left(\left({k}\in {Z}⟼{A}\cap {F}\left({k}\right)\right):{Z}⟶𝒫{X}↔\left({n}\in {Z}⟼{A}\cap {F}\left({n}\right)\right):{Z}⟶𝒫{X}\right)$
37 31 36 mpbird ${⊢}{\phi }\to \left({k}\in {Z}⟼{A}\cap {F}\left({k}\right)\right):{Z}⟶𝒫{X}$
38 simpr ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {n}\in {Z}$
39 25 adantr ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {A}\cap {F}\left({n}\right)\in \mathrm{V}$
40 34 fvmpt2 ${⊢}\left({n}\in {Z}\wedge {A}\cap {F}\left({n}\right)\in \mathrm{V}\right)\to \left({k}\in {Z}⟼{A}\cap {F}\left({k}\right)\right)\left({n}\right)={A}\cap {F}\left({n}\right)$
41 38 39 40 syl2anc ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to \left({k}\in {Z}⟼{A}\cap {F}\left({k}\right)\right)\left({n}\right)={A}\cap {F}\left({n}\right)$
42 41 iuneq2dv ${⊢}{\phi }\to \bigcup _{{n}\in {Z}}\left({k}\in {Z}⟼{A}\cap {F}\left({k}\right)\right)\left({n}\right)=\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)$
43 42 fveq2d ${⊢}{\phi }\to {O}\left(\bigcup _{{n}\in {Z}}\left({k}\in {Z}⟼{A}\cap {F}\left({k}\right)\right)\left({n}\right)\right)={O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)$
44 nfv ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}{\phi }$
45 44 7 8 11 iundjiun ${⊢}{\phi }\to \left(\left(\forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\bigcup _{{n}={M}}^{{m}}{F}\left({n}\right)=\bigcup _{{n}={M}}^{{m}}{E}\left({n}\right)\wedge \bigcup _{{n}\in {Z}}{F}\left({n}\right)=\bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)\wedge \underset{{n}\in {Z}}{Disj}{F}\left({n}\right)\right)$
46 45 simplrd ${⊢}{\phi }\to \bigcup _{{n}\in {Z}}{F}\left({n}\right)=\bigcup _{{n}\in {Z}}{E}\left({n}\right)$
47 46 eqcomd ${⊢}{\phi }\to \bigcup _{{n}\in {Z}}{E}\left({n}\right)=\bigcup _{{n}\in {Z}}{F}\left({n}\right)$
48 47 ineq2d ${⊢}{\phi }\to {A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)={A}\cap \bigcup _{{n}\in {Z}}{F}\left({n}\right)$
49 iunin2 ${⊢}\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)={A}\cap \bigcup _{{n}\in {Z}}{F}\left({n}\right)$
50 49 eqcomi ${⊢}{A}\cap \bigcup _{{n}\in {Z}}{F}\left({n}\right)=\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)$
51 50 a1i ${⊢}{\phi }\to {A}\cap \bigcup _{{n}\in {Z}}{F}\left({n}\right)=\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)$
52 48 51 eqtrd ${⊢}{\phi }\to {A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)=\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)$
53 52 fveq2d ${⊢}{\phi }\to {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)={O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)$
54 53 14 eqeltrrd ${⊢}{\phi }\to {O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)\in ℝ$
55 43 54 eqeltrd ${⊢}{\phi }\to {O}\left(\bigcup _{{n}\in {Z}}\left({k}\in {Z}⟼{A}\cap {F}\left({k}\right)\right)\left({n}\right)\right)\in ℝ$
56 1 3 7 37 55 9 omeiunltfirp ${⊢}{\phi }\to \exists {z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{O}\left(\bigcup _{{n}\in {Z}}\left({k}\in {Z}⟼{A}\cap {F}\left({k}\right)\right)\left({n}\right)\right)<\sum _{{n}\in {z}}{O}\left(\left({k}\in {Z}⟼{A}\cap {F}\left({k}\right)\right)\left({n}\right)\right)+{Y}$
57 43 adantr ${⊢}\left({\phi }\wedge {z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\right)\to {O}\left(\bigcup _{{n}\in {Z}}\left({k}\in {Z}⟼{A}\cap {F}\left({k}\right)\right)\left({n}\right)\right)={O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)$
58 elpwinss ${⊢}{z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\to {z}\subseteq {Z}$
59 58 adantr ${⊢}\left({z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\wedge {n}\in {z}\right)\to {z}\subseteq {Z}$
60 simpr ${⊢}\left({z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\wedge {n}\in {z}\right)\to {n}\in {z}$
61 59 60 sseldd ${⊢}\left({z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\wedge {n}\in {z}\right)\to {n}\in {Z}$
62 61 adantll ${⊢}\left(\left({\phi }\wedge {z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\right)\wedge {n}\in {z}\right)\to {n}\in {Z}$
63 25 ad2antrr ${⊢}\left(\left({\phi }\wedge {z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\right)\wedge {n}\in {z}\right)\to {A}\cap {F}\left({n}\right)\in \mathrm{V}$
64 62 63 40 syl2anc ${⊢}\left(\left({\phi }\wedge {z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\right)\wedge {n}\in {z}\right)\to \left({k}\in {Z}⟼{A}\cap {F}\left({k}\right)\right)\left({n}\right)={A}\cap {F}\left({n}\right)$
65 64 fveq2d ${⊢}\left(\left({\phi }\wedge {z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\right)\wedge {n}\in {z}\right)\to {O}\left(\left({k}\in {Z}⟼{A}\cap {F}\left({k}\right)\right)\left({n}\right)\right)={O}\left({A}\cap {F}\left({n}\right)\right)$
66 65 sumeq2dv ${⊢}\left({\phi }\wedge {z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\right)\to \sum _{{n}\in {z}}{O}\left(\left({k}\in {Z}⟼{A}\cap {F}\left({k}\right)\right)\left({n}\right)\right)=\sum _{{n}\in {z}}{O}\left({A}\cap {F}\left({n}\right)\right)$
67 66 oveq1d ${⊢}\left({\phi }\wedge {z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\right)\to \sum _{{n}\in {z}}{O}\left(\left({k}\in {Z}⟼{A}\cap {F}\left({k}\right)\right)\left({n}\right)\right)+{Y}=\sum _{{n}\in {z}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}$
68 57 67 breq12d ${⊢}\left({\phi }\wedge {z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\right)\to \left({O}\left(\bigcup _{{n}\in {Z}}\left({k}\in {Z}⟼{A}\cap {F}\left({k}\right)\right)\left({n}\right)\right)<\sum _{{n}\in {z}}{O}\left(\left({k}\in {Z}⟼{A}\cap {F}\left({k}\right)\right)\left({n}\right)\right)+{Y}↔{O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)<\sum _{{n}\in {z}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\right)$
69 68 biimpd ${⊢}\left({\phi }\wedge {z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\right)\to \left({O}\left(\bigcup _{{n}\in {Z}}\left({k}\in {Z}⟼{A}\cap {F}\left({k}\right)\right)\left({n}\right)\right)<\sum _{{n}\in {z}}{O}\left(\left({k}\in {Z}⟼{A}\cap {F}\left({k}\right)\right)\left({n}\right)\right)+{Y}\to {O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)<\sum _{{n}\in {z}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\right)$
70 69 reximdva ${⊢}{\phi }\to \left(\exists {z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{O}\left(\bigcup _{{n}\in {Z}}\left({k}\in {Z}⟼{A}\cap {F}\left({k}\right)\right)\left({n}\right)\right)<\sum _{{n}\in {z}}{O}\left(\left({k}\in {Z}⟼{A}\cap {F}\left({k}\right)\right)\left({n}\right)\right)+{Y}\to \exists {z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)<\sum _{{n}\in {z}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\right)$
71 56 70 mpd ${⊢}{\phi }\to \exists {z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)<\sum _{{n}\in {z}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}$
72 6 adantr ${⊢}\left({\phi }\wedge {z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\right)\to {M}\in ℤ$
73 58 adantl ${⊢}\left({\phi }\wedge {z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\right)\to {z}\subseteq {Z}$
74 elinel2 ${⊢}{z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\to {z}\in \mathrm{Fin}$
75 74 adantl ${⊢}\left({\phi }\wedge {z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\right)\to {z}\in \mathrm{Fin}$
76 72 7 73 75 uzfissfz ${⊢}\left({\phi }\wedge {z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\right)\to \exists {k}\in {Z}\phantom{\rule{.4em}{0ex}}{z}\subseteq \left({M}\dots {k}\right)$
77 76 adantr ${⊢}\left(\left({\phi }\wedge {z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\right)\wedge {O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)<\sum _{{n}\in {z}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\right)\to \exists {k}\in {Z}\phantom{\rule{.4em}{0ex}}{z}\subseteq \left({M}\dots {k}\right)$
78 54 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\right)\wedge {O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)<\sum _{{n}\in {z}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\right)\wedge {z}\subseteq \left({M}\dots {k}\right)\right)\to {O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)\in ℝ$
79 fzfid ${⊢}{z}\subseteq \left({M}\dots {k}\right)\to \left({M}\dots {k}\right)\in \mathrm{Fin}$
80 id ${⊢}{z}\subseteq \left({M}\dots {k}\right)\to {z}\subseteq \left({M}\dots {k}\right)$
81 ssfi ${⊢}\left(\left({M}\dots {k}\right)\in \mathrm{Fin}\wedge {z}\subseteq \left({M}\dots {k}\right)\right)\to {z}\in \mathrm{Fin}$
82 79 80 81 syl2anc ${⊢}{z}\subseteq \left({M}\dots {k}\right)\to {z}\in \mathrm{Fin}$
83 82 adantl ${⊢}\left({\phi }\wedge {z}\subseteq \left({M}\dots {k}\right)\right)\to {z}\in \mathrm{Fin}$
84 1 ad2antrr ${⊢}\left(\left({\phi }\wedge {z}\subseteq \left({M}\dots {k}\right)\right)\wedge {n}\in {z}\right)\to {O}\in \mathrm{OutMeas}$
85 4 ad2antrr ${⊢}\left(\left({\phi }\wedge {z}\subseteq \left({M}\dots {k}\right)\right)\wedge {n}\in {z}\right)\to {A}\subseteq {X}$
86 5 ad2antrr ${⊢}\left(\left({\phi }\wedge {z}\subseteq \left({M}\dots {k}\right)\right)\wedge {n}\in {z}\right)\to {O}\left({A}\right)\in ℝ$
87 inss1 ${⊢}{A}\cap {F}\left({n}\right)\subseteq {A}$
88 87 a1i ${⊢}\left(\left({\phi }\wedge {z}\subseteq \left({M}\dots {k}\right)\right)\wedge {n}\in {z}\right)\to {A}\cap {F}\left({n}\right)\subseteq {A}$
89 84 3 85 86 88 omessre ${⊢}\left(\left({\phi }\wedge {z}\subseteq \left({M}\dots {k}\right)\right)\wedge {n}\in {z}\right)\to {O}\left({A}\cap {F}\left({n}\right)\right)\in ℝ$
90 83 89 fsumrecl ${⊢}\left({\phi }\wedge {z}\subseteq \left({M}\dots {k}\right)\right)\to \sum _{{n}\in {z}}{O}\left({A}\cap {F}\left({n}\right)\right)\in ℝ$
91 9 rpred ${⊢}{\phi }\to {Y}\in ℝ$
92 91 adantr ${⊢}\left({\phi }\wedge {z}\subseteq \left({M}\dots {k}\right)\right)\to {Y}\in ℝ$
93 90 92 readdcld ${⊢}\left({\phi }\wedge {z}\subseteq \left({M}\dots {k}\right)\right)\to \sum _{{n}\in {z}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\in ℝ$
94 93 ad4ant14 ${⊢}\left(\left(\left({\phi }\wedge {z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\right)\wedge {O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)<\sum _{{n}\in {z}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\right)\wedge {z}\subseteq \left({M}\dots {k}\right)\right)\to \sum _{{n}\in {z}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\in ℝ$
95 fzfid ${⊢}{\phi }\to \left({M}\dots {k}\right)\in \mathrm{Fin}$
96 87 a1i ${⊢}{\phi }\to {A}\cap {F}\left({n}\right)\subseteq {A}$
97 1 3 4 5 96 omessre ${⊢}{\phi }\to {O}\left({A}\cap {F}\left({n}\right)\right)\in ℝ$
98 97 adantr ${⊢}\left({\phi }\wedge {n}\in \left({M}\dots {k}\right)\right)\to {O}\left({A}\cap {F}\left({n}\right)\right)\in ℝ$
99 95 98 fsumrecl ${⊢}{\phi }\to \sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)\in ℝ$
100 99 adantr ${⊢}\left({\phi }\wedge {z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\right)\to \sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)\in ℝ$
101 91 adantr ${⊢}\left({\phi }\wedge {z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\right)\to {Y}\in ℝ$
102 100 101 readdcld ${⊢}\left({\phi }\wedge {z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\right)\to \sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\in ℝ$
103 102 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge {z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\right)\wedge {O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)<\sum _{{n}\in {z}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\right)\wedge {z}\subseteq \left({M}\dots {k}\right)\right)\to \sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\in ℝ$
104 simplr ${⊢}\left(\left(\left({\phi }\wedge {z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\right)\wedge {O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)<\sum _{{n}\in {z}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\right)\wedge {z}\subseteq \left({M}\dots {k}\right)\right)\to {O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)<\sum _{{n}\in {z}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}$
105 99 adantr ${⊢}\left({\phi }\wedge {z}\subseteq \left({M}\dots {k}\right)\right)\to \sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)\in ℝ$
106 fzfid ${⊢}\left({\phi }\wedge {z}\subseteq \left({M}\dots {k}\right)\right)\to \left({M}\dots {k}\right)\in \mathrm{Fin}$
107 98 adantlr ${⊢}\left(\left({\phi }\wedge {z}\subseteq \left({M}\dots {k}\right)\right)\wedge {n}\in \left({M}\dots {k}\right)\right)\to {O}\left({A}\cap {F}\left({n}\right)\right)\in ℝ$
108 0xr ${⊢}0\in {ℝ}^{*}$
109 108 a1i ${⊢}\left({\phi }\wedge {n}\in \left({M}\dots {k}\right)\right)\to 0\in {ℝ}^{*}$
110 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
111 110 a1i ${⊢}\left({\phi }\wedge {n}\in \left({M}\dots {k}\right)\right)\to \mathrm{+\infty }\in {ℝ}^{*}$
112 1 3 20 omecl ${⊢}{\phi }\to {O}\left({A}\cap {F}\left({n}\right)\right)\in \left[0,\mathrm{+\infty }\right]$
113 112 adantr ${⊢}\left({\phi }\wedge {n}\in \left({M}\dots {k}\right)\right)\to {O}\left({A}\cap {F}\left({n}\right)\right)\in \left[0,\mathrm{+\infty }\right]$
114 iccgelb ${⊢}\left(0\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\wedge {O}\left({A}\cap {F}\left({n}\right)\right)\in \left[0,\mathrm{+\infty }\right]\right)\to 0\le {O}\left({A}\cap {F}\left({n}\right)\right)$
115 109 111 113 114 syl3anc ${⊢}\left({\phi }\wedge {n}\in \left({M}\dots {k}\right)\right)\to 0\le {O}\left({A}\cap {F}\left({n}\right)\right)$
116 115 adantlr ${⊢}\left(\left({\phi }\wedge {z}\subseteq \left({M}\dots {k}\right)\right)\wedge {n}\in \left({M}\dots {k}\right)\right)\to 0\le {O}\left({A}\cap {F}\left({n}\right)\right)$
117 simpr ${⊢}\left({\phi }\wedge {z}\subseteq \left({M}\dots {k}\right)\right)\to {z}\subseteq \left({M}\dots {k}\right)$
118 106 107 116 117 fsumless ${⊢}\left({\phi }\wedge {z}\subseteq \left({M}\dots {k}\right)\right)\to \sum _{{n}\in {z}}{O}\left({A}\cap {F}\left({n}\right)\right)\le \sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)$
119 90 105 92 118 leadd1dd ${⊢}\left({\phi }\wedge {z}\subseteq \left({M}\dots {k}\right)\right)\to \sum _{{n}\in {z}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\le \sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}$
120 119 ad4ant14 ${⊢}\left(\left(\left({\phi }\wedge {z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\right)\wedge {O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)<\sum _{{n}\in {z}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\right)\wedge {z}\subseteq \left({M}\dots {k}\right)\right)\to \sum _{{n}\in {z}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\le \sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}$
121 78 94 103 104 120 ltletrd ${⊢}\left(\left(\left({\phi }\wedge {z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\right)\wedge {O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)<\sum _{{n}\in {z}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\right)\wedge {z}\subseteq \left({M}\dots {k}\right)\right)\to {O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)<\sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}$
122 121 ex ${⊢}\left(\left({\phi }\wedge {z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\right)\wedge {O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)<\sum _{{n}\in {z}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\right)\to \left({z}\subseteq \left({M}\dots {k}\right)\to {O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)<\sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\right)$
123 122 reximdv ${⊢}\left(\left({\phi }\wedge {z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\right)\wedge {O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)<\sum _{{n}\in {z}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\right)\to \left(\exists {k}\in {Z}\phantom{\rule{.4em}{0ex}}{z}\subseteq \left({M}\dots {k}\right)\to \exists {k}\in {Z}\phantom{\rule{.4em}{0ex}}{O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)<\sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\right)$
124 77 123 mpd ${⊢}\left(\left({\phi }\wedge {z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\right)\wedge {O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)<\sum _{{n}\in {z}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\right)\to \exists {k}\in {Z}\phantom{\rule{.4em}{0ex}}{O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)<\sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}$
125 124 rexlimdva2 ${⊢}{\phi }\to \left(\exists {z}\in \left(𝒫{Z}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)<\sum _{{n}\in {z}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\to \exists {k}\in {Z}\phantom{\rule{.4em}{0ex}}{O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)<\sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\right)$
126 71 125 mpd ${⊢}{\phi }\to \exists {k}\in {Z}\phantom{\rule{.4em}{0ex}}{O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)<\sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}$
127 53 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in {Z}\right)\wedge {O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)<\sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\right)\to {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)={O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)$
128 simpr ${⊢}\left(\left({\phi }\wedge {k}\in {Z}\right)\wedge {O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)<\sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\right)\to {O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)<\sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}$
129 127 128 eqbrtrd ${⊢}\left(\left({\phi }\wedge {k}\in {Z}\right)\wedge {O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)<\sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\right)\to {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)<\sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}$
130 129 ex ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to \left({O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)<\sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\to {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)<\sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\right)$
131 130 reximdva ${⊢}{\phi }\to \left(\exists {k}\in {Z}\phantom{\rule{.4em}{0ex}}{O}\left(\bigcup _{{n}\in {Z}}\left({A}\cap {F}\left({n}\right)\right)\right)<\sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\to \exists {k}\in {Z}\phantom{\rule{.4em}{0ex}}{O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)<\sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\right)$
132 126 131 mpd ${⊢}{\phi }\to \exists {k}\in {Z}\phantom{\rule{.4em}{0ex}}{O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)<\sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}$
133 simpr ${⊢}\left(\left({\phi }\wedge {k}\in {Z}\right)\wedge {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)<\sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\right)\to {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)<\sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}$
134 1 adantr ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {O}\in \mathrm{OutMeas}$
135 4 adantr ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {A}\subseteq {X}$
136 5 adantr ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {O}\left({A}\right)\in ℝ$
137 8 adantr ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {E}:{Z}⟶{S}$
138 simpr ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {k}\in {Z}$
139 134 2 3 135 136 7 137 10 11 138 carageniuncllem1 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to \sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)={O}\left({A}\cap {G}\left({k}\right)\right)$
140 139 oveq1d ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to \sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}={O}\left({A}\cap {G}\left({k}\right)\right)+{Y}$
141 140 adantr ${⊢}\left(\left({\phi }\wedge {k}\in {Z}\right)\wedge {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)<\sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\right)\to \sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}={O}\left({A}\cap {G}\left({k}\right)\right)+{Y}$
142 133 141 breqtrd ${⊢}\left(\left({\phi }\wedge {k}\in {Z}\right)\wedge {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)<\sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\right)\to {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)<{O}\left({A}\cap {G}\left({k}\right)\right)+{Y}$
143 142 ex ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to \left({O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)<\sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\to {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)<{O}\left({A}\cap {G}\left({k}\right)\right)+{Y}\right)$
144 143 reximdva ${⊢}{\phi }\to \left(\exists {k}\in {Z}\phantom{\rule{.4em}{0ex}}{O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)<\sum _{{n}={M}}^{{k}}{O}\left({A}\cap {F}\left({n}\right)\right)+{Y}\to \exists {k}\in {Z}\phantom{\rule{.4em}{0ex}}{O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)<{O}\left({A}\cap {G}\left({k}\right)\right)+{Y}\right)$
145 132 144 mpd ${⊢}{\phi }\to \exists {k}\in {Z}\phantom{\rule{.4em}{0ex}}{O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)<{O}\left({A}\cap {G}\left({k}\right)\right)+{Y}$
146 14 3ad2ant1 ${⊢}\left({\phi }\wedge {k}\in {Z}\wedge {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)<{O}\left({A}\cap {G}\left({k}\right)\right)+{Y}\right)\to {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)\in ℝ$
147 16 3ad2ant1 ${⊢}\left({\phi }\wedge {k}\in {Z}\wedge {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)<{O}\left({A}\cap {G}\left({k}\right)\right)+{Y}\right)\to {O}\left({A}\setminus \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)\in ℝ$
148 inss1 ${⊢}{A}\cap {G}\left({k}\right)\subseteq {A}$
149 148 a1i ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {A}\cap {G}\left({k}\right)\subseteq {A}$
150 134 3 135 136 149 omessre ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {O}\left({A}\cap {G}\left({k}\right)\right)\in ℝ$
151 91 adantr ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {Y}\in ℝ$
152 150 151 readdcld ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {O}\left({A}\cap {G}\left({k}\right)\right)+{Y}\in ℝ$
153 152 3adant3 ${⊢}\left({\phi }\wedge {k}\in {Z}\wedge {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)<{O}\left({A}\cap {G}\left({k}\right)\right)+{Y}\right)\to {O}\left({A}\cap {G}\left({k}\right)\right)+{Y}\in ℝ$
154 difssd ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {A}\setminus {G}\left({k}\right)\subseteq {A}$
155 134 3 135 136 154 omessre ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {O}\left({A}\setminus {G}\left({k}\right)\right)\in ℝ$
156 155 3adant3 ${⊢}\left({\phi }\wedge {k}\in {Z}\wedge {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)<{O}\left({A}\cap {G}\left({k}\right)\right)+{Y}\right)\to {O}\left({A}\setminus {G}\left({k}\right)\right)\in ℝ$
157 simp3 ${⊢}\left({\phi }\wedge {k}\in {Z}\wedge {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)<{O}\left({A}\cap {G}\left({k}\right)\right)+{Y}\right)\to {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)<{O}\left({A}\cap {G}\left({k}\right)\right)+{Y}$
158 146 153 157 ltled ${⊢}\left({\phi }\wedge {k}\in {Z}\wedge {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)<{O}\left({A}\cap {G}\left({k}\right)\right)+{Y}\right)\to {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)\le {O}\left({A}\cap {G}\left({k}\right)\right)+{Y}$
159 135 ssdifssd ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {A}\setminus {G}\left({k}\right)\subseteq {X}$
160 oveq2 ${⊢}{n}={k}\to \left({M}\dots {n}\right)=\left({M}\dots {k}\right)$
161 160 iuneq1d ${⊢}{n}={k}\to \bigcup _{{i}={M}}^{{n}}{E}\left({i}\right)=\bigcup _{{i}={M}}^{{k}}{E}\left({i}\right)$
162 ovex ${⊢}\left({M}\dots {k}\right)\in \mathrm{V}$
163 fvex ${⊢}{E}\left({i}\right)\in \mathrm{V}$
164 162 163 iunex ${⊢}\bigcup _{{i}={M}}^{{k}}{E}\left({i}\right)\in \mathrm{V}$
165 161 10 164 fvmpt ${⊢}{k}\in {Z}\to {G}\left({k}\right)=\bigcup _{{i}={M}}^{{k}}{E}\left({i}\right)$
166 fveq2 ${⊢}{i}={n}\to {E}\left({i}\right)={E}\left({n}\right)$
167 166 cbviunv ${⊢}\bigcup _{{i}={M}}^{{k}}{E}\left({i}\right)=\bigcup _{{n}={M}}^{{k}}{E}\left({n}\right)$
168 167 a1i ${⊢}{k}\in {Z}\to \bigcup _{{i}={M}}^{{k}}{E}\left({i}\right)=\bigcup _{{n}={M}}^{{k}}{E}\left({n}\right)$
169 165 168 eqtrd ${⊢}{k}\in {Z}\to {G}\left({k}\right)=\bigcup _{{n}={M}}^{{k}}{E}\left({n}\right)$
170 elfzuz ${⊢}{i}\in \left({M}\dots {k}\right)\to {i}\in {ℤ}_{\ge {M}}$
171 7 eqcomi ${⊢}{ℤ}_{\ge {M}}={Z}$
172 171 a1i ${⊢}{i}\in \left({M}\dots {k}\right)\to {ℤ}_{\ge {M}}={Z}$
173 170 172 eleqtrd ${⊢}{i}\in \left({M}\dots {k}\right)\to {i}\in {Z}$
174 173 ssriv ${⊢}\left({M}\dots {k}\right)\subseteq {Z}$
175 iunss1 ${⊢}\left({M}\dots {k}\right)\subseteq {Z}\to \bigcup _{{n}={M}}^{{k}}{E}\left({n}\right)\subseteq \bigcup _{{n}\in {Z}}{E}\left({n}\right)$
176 174 175 ax-mp ${⊢}\bigcup _{{n}={M}}^{{k}}{E}\left({n}\right)\subseteq \bigcup _{{n}\in {Z}}{E}\left({n}\right)$
177 176 a1i ${⊢}{k}\in {Z}\to \bigcup _{{n}={M}}^{{k}}{E}\left({n}\right)\subseteq \bigcup _{{n}\in {Z}}{E}\left({n}\right)$
178 169 177 eqsstrd ${⊢}{k}\in {Z}\to {G}\left({k}\right)\subseteq \bigcup _{{n}\in {Z}}{E}\left({n}\right)$
179 178 adantl ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {G}\left({k}\right)\subseteq \bigcup _{{n}\in {Z}}{E}\left({n}\right)$
180 179 sscond ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {A}\setminus \bigcup _{{n}\in {Z}}{E}\left({n}\right)\subseteq {A}\setminus {G}\left({k}\right)$
181 134 3 159 180 omessle ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {O}\left({A}\setminus \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)\le {O}\left({A}\setminus {G}\left({k}\right)\right)$
182 181 3adant3 ${⊢}\left({\phi }\wedge {k}\in {Z}\wedge {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)<{O}\left({A}\cap {G}\left({k}\right)\right)+{Y}\right)\to {O}\left({A}\setminus \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)\le {O}\left({A}\setminus {G}\left({k}\right)\right)$
183 146 147 153 156 158 182 le2addd ${⊢}\left({\phi }\wedge {k}\in {Z}\wedge {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)<{O}\left({A}\cap {G}\left({k}\right)\right)+{Y}\right)\to {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)+{O}\left({A}\setminus \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)\le {O}\left({A}\cap {G}\left({k}\right)\right)+{Y}+{O}\left({A}\setminus {G}\left({k}\right)\right)$
184 150 recnd ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {O}\left({A}\cap {G}\left({k}\right)\right)\in ℂ$
185 91 recnd ${⊢}{\phi }\to {Y}\in ℂ$
186 185 adantr ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {Y}\in ℂ$
187 155 recnd ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {O}\left({A}\setminus {G}\left({k}\right)\right)\in ℂ$
188 184 186 187 add32d ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {O}\left({A}\cap {G}\left({k}\right)\right)+{Y}+{O}\left({A}\setminus {G}\left({k}\right)\right)={O}\left({A}\cap {G}\left({k}\right)\right)+{O}\left({A}\setminus {G}\left({k}\right)\right)+{Y}$
189 rexadd ${⊢}\left({O}\left({A}\cap {G}\left({k}\right)\right)\in ℝ\wedge {O}\left({A}\setminus {G}\left({k}\right)\right)\in ℝ\right)\to {O}\left({A}\cap {G}\left({k}\right)\right){+}_{𝑒}{O}\left({A}\setminus {G}\left({k}\right)\right)={O}\left({A}\cap {G}\left({k}\right)\right)+{O}\left({A}\setminus {G}\left({k}\right)\right)$
190 150 155 189 syl2anc ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {O}\left({A}\cap {G}\left({k}\right)\right){+}_{𝑒}{O}\left({A}\setminus {G}\left({k}\right)\right)={O}\left({A}\cap {G}\left({k}\right)\right)+{O}\left({A}\setminus {G}\left({k}\right)\right)$
191 190 eqcomd ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {O}\left({A}\cap {G}\left({k}\right)\right)+{O}\left({A}\setminus {G}\left({k}\right)\right)={O}\left({A}\cap {G}\left({k}\right)\right){+}_{𝑒}{O}\left({A}\setminus {G}\left({k}\right)\right)$
192 nfv ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}{\phi }$
193 8 adantr ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\right)\to {E}:{Z}⟶{S}$
194 173 adantl ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\right)\to {i}\in {Z}$
195 193 194 ffvelrnd ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\right)\to {E}\left({i}\right)\in {S}$
196 192 1 2 95 195 caragenfiiuncl ${⊢}{\phi }\to \bigcup _{{i}={M}}^{{k}}{E}\left({i}\right)\in {S}$
197 196 adantr ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to \bigcup _{{i}={M}}^{{k}}{E}\left({i}\right)\in {S}$
198 10 161 138 197 fvmptd3 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {G}\left({k}\right)=\bigcup _{{i}={M}}^{{k}}{E}\left({i}\right)$
199 198 197 eqeltrd ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {G}\left({k}\right)\in {S}$
200 134 2 3 199 135 caragensplit ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {O}\left({A}\cap {G}\left({k}\right)\right){+}_{𝑒}{O}\left({A}\setminus {G}\left({k}\right)\right)={O}\left({A}\right)$
201 191 200 eqtrd ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {O}\left({A}\cap {G}\left({k}\right)\right)+{O}\left({A}\setminus {G}\left({k}\right)\right)={O}\left({A}\right)$
202 201 oveq1d ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {O}\left({A}\cap {G}\left({k}\right)\right)+{O}\left({A}\setminus {G}\left({k}\right)\right)+{Y}={O}\left({A}\right)+{Y}$
203 188 202 eqtrd ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {O}\left({A}\cap {G}\left({k}\right)\right)+{Y}+{O}\left({A}\setminus {G}\left({k}\right)\right)={O}\left({A}\right)+{Y}$
204 203 3adant3 ${⊢}\left({\phi }\wedge {k}\in {Z}\wedge {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)<{O}\left({A}\cap {G}\left({k}\right)\right)+{Y}\right)\to {O}\left({A}\cap {G}\left({k}\right)\right)+{Y}+{O}\left({A}\setminus {G}\left({k}\right)\right)={O}\left({A}\right)+{Y}$
205 183 204 breqtrd ${⊢}\left({\phi }\wedge {k}\in {Z}\wedge {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)<{O}\left({A}\cap {G}\left({k}\right)\right)+{Y}\right)\to {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)+{O}\left({A}\setminus \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)\le {O}\left({A}\right)+{Y}$
206 205 3exp ${⊢}{\phi }\to \left({k}\in {Z}\to \left({O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)<{O}\left({A}\cap {G}\left({k}\right)\right)+{Y}\to {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)+{O}\left({A}\setminus \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)\le {O}\left({A}\right)+{Y}\right)\right)$
207 206 rexlimdv ${⊢}{\phi }\to \left(\exists {k}\in {Z}\phantom{\rule{.4em}{0ex}}{O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)<{O}\left({A}\cap {G}\left({k}\right)\right)+{Y}\to {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)+{O}\left({A}\setminus \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)\le {O}\left({A}\right)+{Y}\right)$
208 145 207 mpd ${⊢}{\phi }\to {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)+{O}\left({A}\setminus \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)\le {O}\left({A}\right)+{Y}$
209 18 208 eqbrtrd ${⊢}{\phi }\to {O}\left({A}\cap \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right){+}_{𝑒}{O}\left({A}\setminus \bigcup _{{n}\in {Z}}{E}\left({n}\right)\right)\le {O}\left({A}\right)+{Y}$