Metamath Proof Explorer

Theorem ismblfin

Description: Measurability in terms of inner and outer measure. Proposition 7 of Viaclovsky8 p. 3. (Contributed by Brendan Leahy, 4-Mar-2018) (Revised by Brendan Leahy, 28-Mar-2018)

Ref Expression
Assertion ismblfin ${⊢}\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\to \left({A}\in \mathrm{dom}vol↔{vol}^{*}\left({A}\right)=sup\left(\left\{{y}|\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {y}=vol\left({b}\right)\right)\right\},ℝ,<\right)\right)$

Proof

Step Hyp Ref Expression
1 mblfinlem4 ${⊢}\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge {A}\in \mathrm{dom}vol\right)\to {vol}^{*}\left({A}\right)=sup\left(\left\{{y}|\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {y}=vol\left({b}\right)\right)\right\},ℝ,<\right)$
2 elpwi ${⊢}{w}\in 𝒫ℝ\to {w}\subseteq ℝ$
3 elmapi ${⊢}{f}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\to {f}:ℕ⟶\le \cap {ℝ}^{2}$
4 inss1 ${⊢}{w}\cap {A}\subseteq {w}$
5 ovolsscl ${⊢}\left({w}\cap {A}\subseteq {w}\wedge {w}\subseteq ℝ\wedge {vol}^{*}\left({w}\right)\in ℝ\right)\to {vol}^{*}\left({w}\cap {A}\right)\in ℝ$
6 4 5 mp3an1 ${⊢}\left({w}\subseteq ℝ\wedge {vol}^{*}\left({w}\right)\in ℝ\right)\to {vol}^{*}\left({w}\cap {A}\right)\in ℝ$
7 difss ${⊢}{w}\setminus {A}\subseteq {w}$
8 ovolsscl ${⊢}\left({w}\setminus {A}\subseteq {w}\wedge {w}\subseteq ℝ\wedge {vol}^{*}\left({w}\right)\in ℝ\right)\to {vol}^{*}\left({w}\setminus {A}\right)\in ℝ$
9 7 8 mp3an1 ${⊢}\left({w}\subseteq ℝ\wedge {vol}^{*}\left({w}\right)\in ℝ\right)\to {vol}^{*}\left({w}\setminus {A}\right)\in ℝ$
10 6 9 readdcld ${⊢}\left({w}\subseteq ℝ\wedge {vol}^{*}\left({w}\right)\in ℝ\right)\to {vol}^{*}\left({w}\cap {A}\right)+{vol}^{*}\left({w}\setminus {A}\right)\in ℝ$
11 10 rexrd ${⊢}\left({w}\subseteq ℝ\wedge {vol}^{*}\left({w}\right)\in ℝ\right)\to {vol}^{*}\left({w}\cap {A}\right)+{vol}^{*}\left({w}\setminus {A}\right)\in {ℝ}^{*}$
12 11 ad3antlr ${⊢}\left(\left(\left(\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge {vol}^{*}\left({A}\right)=sup\left(\left\{{y}|\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {y}=vol\left({b}\right)\right)\right\},ℝ,<\right)\right)\wedge \left({w}\subseteq ℝ\wedge {vol}^{*}\left({w}\right)\in ℝ\right)\right)\wedge {f}:ℕ⟶\le \cap {ℝ}^{2}\right)\wedge {w}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\to {vol}^{*}\left({w}\cap {A}\right)+{vol}^{*}\left({w}\setminus {A}\right)\in {ℝ}^{*}$
13 rncoss ${⊢}\mathrm{ran}\left(\left(.\right)\circ {f}\right)\subseteq \mathrm{ran}\left(.\right)$
14 13 unissi ${⊢}\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\subseteq \bigcup \mathrm{ran}\left(.\right)$
15 unirnioo ${⊢}ℝ=\bigcup \mathrm{ran}\left(.\right)$
16 14 15 sseqtrri ${⊢}\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\subseteq ℝ$
17 ovolcl ${⊢}\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\subseteq ℝ\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in {ℝ}^{*}$
18 16 17 mp1i ${⊢}\left(\left(\left(\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge {vol}^{*}\left({A}\right)=sup\left(\left\{{y}|\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {y}=vol\left({b}\right)\right)\right\},ℝ,<\right)\right)\wedge \left({w}\subseteq ℝ\wedge {vol}^{*}\left({w}\right)\in ℝ\right)\right)\wedge {f}:ℕ⟶\le \cap {ℝ}^{2}\right)\wedge {w}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in {ℝ}^{*}$
19 eqid ${⊢}\left(\mathrm{abs}\circ -\right)\circ {f}=\left(\mathrm{abs}\circ -\right)\circ {f}$
20 eqid ${⊢}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right)=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right)$
21 19 20 ovolsf ${⊢}{f}:ℕ⟶\le \cap {ℝ}^{2}\to seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right):ℕ⟶\left[0,\mathrm{+\infty }\right)$
22 frn ${⊢}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right):ℕ⟶\left[0,\mathrm{+\infty }\right)\to \mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right)\subseteq \left[0,\mathrm{+\infty }\right)$
23 icossxr ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq {ℝ}^{*}$
24 22 23 sstrdi ${⊢}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right):ℕ⟶\left[0,\mathrm{+\infty }\right)\to \mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right)\subseteq {ℝ}^{*}$
25 supxrcl ${⊢}\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right)\subseteq {ℝ}^{*}\to sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)\in {ℝ}^{*}$
26 21 24 25 3syl ${⊢}{f}:ℕ⟶\le \cap {ℝ}^{2}\to sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)\in {ℝ}^{*}$
27 26 ad2antlr ${⊢}\left(\left(\left(\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge {vol}^{*}\left({A}\right)=sup\left(\left\{{y}|\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {y}=vol\left({b}\right)\right)\right\},ℝ,<\right)\right)\wedge \left({w}\subseteq ℝ\wedge {vol}^{*}\left({w}\right)\in ℝ\right)\right)\wedge {f}:ℕ⟶\le \cap {ℝ}^{2}\right)\wedge {w}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\to sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)\in {ℝ}^{*}$
28 pnfge ${⊢}{vol}^{*}\left({w}\cap {A}\right)+{vol}^{*}\left({w}\setminus {A}\right)\in {ℝ}^{*}\to {vol}^{*}\left({w}\cap {A}\right)+{vol}^{*}\left({w}\setminus {A}\right)\le \mathrm{+\infty }$
29 11 28 syl ${⊢}\left({w}\subseteq ℝ\wedge {vol}^{*}\left({w}\right)\in ℝ\right)\to {vol}^{*}\left({w}\cap {A}\right)+{vol}^{*}\left({w}\setminus {A}\right)\le \mathrm{+\infty }$
30 29 ad2antrr ${⊢}\left(\left(\left({w}\subseteq ℝ\wedge {vol}^{*}\left({w}\right)\in ℝ\right)\wedge {w}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)=\mathrm{+\infty }\right)\to {vol}^{*}\left({w}\cap {A}\right)+{vol}^{*}\left({w}\setminus {A}\right)\le \mathrm{+\infty }$
31 simpr ${⊢}\left(\left(\left({w}\subseteq ℝ\wedge {vol}^{*}\left({w}\right)\in ℝ\right)\wedge {w}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)=\mathrm{+\infty }\right)\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)=\mathrm{+\infty }$
32 30 31 breqtrrd ${⊢}\left(\left(\left({w}\subseteq ℝ\wedge {vol}^{*}\left({w}\right)\in ℝ\right)\wedge {w}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)=\mathrm{+\infty }\right)\to {vol}^{*}\left({w}\cap {A}\right)+{vol}^{*}\left({w}\setminus {A}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)$
33 32 adantlll ${⊢}\left(\left(\left(\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge {vol}^{*}\left({A}\right)=sup\left(\left\{{y}|\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {y}=vol\left({b}\right)\right)\right\},ℝ,<\right)\right)\wedge \left({w}\subseteq ℝ\wedge {vol}^{*}\left({w}\right)\in ℝ\right)\right)\wedge {w}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)=\mathrm{+\infty }\right)\to {vol}^{*}\left({w}\cap {A}\right)+{vol}^{*}\left({w}\setminus {A}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)$
34 16 17 ax-mp ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in {ℝ}^{*}$
35 nltpnft ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in {ℝ}^{*}\to \left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)=\mathrm{+\infty }↔¬{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)<\mathrm{+\infty }\right)$
36 34 35 ax-mp ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)=\mathrm{+\infty }↔¬{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)<\mathrm{+\infty }$
37 36 necon2abii ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)<\mathrm{+\infty }↔{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\ne \mathrm{+\infty }$
38 ovolge0 ${⊢}\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\subseteq ℝ\to 0\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)$
39 16 38 ax-mp ${⊢}0\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)$
40 0re ${⊢}0\in ℝ$
41 xrre3 ${⊢}\left(\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in {ℝ}^{*}\wedge 0\in ℝ\right)\wedge \left(0\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)<\mathrm{+\infty }\right)\right)\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ$
42 34 40 41 mpanl12 ${⊢}\left(0\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)<\mathrm{+\infty }\right)\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ$
43 39 42 mpan ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)<\mathrm{+\infty }\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ$
44 37 43 sylbir ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\ne \mathrm{+\infty }\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ$
45 10 ad3antlr ${⊢}\left(\left(\left(\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge {vol}^{*}\left({A}\right)=sup\left(\left\{{y}|\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {y}=vol\left({b}\right)\right)\right\},ℝ,<\right)\right)\wedge \left({w}\subseteq ℝ\wedge {vol}^{*}\left({w}\right)\in ℝ\right)\right)\wedge {w}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to {vol}^{*}\left({w}\cap {A}\right)+{vol}^{*}\left({w}\setminus {A}\right)\in ℝ$
46 simpr ${⊢}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\to {z}=vol\left({a}\right)$
47 eleq1w ${⊢}{b}={a}\to \left({b}\in \mathrm{dom}vol↔{a}\in \mathrm{dom}vol\right)$
48 uniretop ${⊢}ℝ=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
49 48 cldss ${⊢}{b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\to {b}\subseteq ℝ$
50 dfss4 ${⊢}{b}\subseteq ℝ↔ℝ\setminus \left(ℝ\setminus {b}\right)={b}$
51 49 50 sylib ${⊢}{b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\to ℝ\setminus \left(ℝ\setminus {b}\right)={b}$
52 rembl ${⊢}ℝ\in \mathrm{dom}vol$
53 48 cldopn ${⊢}{b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\to ℝ\setminus {b}\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
54 opnmbl ${⊢}ℝ\setminus {b}\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\to ℝ\setminus {b}\in \mathrm{dom}vol$
55 53 54 syl ${⊢}{b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\to ℝ\setminus {b}\in \mathrm{dom}vol$
56 difmbl ${⊢}\left(ℝ\in \mathrm{dom}vol\wedge ℝ\setminus {b}\in \mathrm{dom}vol\right)\to ℝ\setminus \left(ℝ\setminus {b}\right)\in \mathrm{dom}vol$
57 52 55 56 sylancr ${⊢}{b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\to ℝ\setminus \left(ℝ\setminus {b}\right)\in \mathrm{dom}vol$
58 51 57 eqeltrrd ${⊢}{b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\to {b}\in \mathrm{dom}vol$
59 47 58 vtoclga ${⊢}{a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\to {a}\in \mathrm{dom}vol$
60 mblvol ${⊢}{a}\in \mathrm{dom}vol\to vol\left({a}\right)={vol}^{*}\left({a}\right)$
61 59 60 syl ${⊢}{a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\to vol\left({a}\right)={vol}^{*}\left({a}\right)$
62 46 61 sylan9eqr ${⊢}\left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge \left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right)\to {z}={vol}^{*}\left({a}\right)$
63 62 adantl ${⊢}\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge \left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right)\right)\to {z}={vol}^{*}\left({a}\right)$
64 inss1 ${⊢}\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)$
65 sstr ${⊢}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\to {a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)$
66 64 65 mpan2 ${⊢}{a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\to {a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)$
67 66 ad2antrl ${⊢}\left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge \left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right)\to {a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)$
68 ovolsscl ${⊢}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\subseteq ℝ\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to {vol}^{*}\left({a}\right)\in ℝ$
69 16 68 mp3an2 ${⊢}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to {vol}^{*}\left({a}\right)\in ℝ$
70 69 ancoms ${⊢}\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge {a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\to {vol}^{*}\left({a}\right)\in ℝ$
71 67 70 sylan2 ${⊢}\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge \left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right)\right)\to {vol}^{*}\left({a}\right)\in ℝ$
72 63 71 eqeltrd ${⊢}\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge \left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right)\right)\to {z}\in ℝ$
73 72 rexlimdvaa ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\to \left(\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\to {z}\in ℝ\right)$
74 73 abssdv ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\to \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\subseteq ℝ$
75 eqeq1 ${⊢}{z}={y}\to \left({z}=vol\left({a}\right)↔{y}=vol\left({a}\right)\right)$
76 75 anbi2d ${⊢}{z}={y}\to \left(\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)↔\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {y}=vol\left({a}\right)\right)\right)$
77 76 rexbidv ${⊢}{z}={y}\to \left(\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)↔\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {y}=vol\left({a}\right)\right)\right)$
78 77 ralab ${⊢}\forall {y}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{y}\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left(\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {y}=vol\left({a}\right)\right)\to {y}\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\right)$
79 simpr ${⊢}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {y}=vol\left({a}\right)\right)\to {y}=vol\left({a}\right)$
80 79 61 sylan9eqr ${⊢}\left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge \left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {y}=vol\left({a}\right)\right)\right)\to {y}={vol}^{*}\left({a}\right)$
81 ovolss ${⊢}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\subseteq ℝ\right)\to {vol}^{*}\left({a}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)$
82 66 16 81 sylancl ${⊢}{a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\to {vol}^{*}\left({a}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)$
83 82 ad2antrl ${⊢}\left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge \left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {y}=vol\left({a}\right)\right)\right)\to {vol}^{*}\left({a}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)$
84 80 83 eqbrtrd ${⊢}\left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge \left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {y}=vol\left({a}\right)\right)\right)\to {y}\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)$
85 84 rexlimiva ${⊢}\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {y}=vol\left({a}\right)\right)\to {y}\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)$
86 78 85 mpgbir ${⊢}\forall {y}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{y}\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)$
87 brralrspcev ${⊢}\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \forall {y}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{y}\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{y}\le {x}$
88 86 87 mpan2 ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{y}\le {x}$
89 retop ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$
90 0cld ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}\to \varnothing \in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$
91 89 90 ax-mp ${⊢}\varnothing \in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$
92 0ss ${⊢}\varnothing \subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}$
93 0mbl ${⊢}\varnothing \in \mathrm{dom}vol$
94 mblvol ${⊢}\varnothing \in \mathrm{dom}vol\to vol\left(\varnothing \right)={vol}^{*}\left(\varnothing \right)$
95 93 94 ax-mp ${⊢}vol\left(\varnothing \right)={vol}^{*}\left(\varnothing \right)$
96 ovol0 ${⊢}{vol}^{*}\left(\varnothing \right)=0$
97 95 96 eqtr2i ${⊢}0=vol\left(\varnothing \right)$
98 92 97 pm3.2i ${⊢}\left(\varnothing \subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge 0=vol\left(\varnothing \right)\right)$
99 sseq1 ${⊢}{a}=\varnothing \to \left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}↔\varnothing \subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\right)$
100 fveq2 ${⊢}{a}=\varnothing \to vol\left({a}\right)=vol\left(\varnothing \right)$
101 100 eqeq2d ${⊢}{a}=\varnothing \to \left(0=vol\left({a}\right)↔0=vol\left(\varnothing \right)\right)$
102 99 101 anbi12d ${⊢}{a}=\varnothing \to \left(\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge 0=vol\left({a}\right)\right)↔\left(\varnothing \subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge 0=vol\left(\varnothing \right)\right)\right)$
103 102 rspcev ${⊢}\left(\varnothing \in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge \left(\varnothing \subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge 0=vol\left(\varnothing \right)\right)\right)\to \exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge 0=vol\left({a}\right)\right)$
104 91 98 103 mp2an ${⊢}\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge 0=vol\left({a}\right)\right)$
105 c0ex ${⊢}0\in \mathrm{V}$
106 eqeq1 ${⊢}{z}=0\to \left({z}=vol\left({a}\right)↔0=vol\left({a}\right)\right)$
107 106 anbi2d ${⊢}{z}=0\to \left(\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)↔\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge 0=vol\left({a}\right)\right)\right)$
108 107 rexbidv ${⊢}{z}=0\to \left(\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)↔\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge 0=vol\left({a}\right)\right)\right)$
109 105 108 elab ${⊢}0\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}↔\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge 0=vol\left({a}\right)\right)$
110 104 109 mpbir ${⊢}0\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}$
111 110 ne0ii ${⊢}\left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\ne \varnothing$
112 suprcl ${⊢}\left(\left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\subseteq ℝ\wedge \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to sup\left(\left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\},ℝ,<\right)\in ℝ$
113 111 112 mp3an2 ${⊢}\left(\left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\subseteq ℝ\wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to sup\left(\left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\},ℝ,<\right)\in ℝ$
114 74 88 113 syl2anc ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\to sup\left(\left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\},ℝ,<\right)\in ℝ$
115 simpr ${⊢}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\to {z}=vol\left({c}\right)$
116 eleq1w ${⊢}{b}={c}\to \left({b}\in \mathrm{dom}vol↔{c}\in \mathrm{dom}vol\right)$
117 116 58 vtoclga ${⊢}{c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\to {c}\in \mathrm{dom}vol$
118 mblvol ${⊢}{c}\in \mathrm{dom}vol\to vol\left({c}\right)={vol}^{*}\left({c}\right)$
119 117 118 syl ${⊢}{c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\to vol\left({c}\right)={vol}^{*}\left({c}\right)$
120 115 119 sylan9eqr ${⊢}\left({c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge \left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right)\to {z}={vol}^{*}\left({c}\right)$
121 120 adantl ${⊢}\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \left({c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge \left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right)\right)\to {z}={vol}^{*}\left({c}\right)$
122 difss2 ${⊢}{c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\to {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)$
123 122 ad2antrl ${⊢}\left({c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge \left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right)\to {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)$
124 ovolsscl ${⊢}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\subseteq ℝ\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to {vol}^{*}\left({c}\right)\in ℝ$
125 16 124 mp3an2 ${⊢}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to {vol}^{*}\left({c}\right)\in ℝ$
126 125 ancoms ${⊢}\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\to {vol}^{*}\left({c}\right)\in ℝ$
127 123 126 sylan2 ${⊢}\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \left({c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge \left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right)\right)\to {vol}^{*}\left({c}\right)\in ℝ$
128 121 127 eqeltrd ${⊢}\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \left({c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge \left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right)\right)\to {z}\in ℝ$
129 128 rexlimdvaa ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\to \left(\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\to {z}\in ℝ\right)$
130 129 abssdv ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\to \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\subseteq ℝ$
131 eqeq1 ${⊢}{z}={y}\to \left({z}=vol\left({c}\right)↔{y}=vol\left({c}\right)\right)$
132 131 anbi2d ${⊢}{z}={y}\to \left(\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)↔\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {y}=vol\left({c}\right)\right)\right)$
133 132 rexbidv ${⊢}{z}={y}\to \left(\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)↔\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {y}=vol\left({c}\right)\right)\right)$
134 133 ralab ${⊢}\forall {y}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{y}\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left(\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {y}=vol\left({c}\right)\right)\to {y}\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\right)$
135 simpr ${⊢}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {y}=vol\left({c}\right)\right)\to {y}=vol\left({c}\right)$
136 135 119 sylan9eqr ${⊢}\left({c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge \left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {y}=vol\left({c}\right)\right)\right)\to {y}={vol}^{*}\left({c}\right)$
137 ovolss ${⊢}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\subseteq ℝ\right)\to {vol}^{*}\left({c}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)$
138 122 16 137 sylancl ${⊢}{c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\to {vol}^{*}\left({c}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)$
139 138 ad2antrl ${⊢}\left({c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge \left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {y}=vol\left({c}\right)\right)\right)\to {vol}^{*}\left({c}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)$
140 136 139 eqbrtrd ${⊢}\left({c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge \left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {y}=vol\left({c}\right)\right)\right)\to {y}\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)$
141 140 rexlimiva ${⊢}\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {y}=vol\left({c}\right)\right)\to {y}\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)$
142 134 141 mpgbir ${⊢}\forall {y}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{y}\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)$
143 brralrspcev ${⊢}\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \forall {y}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{y}\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{y}\le {x}$
144 142 143 mpan2 ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{y}\le {x}$
145 0ss ${⊢}\varnothing \subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}$
146 145 97 pm3.2i ${⊢}\left(\varnothing \subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge 0=vol\left(\varnothing \right)\right)$
147 sseq1 ${⊢}{c}=\varnothing \to \left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}↔\varnothing \subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)$
148 fveq2 ${⊢}{c}=\varnothing \to vol\left({c}\right)=vol\left(\varnothing \right)$
149 148 eqeq2d ${⊢}{c}=\varnothing \to \left(0=vol\left({c}\right)↔0=vol\left(\varnothing \right)\right)$
150 147 149 anbi12d ${⊢}{c}=\varnothing \to \left(\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge 0=vol\left({c}\right)\right)↔\left(\varnothing \subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge 0=vol\left(\varnothing \right)\right)\right)$
151 150 rspcev ${⊢}\left(\varnothing \in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge \left(\varnothing \subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge 0=vol\left(\varnothing \right)\right)\right)\to \exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge 0=vol\left({c}\right)\right)$
152 91 146 151 mp2an ${⊢}\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge 0=vol\left({c}\right)\right)$
153 eqeq1 ${⊢}{z}=0\to \left({z}=vol\left({c}\right)↔0=vol\left({c}\right)\right)$
154 153 anbi2d ${⊢}{z}=0\to \left(\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)↔\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge 0=vol\left({c}\right)\right)\right)$
155 154 rexbidv ${⊢}{z}=0\to \left(\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)↔\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge 0=vol\left({c}\right)\right)\right)$
156 105 155 elab ${⊢}0\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}↔\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge 0=vol\left({c}\right)\right)$
157 152 156 mpbir ${⊢}0\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}$
158 157 ne0ii ${⊢}\left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\ne \varnothing$
159 suprcl ${⊢}\left(\left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\subseteq ℝ\wedge \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to sup\left(\left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\},ℝ,<\right)\in ℝ$
160 158 159 mp3an2 ${⊢}\left(\left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\subseteq ℝ\wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to sup\left(\left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\},ℝ,<\right)\in ℝ$
161 130 144 160 syl2anc ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\to sup\left(\left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\},ℝ,<\right)\in ℝ$
162 114 161 readdcld ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\to sup\left(\left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\},ℝ,<\right)+sup\left(\left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\},ℝ,<\right)\in ℝ$
163 162 adantl ${⊢}\left(\left(\left(\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge {vol}^{*}\left({A}\right)=sup\left(\left\{{y}|\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {y}=vol\left({b}\right)\right)\right\},ℝ,<\right)\right)\wedge \left({w}\subseteq ℝ\wedge {vol}^{*}\left({w}\right)\in ℝ\right)\right)\wedge {w}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to sup\left(\left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\},ℝ,<\right)+sup\left(\left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\},ℝ,<\right)\in ℝ$
164 simpr ${⊢}\left(\left(\left(\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge {vol}^{*}\left({A}\right)=sup\left(\left\{{y}|\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {y}=vol\left({b}\right)\right)\right\},ℝ,<\right)\right)\wedge \left({w}\subseteq ℝ\wedge {vol}^{*}\left({w}\right)\in ℝ\right)\right)\wedge {w}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ$
165 6 ad2antrr ${⊢}\left(\left(\left({w}\subseteq ℝ\wedge {vol}^{*}\left({w}\right)\in ℝ\right)\wedge {w}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to {vol}^{*}\left({w}\cap {A}\right)\in ℝ$
166 9 ad2antrr ${⊢}\left(\left(\left({w}\subseteq ℝ\wedge {vol}^{*}\left({w}\right)\in ℝ\right)\wedge {w}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to {vol}^{*}\left({w}\setminus {A}\right)\in ℝ$
167 ovolsscl ${⊢}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\subseteq ℝ\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\right)\in ℝ$
168 64 16 167 mp3an12 ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\right)\in ℝ$
169 168 adantl ${⊢}\left(\left(\left({w}\subseteq ℝ\wedge {vol}^{*}\left({w}\right)\in ℝ\right)\wedge {w}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\right)\in ℝ$
170 difss ${⊢}\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)$
171 ovolsscl ${⊢}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\subseteq ℝ\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\in ℝ$
172 170 16 171 mp3an12 ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\in ℝ$
173 172 adantl ${⊢}\left(\left(\left({w}\subseteq ℝ\wedge {vol}^{*}\left({w}\right)\in ℝ\right)\wedge {w}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\in ℝ$
174 ssrin ${⊢}{w}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\to {w}\cap {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}$
175 64 16 sstri ${⊢}\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\subseteq ℝ$
176 ovolss ${⊢}\left({w}\cap {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\subseteq ℝ\right)\to {vol}^{*}\left({w}\cap {A}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\right)$
177 174 175 176 sylancl ${⊢}{w}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\to {vol}^{*}\left({w}\cap {A}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\right)$
178 177 ad2antlr ${⊢}\left(\left(\left({w}\subseteq ℝ\wedge {vol}^{*}\left({w}\right)\in ℝ\right)\wedge {w}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to {vol}^{*}\left({w}\cap {A}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\right)$
179 ssdif ${⊢}{w}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\to {w}\setminus {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}$
180 170 16 sstri ${⊢}\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\subseteq ℝ$
181 ovolss ${⊢}\left({w}\setminus {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\subseteq ℝ\right)\to {vol}^{*}\left({w}\setminus {A}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)$
182 179 180 181 sylancl ${⊢}{w}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\to {vol}^{*}\left({w}\setminus {A}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)$
183 182 ad2antlr ${⊢}\left(\left(\left({w}\subseteq ℝ\wedge {vol}^{*}\left({w}\right)\in ℝ\right)\wedge {w}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to {vol}^{*}\left({w}\setminus {A}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)$
184 165 166 169 173 178 183 le2addd ${⊢}\left(\left(\left({w}\subseteq ℝ\wedge {vol}^{*}\left({w}\right)\in ℝ\right)\wedge {w}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to {vol}^{*}\left({w}\cap {A}\right)+{vol}^{*}\left({w}\setminus {A}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\right)+{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)$
185 dfin4 ${⊢}\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}=\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)$
186 185 fveq2i ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\right)={vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\right)$
187 186 oveq1i ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\right)+{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)={vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\right)+{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)$
188 184 187 breqtrdi ${⊢}\left(\left(\left({w}\subseteq ℝ\wedge {vol}^{*}\left({w}\right)\in ℝ\right)\wedge {w}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to {vol}^{*}\left({w}\cap {A}\right)+{vol}^{*}\left({w}\setminus {A}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\right)+{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)$
189 188 adantlll ${⊢}\left(\left(\left(\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge {vol}^{*}\left({A}\right)=sup\left(\left\{{y}|\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {y}=vol\left({b}\right)\right)\right\},ℝ,<\right)\right)\wedge \left({w}\subseteq ℝ\wedge {vol}^{*}\left({w}\right)\in ℝ\right)\right)\wedge {w}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to {vol}^{*}\left({w}\cap {A}\right)+{vol}^{*}\left({w}\setminus {A}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\right)+{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)$
190 simpll ${⊢}\left(\left(\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge {vol}^{*}\left({A}\right)=sup\left(\left\{{y}|\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {y}=vol\left({b}\right)\right)\right\},ℝ,<\right)\right)\wedge \left({w}\subseteq ℝ\wedge {vol}^{*}\left({w}\right)\in ℝ\right)\right)\wedge {w}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\to \left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge {vol}^{*}\left({A}\right)=sup\left(\left\{{y}|\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {y}=vol\left({b}\right)\right)\right\},ℝ,<\right)\right)$
191 185 sseq2i ${⊢}{a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}↔{a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)$
192 191 anbi1i ${⊢}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)↔\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\wedge {z}=vol\left({a}\right)\right)$
193 192 rexbii ${⊢}\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)↔\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\wedge {z}=vol\left({a}\right)\right)$
194 193 abbii ${⊢}\left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}=\left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\wedge {z}=vol\left({a}\right)\right)\right\}$
195 194 supeq1i ${⊢}sup\left(\left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\},ℝ,<\right)=sup\left(\left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\wedge {z}=vol\left({a}\right)\right)\right\},ℝ,<\right)$
196 16 jctl ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\to \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\subseteq ℝ\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)$
197 196 adantl ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge {vol}^{*}\left({A}\right)=sup\left(\left\{{y}|\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {y}=vol\left({b}\right)\right)\right\},ℝ,<\right)\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\subseteq ℝ\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)$
198 172 180 jctil ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\to \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\subseteq ℝ\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\in ℝ\right)$
199 198 adantl ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge {vol}^{*}\left({A}\right)=sup\left(\left\{{y}|\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {y}=vol\left({b}\right)\right)\right\},ℝ,<\right)\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\subseteq ℝ\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\in ℝ\right)$
200 ltso ${⊢}<\mathrm{Or}ℝ$
201 200 a1i ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\to <\mathrm{Or}ℝ$
202 id ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ$
203 vex ${⊢}{x}\in \mathrm{V}$
204 eqeq1 ${⊢}{z}={x}\to \left({z}=vol\left({c}\right)↔{x}=vol\left({c}\right)\right)$
205 204 anbi2d ${⊢}{z}={x}\to \left(\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {z}=vol\left({c}\right)\right)↔\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {x}=vol\left({c}\right)\right)\right)$
206 205 rexbidv ${⊢}{z}={x}\to \left(\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {z}=vol\left({c}\right)\right)↔\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {x}=vol\left({c}\right)\right)\right)$
207 203 206 elab ${⊢}{x}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {z}=vol\left({c}\right)\right)\right\}↔\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {x}=vol\left({c}\right)\right)$
208 16 137 mpan2 ${⊢}{c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\to {vol}^{*}\left({c}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)$
209 208 ad2antrl ${⊢}\left({c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge \left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {x}=vol\left({c}\right)\right)\right)\to {vol}^{*}\left({c}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)$
210 48 cldss ${⊢}{c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\to {c}\subseteq ℝ$
211 ovolcl ${⊢}{c}\subseteq ℝ\to {vol}^{*}\left({c}\right)\in {ℝ}^{*}$
212 210 211 syl ${⊢}{c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\to {vol}^{*}\left({c}\right)\in {ℝ}^{*}$
213 xrlenlt ${⊢}\left({vol}^{*}\left({c}\right)\in {ℝ}^{*}\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in {ℝ}^{*}\right)\to \left({vol}^{*}\left({c}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)↔¬{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)<{vol}^{*}\left({c}\right)\right)$
214 212 34 213 sylancl ${⊢}{c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\to \left({vol}^{*}\left({c}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)↔¬{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)<{vol}^{*}\left({c}\right)\right)$
215 214 adantr ${⊢}\left({c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge \left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {x}=vol\left({c}\right)\right)\right)\to \left({vol}^{*}\left({c}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)↔¬{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)<{vol}^{*}\left({c}\right)\right)$
216 id ${⊢}{x}=vol\left({c}\right)\to {x}=vol\left({c}\right)$
217 216 119 sylan9eqr ${⊢}\left({c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge {x}=vol\left({c}\right)\right)\to {x}={vol}^{*}\left({c}\right)$
218 breq2 ${⊢}{x}={vol}^{*}\left({c}\right)\to \left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)<{x}↔{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)<{vol}^{*}\left({c}\right)\right)$
219 218 notbid ${⊢}{x}={vol}^{*}\left({c}\right)\to \left(¬{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)<{x}↔¬{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)<{vol}^{*}\left({c}\right)\right)$
220 217 219 syl ${⊢}\left({c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge {x}=vol\left({c}\right)\right)\to \left(¬{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)<{x}↔¬{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)<{vol}^{*}\left({c}\right)\right)$
221 220 adantrl ${⊢}\left({c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge \left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {x}=vol\left({c}\right)\right)\right)\to \left(¬{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)<{x}↔¬{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)<{vol}^{*}\left({c}\right)\right)$
222 215 221 bitr4d ${⊢}\left({c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge \left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {x}=vol\left({c}\right)\right)\right)\to \left({vol}^{*}\left({c}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)↔¬{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)<{x}\right)$
223 209 222 mpbid ${⊢}\left({c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge \left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {x}=vol\left({c}\right)\right)\right)\to ¬{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)<{x}$
224 223 rexlimiva ${⊢}\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {x}=vol\left({c}\right)\right)\to ¬{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)<{x}$
225 207 224 sylbi ${⊢}{x}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {z}=vol\left({c}\right)\right)\right\}\to ¬{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)<{x}$
226 225 adantl ${⊢}\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge {x}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {z}=vol\left({c}\right)\right)\right\}\right)\to ¬{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)<{x}$
227 retopbas ${⊢}\mathrm{ran}\left(.\right)\in \mathrm{TopBases}$
228 bastg ${⊢}\mathrm{ran}\left(.\right)\in \mathrm{TopBases}\to \mathrm{ran}\left(.\right)\subseteq \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
229 227 228 ax-mp ${⊢}\mathrm{ran}\left(.\right)\subseteq \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
230 13 229 sstri ${⊢}\mathrm{ran}\left(\left(.\right)\circ {f}\right)\subseteq \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
231 uniopn ${⊢}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}\wedge \mathrm{ran}\left(\left(.\right)\circ {f}\right)\subseteq \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\to \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
232 89 230 231 mp2an ${⊢}\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
233 mblfinlem2 ${⊢}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\wedge {x}\in ℝ\wedge {x}<{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\right)\to \exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {x}<{vol}^{*}\left({c}\right)\right)$
234 232 233 mp3an1 ${⊢}\left({x}\in ℝ\wedge {x}<{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\right)\to \exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {x}<{vol}^{*}\left({c}\right)\right)$
235 119 eqcomd ${⊢}{c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\to {vol}^{*}\left({c}\right)=vol\left({c}\right)$
236 235 anim1i ${⊢}\left({c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge {x}<{vol}^{*}\left({c}\right)\right)\to \left({vol}^{*}\left({c}\right)=vol\left({c}\right)\wedge {x}<{vol}^{*}\left({c}\right)\right)$
237 236 ex ${⊢}{c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\to \left({x}<{vol}^{*}\left({c}\right)\to \left({vol}^{*}\left({c}\right)=vol\left({c}\right)\wedge {x}<{vol}^{*}\left({c}\right)\right)\right)$
238 237 anim2d ${⊢}{c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\to \left(\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {x}<{vol}^{*}\left({c}\right)\right)\to \left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge \left({vol}^{*}\left({c}\right)=vol\left({c}\right)\wedge {x}<{vol}^{*}\left({c}\right)\right)\right)\right)$
239 fvex ${⊢}{vol}^{*}\left({c}\right)\in \mathrm{V}$
240 eqeq1 ${⊢}{y}={vol}^{*}\left({c}\right)\to \left({y}=vol\left({c}\right)↔{vol}^{*}\left({c}\right)=vol\left({c}\right)\right)$
241 240 anbi2d ${⊢}{y}={vol}^{*}\left({c}\right)\to \left(\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=vol\left({c}\right)\right)↔\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {vol}^{*}\left({c}\right)=vol\left({c}\right)\right)\right)$
242 breq2 ${⊢}{y}={vol}^{*}\left({c}\right)\to \left({x}<{y}↔{x}<{vol}^{*}\left({c}\right)\right)$
243 241 242 anbi12d ${⊢}{y}={vol}^{*}\left({c}\right)\to \left(\left(\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=vol\left({c}\right)\right)\wedge {x}<{y}\right)↔\left(\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {vol}^{*}\left({c}\right)=vol\left({c}\right)\right)\wedge {x}<{vol}^{*}\left({c}\right)\right)\right)$
244 239 243 spcev ${⊢}\left(\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {vol}^{*}\left({c}\right)=vol\left({c}\right)\right)\wedge {x}<{vol}^{*}\left({c}\right)\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=vol\left({c}\right)\right)\wedge {x}<{y}\right)$
245 244 anasss ${⊢}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge \left({vol}^{*}\left({c}\right)=vol\left({c}\right)\wedge {x}<{vol}^{*}\left({c}\right)\right)\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=vol\left({c}\right)\right)\wedge {x}<{y}\right)$
246 238 245 syl6 ${⊢}{c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\to \left(\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {x}<{vol}^{*}\left({c}\right)\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=vol\left({c}\right)\right)\wedge {x}<{y}\right)\right)$
247 246 reximia ${⊢}\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {x}<{vol}^{*}\left({c}\right)\right)\to \exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=vol\left({c}\right)\right)\wedge {x}<{y}\right)$
248 234 247 syl ${⊢}\left({x}\in ℝ\wedge {x}<{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\right)\to \exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=vol\left({c}\right)\right)\wedge {x}<{y}\right)$
249 r19.41v ${⊢}\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left(\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=vol\left({c}\right)\right)\wedge {x}<{y}\right)↔\left(\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=vol\left({c}\right)\right)\wedge {x}<{y}\right)$
250 249 exbii ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left(\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=vol\left({c}\right)\right)\wedge {x}<{y}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left(\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=vol\left({c}\right)\right)\wedge {x}<{y}\right)$
251 rexcom4 ${⊢}\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=vol\left({c}\right)\right)\wedge {x}<{y}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left(\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=vol\left({c}\right)\right)\wedge {x}<{y}\right)$
252 131 anbi2d ${⊢}{z}={y}\to \left(\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {z}=vol\left({c}\right)\right)↔\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=vol\left({c}\right)\right)\right)$
253 252 rexbidv ${⊢}{z}={y}\to \left(\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {z}=vol\left({c}\right)\right)↔\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=vol\left({c}\right)\right)\right)$
254 253 rexab ${⊢}\exists {y}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{x}<{y}↔\exists {y}\phantom{\rule{.4em}{0ex}}\left(\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=vol\left({c}\right)\right)\wedge {x}<{y}\right)$
255 250 251 254 3bitr4i ${⊢}\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=vol\left({c}\right)\right)\wedge {x}<{y}\right)↔\exists {y}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{x}<{y}$
256 248 255 sylib ${⊢}\left({x}\in ℝ\wedge {x}<{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\right)\to \exists {y}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{x}<{y}$
257 256 adantl ${⊢}\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \left({x}\in ℝ\wedge {x}<{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\right)\right)\to \exists {y}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{x}<{y}$
258 201 202 226 257 eqsupd ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\to sup\left(\left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {z}=vol\left({c}\right)\right)\right\},ℝ,<\right)={vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)$
259 258 eqcomd ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)=sup\left(\left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {z}=vol\left({c}\right)\right)\right\},ℝ,<\right)$
260 259 adantl ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge {vol}^{*}\left({A}\right)=sup\left(\left\{{y}|\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {y}=vol\left({b}\right)\right)\right\},ℝ,<\right)\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)=sup\left(\left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {z}=vol\left({c}\right)\right)\right\},ℝ,<\right)$
261 sseq1 ${⊢}{c}={a}\to \left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)↔{a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)$
262 fveq2 ${⊢}{c}={a}\to vol\left({c}\right)=vol\left({a}\right)$
263 262 eqeq2d ${⊢}{c}={a}\to \left({z}=vol\left({c}\right)↔{z}=vol\left({a}\right)\right)$
264 261 263 anbi12d ${⊢}{c}={a}\to \left(\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {z}=vol\left({c}\right)\right)↔\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {z}=vol\left({a}\right)\right)\right)$
265 264 cbvrexvw ${⊢}\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {z}=vol\left({c}\right)\right)↔\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {z}=vol\left({a}\right)\right)$
266 265 abbii ${⊢}\left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {z}=vol\left({c}\right)\right)\right\}=\left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {z}=vol\left({a}\right)\right)\right\}$
267 266 supeq1i ${⊢}sup\left(\left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {z}=vol\left({c}\right)\right)\right\},ℝ,<\right)=sup\left(\left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {z}=vol\left({a}\right)\right)\right\},ℝ,<\right)$
268 260 267 syl6eq ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge {vol}^{*}\left({A}\right)=sup\left(\left\{{y}|\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {y}=vol\left({b}\right)\right)\right\},ℝ,<\right)\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)=sup\left(\left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {z}=vol\left({a}\right)\right)\right\},ℝ,<\right)$
269 sseq1 ${⊢}{c}={a}\to \left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}↔{a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)$
270 269 263 anbi12d ${⊢}{c}={a}\to \left(\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)↔\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({a}\right)\right)\right)$
271 270 cbvrexvw ${⊢}\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)↔\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({a}\right)\right)$
272 271 abbii ${⊢}\left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}=\left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({a}\right)\right)\right\}$
273 272 supeq1i ${⊢}sup\left(\left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\},ℝ,<\right)=sup\left(\left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({a}\right)\right)\right\},ℝ,<\right)$
274 simpll ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge {vol}^{*}\left({A}\right)=sup\left(\left\{{y}|\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {y}=vol\left({b}\right)\right)\right\},ℝ,<\right)\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to \left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)$
275 eqeq1 ${⊢}{y}={z}\to \left({y}=vol\left({b}\right)↔{z}=vol\left({b}\right)\right)$
276 275 anbi2d ${⊢}{y}={z}\to \left(\left({b}\subseteq {A}\wedge {y}=vol\left({b}\right)\right)↔\left({b}\subseteq {A}\wedge {z}=vol\left({b}\right)\right)\right)$
277 276 rexbidv ${⊢}{y}={z}\to \left(\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {y}=vol\left({b}\right)\right)↔\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {z}=vol\left({b}\right)\right)\right)$
278 sseq1 ${⊢}{b}={c}\to \left({b}\subseteq {A}↔{c}\subseteq {A}\right)$
279 fveq2 ${⊢}{b}={c}\to vol\left({b}\right)=vol\left({c}\right)$
280 279 eqeq2d ${⊢}{b}={c}\to \left({z}=vol\left({b}\right)↔{z}=vol\left({c}\right)\right)$
281 278 280 anbi12d ${⊢}{b}={c}\to \left(\left({b}\subseteq {A}\wedge {z}=vol\left({b}\right)\right)↔\left({c}\subseteq {A}\wedge {z}=vol\left({c}\right)\right)\right)$
282 281 cbvrexvw ${⊢}\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {z}=vol\left({b}\right)\right)↔\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq {A}\wedge {z}=vol\left({c}\right)\right)$
283 277 282 syl6bb ${⊢}{y}={z}\to \left(\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {y}=vol\left({b}\right)\right)↔\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq {A}\wedge {z}=vol\left({c}\right)\right)\right)$
284 283 cbvabv ${⊢}\left\{{y}|\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {y}=vol\left({b}\right)\right)\right\}=\left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq {A}\wedge {z}=vol\left({c}\right)\right)\right\}$
285 284 supeq1i ${⊢}sup\left(\left\{{y}|\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {y}=vol\left({b}\right)\right)\right\},ℝ,<\right)=sup\left(\left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq {A}\wedge {z}=vol\left({c}\right)\right)\right\},ℝ,<\right)$
286 285 eqeq2i ${⊢}{vol}^{*}\left({A}\right)=sup\left(\left\{{y}|\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {y}=vol\left({b}\right)\right)\right\},ℝ,<\right)↔{vol}^{*}\left({A}\right)=sup\left(\left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq {A}\wedge {z}=vol\left({c}\right)\right)\right\},ℝ,<\right)$
287 286 biimpi ${⊢}{vol}^{*}\left({A}\right)=sup\left(\left\{{y}|\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {y}=vol\left({b}\right)\right)\right\},ℝ,<\right)\to {vol}^{*}\left({A}\right)=sup\left(\left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq {A}\wedge {z}=vol\left({c}\right)\right)\right\},ℝ,<\right)$
288 287 ad2antlr ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge {vol}^{*}\left({A}\right)=sup\left(\left\{{y}|\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {y}=vol\left({b}\right)\right)\right\},ℝ,<\right)\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to {vol}^{*}\left({A}\right)=sup\left(\left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq {A}\wedge {z}=vol\left({c}\right)\right)\right\},ℝ,<\right)$
289 mblfinlem3 ${⊢}\left(\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\subseteq ℝ\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\wedge \left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge \left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)=sup\left(\left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {z}=vol\left({c}\right)\right)\right\},ℝ,<\right)\wedge {vol}^{*}\left({A}\right)=sup\left(\left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq {A}\wedge {z}=vol\left({c}\right)\right)\right\},ℝ,<\right)\right)\right)\to sup\left(\left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\},ℝ,<\right)={vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)$
290 197 274 260 288 289 syl112anc ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge {vol}^{*}\left({A}\right)=sup\left(\left\{{y}|\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {y}=vol\left({b}\right)\right)\right\},ℝ,<\right)\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to sup\left(\left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\},ℝ,<\right)={vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)$
291 273 290 syl5reqr ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge {vol}^{*}\left({A}\right)=sup\left(\left\{{y}|\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {y}=vol\left({b}\right)\right)\right\},ℝ,<\right)\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)=sup\left(\left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({a}\right)\right)\right\},ℝ,<\right)$
292 mblfinlem3 ${⊢}\left(\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\subseteq ℝ\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\wedge \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\subseteq ℝ\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\in ℝ\right)\wedge \left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)=sup\left(\left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {z}=vol\left({a}\right)\right)\right\},ℝ,<\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)=sup\left(\left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({a}\right)\right)\right\},ℝ,<\right)\right)\right)\to sup\left(\left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\wedge {z}=vol\left({a}\right)\right)\right\},ℝ,<\right)={vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\right)$
293 197 199 268 291 292 syl112anc ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge {vol}^{*}\left({A}\right)=sup\left(\left\{{y}|\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {y}=vol\left({b}\right)\right)\right\},ℝ,<\right)\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to sup\left(\left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\wedge {z}=vol\left({a}\right)\right)\right\},ℝ,<\right)={vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\right)$
294 195 293 syl5eq ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge {vol}^{*}\left({A}\right)=sup\left(\left\{{y}|\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {y}=vol\left({b}\right)\right)\right\},ℝ,<\right)\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to sup\left(\left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\},ℝ,<\right)={vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\right)$
295 294 290 oveq12d ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge {vol}^{*}\left({A}\right)=sup\left(\left\{{y}|\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {y}=vol\left({b}\right)\right)\right\},ℝ,<\right)\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to sup\left(\left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\},ℝ,<\right)+sup\left(\left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\},ℝ,<\right)={vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\right)+{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)$
296 190 295 sylan ${⊢}\left(\left(\left(\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge {vol}^{*}\left({A}\right)=sup\left(\left\{{y}|\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {y}=vol\left({b}\right)\right)\right\},ℝ,<\right)\right)\wedge \left({w}\subseteq ℝ\wedge {vol}^{*}\left({w}\right)\in ℝ\right)\right)\wedge {w}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to sup\left(\left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\},ℝ,<\right)+sup\left(\left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\},ℝ,<\right)={vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\right)+{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)$
297 189 296 breqtrrd ${⊢}\left(\left(\left(\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge {vol}^{*}\left({A}\right)=sup\left(\left\{{y}|\exists {b}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({b}\subseteq {A}\wedge {y}=vol\left({b}\right)\right)\right\},ℝ,<\right)\right)\wedge \left({w}\subseteq ℝ\wedge {vol}^{*}\left({w}\right)\in ℝ\right)\right)\wedge {w}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to {vol}^{*}\left({w}\cap {A}\right)+{vol}^{*}\left({w}\setminus {A}\right)\le sup\left(\left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\},ℝ,<\right)+sup\left(\left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\},ℝ,<\right)$
298 ne0i ${⊢}0\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\to \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\ne \varnothing$
299 110 298 mp1i ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\to \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\ne \varnothing$
300 ne0i ${⊢}0\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\to \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\ne \varnothing$
301 157 300 mp1i ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\to \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\ne \varnothing$
302 eqid ${⊢}\left\{{t}|\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{t}={u}+{v}\right\}=\left\{{t}|\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{t}={u}+{v}\right\}$
303 74 299 88 130 301 144 302 supadd ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\to sup\left(\left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\},ℝ,<\right)+sup\left(\left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\},ℝ,<\right)=sup\left(\left\{{t}|\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{t}={u}+{v}\right\},ℝ,<\right)$
304 reeanv ${⊢}\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left(\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {u}=vol\left({a}\right)\right)\wedge \left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {v}=vol\left({c}\right)\right)\right)↔\left(\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {u}=vol\left({a}\right)\right)\wedge \exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {v}=vol\left({c}\right)\right)\right)$
305 vex ${⊢}{u}\in \mathrm{V}$
306 eqeq1 ${⊢}{z}={u}\to \left({z}=vol\left({a}\right)↔{u}=vol\left({a}\right)\right)$
307 306 anbi2d ${⊢}{z}={u}\to \left(\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)↔\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {u}=vol\left({a}\right)\right)\right)$
308 307 rexbidv ${⊢}{z}={u}\to \left(\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)↔\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {u}=vol\left({a}\right)\right)\right)$
309 305 308 elab ${⊢}{u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}↔\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {u}=vol\left({a}\right)\right)$
310 vex ${⊢}{v}\in \mathrm{V}$
311 eqeq1 ${⊢}{z}={v}\to \left({z}=vol\left({c}\right)↔{v}=vol\left({c}\right)\right)$
312 311 anbi2d ${⊢}{z}={v}\to \left(\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)↔\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {v}=vol\left({c}\right)\right)\right)$
313 312 rexbidv ${⊢}{z}={v}\to \left(\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)↔\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {v}=vol\left({c}\right)\right)\right)$
314 310 313 elab ${⊢}{v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}↔\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {v}=vol\left({c}\right)\right)$
315 309 314 anbi12i ${⊢}\left({u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\wedge {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\right)↔\left(\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {u}=vol\left({a}\right)\right)\wedge \exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {v}=vol\left({c}\right)\right)\right)$
316 304 315 bitr4i ${⊢}\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left(\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {u}=vol\left({a}\right)\right)\wedge \left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {v}=vol\left({c}\right)\right)\right)↔\left({u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\wedge {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\right)$
317 an4 ${⊢}\left(\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\wedge \left({u}=vol\left({a}\right)\wedge {v}=vol\left({c}\right)\right)\right)↔\left(\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {u}=vol\left({a}\right)\right)\wedge \left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {v}=vol\left({c}\right)\right)\right)$
318 oveq12 ${⊢}\left({u}=vol\left({a}\right)\wedge {v}=vol\left({c}\right)\right)\to {u}+{v}=vol\left({a}\right)+vol\left({c}\right)$
319 59 adantr ${⊢}\left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\right)\to {a}\in \mathrm{dom}vol$
320 319 ad2antlr ${⊢}\left(\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\right)\right)\wedge \left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\right)\to {a}\in \mathrm{dom}vol$
321 117 adantl ${⊢}\left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\right)\to {c}\in \mathrm{dom}vol$
322 321 ad2antlr ${⊢}\left(\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\right)\right)\wedge \left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\right)\to {c}\in \mathrm{dom}vol$
323 ss2in ${⊢}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\to {a}\cap {c}\subseteq \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\right)\cap \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)$
324 185 ineq1i ${⊢}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\right)\cap \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)=\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\right)\cap \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)$
325 incom ${⊢}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\right)\cap \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)=\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\cap \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\right)$
326 disjdif ${⊢}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\cap \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\right)=\varnothing$
327 324 325 326 3eqtri ${⊢}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\right)\cap \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)=\varnothing$
328 323 327 sseqtrdi ${⊢}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\to {a}\cap {c}\subseteq \varnothing$
329 ss0 ${⊢}{a}\cap {c}\subseteq \varnothing \to {a}\cap {c}=\varnothing$
330 328 329 syl ${⊢}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\to {a}\cap {c}=\varnothing$
331 330 adantl ${⊢}\left(\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\right)\right)\wedge \left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\right)\to {a}\cap {c}=\varnothing$
332 61 adantr ${⊢}\left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\right)\to vol\left({a}\right)={vol}^{*}\left({a}\right)$
333 332 ad2antlr ${⊢}\left(\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\right)\right)\wedge \left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\right)\to vol\left({a}\right)={vol}^{*}\left({a}\right)$
334 66 16 jctir ${⊢}{a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\to \left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\subseteq ℝ\right)$
335 68 3expa ${⊢}\left(\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\subseteq ℝ\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to {vol}^{*}\left({a}\right)\in ℝ$
336 334 335 sylan ${⊢}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to {vol}^{*}\left({a}\right)\in ℝ$
337 336 ancoms ${⊢}\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge {a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\right)\to {vol}^{*}\left({a}\right)\in ℝ$
338 337 ad2ant2r ${⊢}\left(\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\right)\right)\wedge \left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\right)\to {vol}^{*}\left({a}\right)\in ℝ$
339 333 338 eqeltrd ${⊢}\left(\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\right)\right)\wedge \left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\right)\to vol\left({a}\right)\in ℝ$
340 119 adantl ${⊢}\left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\right)\to vol\left({c}\right)={vol}^{*}\left({c}\right)$
341 340 ad2antlr ${⊢}\left(\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\right)\right)\wedge \left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\right)\to vol\left({c}\right)={vol}^{*}\left({c}\right)$
342 122 16 jctir ${⊢}{c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\to \left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\subseteq ℝ\right)$
343 124 3expa ${⊢}\left(\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\subseteq ℝ\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to {vol}^{*}\left({c}\right)\in ℝ$
344 342 343 sylan ${⊢}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to {vol}^{*}\left({c}\right)\in ℝ$
345 344 ancoms ${⊢}\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\to {vol}^{*}\left({c}\right)\in ℝ$
346 345 ad2ant2rl ${⊢}\left(\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\right)\right)\wedge \left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\right)\to {vol}^{*}\left({c}\right)\in ℝ$
347 341 346 eqeltrd ${⊢}\left(\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\right)\right)\wedge \left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\right)\to vol\left({c}\right)\in ℝ$
348 volun ${⊢}\left(\left({a}\in \mathrm{dom}vol\wedge {c}\in \mathrm{dom}vol\wedge {a}\cap {c}=\varnothing \right)\wedge \left(vol\left({a}\right)\in ℝ\wedge vol\left({c}\right)\in ℝ\right)\right)\to vol\left({a}\cup {c}\right)=vol\left({a}\right)+vol\left({c}\right)$
349 320 322 331 339 347 348 syl32anc ${⊢}\left(\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\right)\right)\wedge \left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\right)\to vol\left({a}\cup {c}\right)=vol\left({a}\right)+vol\left({c}\right)$
350 unmbl ${⊢}\left({a}\in \mathrm{dom}vol\wedge {c}\in \mathrm{dom}vol\right)\to {a}\cup {c}\in \mathrm{dom}vol$
351 59 117 350 syl2an ${⊢}\left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\right)\to {a}\cup {c}\in \mathrm{dom}vol$
352 mblvol ${⊢}{a}\cup {c}\in \mathrm{dom}vol\to vol\left({a}\cup {c}\right)={vol}^{*}\left({a}\cup {c}\right)$
353 351 352 syl ${⊢}\left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\right)\to vol\left({a}\cup {c}\right)={vol}^{*}\left({a}\cup {c}\right)$
354 353 ad2antlr ${⊢}\left(\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\right)\right)\wedge \left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\right)\to vol\left({a}\cup {c}\right)={vol}^{*}\left({a}\cup {c}\right)$
355 349 354 eqtr3d ${⊢}\left(\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\right)\right)\wedge \left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\right)\to vol\left({a}\right)+vol\left({c}\right)={vol}^{*}\left({a}\cup {c}\right)$
356 318 355 sylan9eqr ${⊢}\left(\left(\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\right)\right)\wedge \left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\right)\wedge \left({u}=vol\left({a}\right)\wedge {v}=vol\left({c}\right)\right)\right)\to {u}+{v}={vol}^{*}\left({a}\cup {c}\right)$
357 eqtr ${⊢}\left({y}={u}+{v}\wedge {u}+{v}={vol}^{*}\left({a}\cup {c}\right)\right)\to {y}={vol}^{*}\left({a}\cup {c}\right)$
358 357 ancoms ${⊢}\left({u}+{v}={vol}^{*}\left({a}\cup {c}\right)\wedge {y}={u}+{v}\right)\to {y}={vol}^{*}\left({a}\cup {c}\right)$
359 356 358 sylan ${⊢}\left(\left(\left(\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\right)\right)\wedge \left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\right)\wedge \left({u}=vol\left({a}\right)\wedge {v}=vol\left({c}\right)\right)\right)\wedge {y}={u}+{v}\right)\to {y}={vol}^{*}\left({a}\cup {c}\right)$
360 66 122 anim12i ${⊢}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\to \left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)$
361 unss ${⊢}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)↔{a}\cup {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)$
362 360 361 sylib ${⊢}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\to {a}\cup {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)$
363 ovolss ${⊢}\left({a}\cup {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\subseteq ℝ\right)\to {vol}^{*}\left({a}\cup {c}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)$
364 362 16 363 sylancl ${⊢}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\to {vol}^{*}\left({a}\cup {c}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)$
365 364 ad3antlr ${⊢}\left(\left(\left(\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\right)\right)\wedge \left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\right)\wedge \left({u}=vol\left({a}\right)\wedge {v}=vol\left({c}\right)\right)\right)\wedge {y}={u}+{v}\right)\to {vol}^{*}\left({a}\cup {c}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)$
366 359 365 eqbrtrd ${⊢}\left(\left(\left(\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\right)\right)\wedge \left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\right)\wedge \left({u}=vol\left({a}\right)\wedge {v}=vol\left({c}\right)\right)\right)\wedge {y}={u}+{v}\right)\to {y}\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)$
367 366 ex ${⊢}\left(\left(\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\right)\right)\wedge \left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\right)\wedge \left({u}=vol\left({a}\right)\wedge {v}=vol\left({c}\right)\right)\right)\to \left({y}={u}+{v}\to {y}\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\right)$
368 367 expl ${⊢}\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\right)\right)\to \left(\left(\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\right)\wedge \left({u}=vol\left({a}\right)\wedge {v}=vol\left({c}\right)\right)\right)\to \left({y}={u}+{v}\to {y}\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\right)\right)$
369 317 368 syl5bir ${⊢}\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \left({a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\right)\right)\to \left(\left(\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {u}=vol\left({a}\right)\right)\wedge \left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {v}=vol\left({c}\right)\right)\right)\to \left({y}={u}+{v}\to {y}\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\right)\right)$
370 369 rexlimdvva ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\to \left(\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left(\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {u}=vol\left({a}\right)\right)\wedge \left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {v}=vol\left({c}\right)\right)\right)\to \left({y}={u}+{v}\to {y}\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\right)\right)$
371 316 370 syl5bir ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\to \left(\left({u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\wedge {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\right)\to \left({y}={u}+{v}\to {y}\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\right)\right)$
372 371 rexlimdvv ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\to \left(\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{y}={u}+{v}\to {y}\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\right)$
373 372 alrimiv ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\to \forall {y}\phantom{\rule{.4em}{0ex}}\left(\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{y}={u}+{v}\to {y}\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\right)$
374 eqeq1 ${⊢}{t}={y}\to \left({t}={u}+{v}↔{y}={u}+{v}\right)$
375 374 2rexbidv ${⊢}{t}={y}\to \left(\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{t}={u}+{v}↔\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{y}={u}+{v}\right)$
376 375 ralab ${⊢}\forall {y}\in \left\{{t}|\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{t}={u}+{v}\right\}\phantom{\rule{.4em}{0ex}}{y}\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left(\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{y}={u}+{v}\to {y}\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\right)$
377 373 376 sylibr ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\to \forall {y}\in \left\{{t}|\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{t}={u}+{v}\right\}\phantom{\rule{.4em}{0ex}}{y}\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)$
378 simpr ${⊢}\left(\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \left({u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\wedge {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\right)\right)\wedge {t}={u}+{v}\right)\to {t}={u}+{v}$
379 74 sselda ${⊢}\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\right)\to {u}\in ℝ$
380 130 sselda ${⊢}\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\right)\to {v}\in ℝ$
381 readdcl ${⊢}\left({u}\in ℝ\wedge {v}\in ℝ\right)\to {u}+{v}\in ℝ$
382 379 380 381 syl2an ${⊢}\left(\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\right)\wedge \left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\right)\right)\to {u}+{v}\in ℝ$
383 382 anandis ${⊢}\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \left({u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\wedge {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\right)\right)\to {u}+{v}\in ℝ$
384 383 adantr ${⊢}\left(\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \left({u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\wedge {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\right)\right)\wedge {t}={u}+{v}\right)\to {u}+{v}\in ℝ$
385 378 384 eqeltrd ${⊢}\left(\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \left({u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\wedge {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\right)\right)\wedge {t}={u}+{v}\right)\to {t}\in ℝ$
386 385 ex ${⊢}\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \left({u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\wedge {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\right)\right)\to \left({t}={u}+{v}\to {t}\in ℝ\right)$
387 386 rexlimdvva ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\to \left(\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{t}={u}+{v}\to {t}\in ℝ\right)$
388 387 abssdv ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\to \left\{{t}|\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{t}={u}+{v}\right\}\subseteq ℝ$
389 00id ${⊢}0+0=0$
390 389 eqcomi ${⊢}0=0+0$
391 rspceov ${⊢}\left(0\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\wedge 0\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\wedge 0=0+0\right)\to \exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}0={u}+{v}$
392 110 157 390 391 mp3an ${⊢}\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}0={u}+{v}$
393 eqeq1 ${⊢}{t}=0\to \left({t}={u}+{v}↔0={u}+{v}\right)$
394 393 2rexbidv ${⊢}{t}=0\to \left(\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{t}={u}+{v}↔\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}0={u}+{v}\right)$
395 105 394 spcev ${⊢}\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}0={u}+{v}\to \exists {t}\phantom{\rule{.4em}{0ex}}\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{t}={u}+{v}$
396 392 395 ax-mp ${⊢}\exists {t}\phantom{\rule{.4em}{0ex}}\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{t}={u}+{v}$
397 abn0 ${⊢}\left\{{t}|\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{t}={u}+{v}\right\}\ne \varnothing ↔\exists {t}\phantom{\rule{.4em}{0ex}}\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{t}={u}+{v}$
398 396 397 mpbir ${⊢}\left\{{t}|\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{t}={u}+{v}\right\}\ne \varnothing$
399 398 a1i ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\to \left\{{t}|\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{t}={u}+{v}\right\}\ne \varnothing$
400 brralrspcev ${⊢}\left({vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\wedge \forall {y}\in \left\{{t}|\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{t}={u}+{v}\right\}\phantom{\rule{.4em}{0ex}}{y}\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left\{{t}|\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{t}={u}+{v}\right\}\phantom{\rule{.4em}{0ex}}{y}\le {x}$
401 377 400 mpdan ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left\{{t}|\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{t}={u}+{v}\right\}\phantom{\rule{.4em}{0ex}}{y}\le {x}$
402 388 399 401 3jca ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\to \left(\left\{{t}|\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{t}={u}+{v}\right\}\subseteq ℝ\wedge \left\{{t}|\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{t}={u}+{v}\right\}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left\{{t}|\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{t}={u}+{v}\right\}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)$
403 suprleub ${⊢}\left(\left(\left\{{t}|\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{t}={u}+{v}\right\}\subseteq ℝ\wedge \left\{{t}|\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{t}={u}+{v}\right\}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left\{{t}|\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{t}={u}+{v}\right\}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\right)\to \left(sup\left(\left\{{t}|\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{t}={u}+{v}\right\},ℝ,<\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)↔\forall {y}\in \left\{{t}|\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{t}={u}+{v}\right\}\phantom{\rule{.4em}{0ex}}{y}\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\right)$
404 402 403 mpancom ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\to \left(sup\left(\left\{{t}|\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{t}={u}+{v}\right\},ℝ,<\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)↔\forall {y}\in \left\{{t}|\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\cap {A}\wedge {z}=vol\left({a}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left\{{z}|\exists {c}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({c}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\setminus {A}\wedge {z}=vol\left({c}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{t}={u}+{v}\right\}\phantom{\rule{.4em}{0ex}}{y}\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\right)$
405 377 404 mpbird ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\in ℝ\to sup\left(\left\{{t}|\exists {u}\in \left\{{z}|\exists {a}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq \right)\right\}\right\}\right)$