# Metamath Proof Explorer

## Theorem ovolval4lem2

Description: The value of the Lebesgue outer measure for subsets of the reals. Similar to ovolval3 , but here f is may represent unordered interval bounds. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses ovolval4lem2.a ${⊢}{\phi }\to {A}\subseteq ℝ$
ovolval4lem2.m ${⊢}{M}=\left\{{y}\in {ℝ}^{*}|\exists {f}\in \left({{ℝ}^{2}}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {f}\right)\right)\right\}$
ovolval4lem2.g ${⊢}{G}=\left({n}\in ℕ⟼⟨{1}^{st}\left({f}\left({n}\right)\right),if\left({1}^{st}\left({f}\left({n}\right)\right)\le {2}^{nd}\left({f}\left({n}\right)\right),{2}^{nd}\left({f}\left({n}\right)\right),{1}^{st}\left({f}\left({n}\right)\right)\right)⟩\right)$
Assertion ovolval4lem2 ${⊢}{\phi }\to {vol}^{*}\left({A}\right)=sup\left({M},{ℝ}^{*},<\right)$

### Proof

Step Hyp Ref Expression
1 ovolval4lem2.a ${⊢}{\phi }\to {A}\subseteq ℝ$
2 ovolval4lem2.m ${⊢}{M}=\left\{{y}\in {ℝ}^{*}|\exists {f}\in \left({{ℝ}^{2}}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {f}\right)\right)\right\}$
3 ovolval4lem2.g ${⊢}{G}=\left({n}\in ℕ⟼⟨{1}^{st}\left({f}\left({n}\right)\right),if\left({1}^{st}\left({f}\left({n}\right)\right)\le {2}^{nd}\left({f}\left({n}\right)\right),{2}^{nd}\left({f}\left({n}\right)\right),{1}^{st}\left({f}\left({n}\right)\right)\right)⟩\right)$
4 iftrue ${⊢}{1}^{st}\left({f}\left({n}\right)\right)\le {2}^{nd}\left({f}\left({n}\right)\right)\to if\left({1}^{st}\left({f}\left({n}\right)\right)\le {2}^{nd}\left({f}\left({n}\right)\right),{2}^{nd}\left({f}\left({n}\right)\right),{1}^{st}\left({f}\left({n}\right)\right)\right)={2}^{nd}\left({f}\left({n}\right)\right)$
5 4 opeq2d ${⊢}{1}^{st}\left({f}\left({n}\right)\right)\le {2}^{nd}\left({f}\left({n}\right)\right)\to ⟨{1}^{st}\left({f}\left({n}\right)\right),if\left({1}^{st}\left({f}\left({n}\right)\right)\le {2}^{nd}\left({f}\left({n}\right)\right),{2}^{nd}\left({f}\left({n}\right)\right),{1}^{st}\left({f}\left({n}\right)\right)\right)⟩=⟨{1}^{st}\left({f}\left({n}\right)\right),{2}^{nd}\left({f}\left({n}\right)\right)⟩$
6 5 adantl ${⊢}\left(\left({f}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {n}\in ℕ\right)\wedge {1}^{st}\left({f}\left({n}\right)\right)\le {2}^{nd}\left({f}\left({n}\right)\right)\right)\to ⟨{1}^{st}\left({f}\left({n}\right)\right),if\left({1}^{st}\left({f}\left({n}\right)\right)\le {2}^{nd}\left({f}\left({n}\right)\right),{2}^{nd}\left({f}\left({n}\right)\right),{1}^{st}\left({f}\left({n}\right)\right)\right)⟩=⟨{1}^{st}\left({f}\left({n}\right)\right),{2}^{nd}\left({f}\left({n}\right)\right)⟩$
7 df-br ${⊢}{1}^{st}\left({f}\left({n}\right)\right)\le {2}^{nd}\left({f}\left({n}\right)\right)↔⟨{1}^{st}\left({f}\left({n}\right)\right),{2}^{nd}\left({f}\left({n}\right)\right)⟩\in \le$
8 7 biimpi ${⊢}{1}^{st}\left({f}\left({n}\right)\right)\le {2}^{nd}\left({f}\left({n}\right)\right)\to ⟨{1}^{st}\left({f}\left({n}\right)\right),{2}^{nd}\left({f}\left({n}\right)\right)⟩\in \le$
9 8 adantl ${⊢}\left(\left({f}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {n}\in ℕ\right)\wedge {1}^{st}\left({f}\left({n}\right)\right)\le {2}^{nd}\left({f}\left({n}\right)\right)\right)\to ⟨{1}^{st}\left({f}\left({n}\right)\right),{2}^{nd}\left({f}\left({n}\right)\right)⟩\in \le$
10 6 9 eqeltrd ${⊢}\left(\left({f}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {n}\in ℕ\right)\wedge {1}^{st}\left({f}\left({n}\right)\right)\le {2}^{nd}\left({f}\left({n}\right)\right)\right)\to ⟨{1}^{st}\left({f}\left({n}\right)\right),if\left({1}^{st}\left({f}\left({n}\right)\right)\le {2}^{nd}\left({f}\left({n}\right)\right),{2}^{nd}\left({f}\left({n}\right)\right),{1}^{st}\left({f}\left({n}\right)\right)\right)⟩\in \le$
11 iffalse ${⊢}¬{1}^{st}\left({f}\left({n}\right)\right)\le {2}^{nd}\left({f}\left({n}\right)\right)\to if\left({1}^{st}\left({f}\left({n}\right)\right)\le {2}^{nd}\left({f}\left({n}\right)\right),{2}^{nd}\left({f}\left({n}\right)\right),{1}^{st}\left({f}\left({n}\right)\right)\right)={1}^{st}\left({f}\left({n}\right)\right)$
12 11 opeq2d ${⊢}¬{1}^{st}\left({f}\left({n}\right)\right)\le {2}^{nd}\left({f}\left({n}\right)\right)\to ⟨{1}^{st}\left({f}\left({n}\right)\right),if\left({1}^{st}\left({f}\left({n}\right)\right)\le {2}^{nd}\left({f}\left({n}\right)\right),{2}^{nd}\left({f}\left({n}\right)\right),{1}^{st}\left({f}\left({n}\right)\right)\right)⟩=⟨{1}^{st}\left({f}\left({n}\right)\right),{1}^{st}\left({f}\left({n}\right)\right)⟩$
13 12 adantl ${⊢}\left(\left({f}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {n}\in ℕ\right)\wedge ¬{1}^{st}\left({f}\left({n}\right)\right)\le {2}^{nd}\left({f}\left({n}\right)\right)\right)\to ⟨{1}^{st}\left({f}\left({n}\right)\right),if\left({1}^{st}\left({f}\left({n}\right)\right)\le {2}^{nd}\left({f}\left({n}\right)\right),{2}^{nd}\left({f}\left({n}\right)\right),{1}^{st}\left({f}\left({n}\right)\right)\right)⟩=⟨{1}^{st}\left({f}\left({n}\right)\right),{1}^{st}\left({f}\left({n}\right)\right)⟩$
14 elmapi ${⊢}{f}\in \left({{ℝ}^{2}}^{ℕ}\right)\to {f}:ℕ⟶{ℝ}^{2}$
15 14 ffvelrnda ${⊢}\left({f}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {n}\in ℕ\right)\to {f}\left({n}\right)\in {ℝ}^{2}$
16 xp1st ${⊢}{f}\left({n}\right)\in {ℝ}^{2}\to {1}^{st}\left({f}\left({n}\right)\right)\in ℝ$
17 15 16 syl ${⊢}\left({f}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {n}\in ℕ\right)\to {1}^{st}\left({f}\left({n}\right)\right)\in ℝ$
18 17 leidd ${⊢}\left({f}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {n}\in ℕ\right)\to {1}^{st}\left({f}\left({n}\right)\right)\le {1}^{st}\left({f}\left({n}\right)\right)$
19 df-br ${⊢}{1}^{st}\left({f}\left({n}\right)\right)\le {1}^{st}\left({f}\left({n}\right)\right)↔⟨{1}^{st}\left({f}\left({n}\right)\right),{1}^{st}\left({f}\left({n}\right)\right)⟩\in \le$
20 18 19 sylib ${⊢}\left({f}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {n}\in ℕ\right)\to ⟨{1}^{st}\left({f}\left({n}\right)\right),{1}^{st}\left({f}\left({n}\right)\right)⟩\in \le$
21 20 adantr ${⊢}\left(\left({f}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {n}\in ℕ\right)\wedge ¬{1}^{st}\left({f}\left({n}\right)\right)\le {2}^{nd}\left({f}\left({n}\right)\right)\right)\to ⟨{1}^{st}\left({f}\left({n}\right)\right),{1}^{st}\left({f}\left({n}\right)\right)⟩\in \le$
22 13 21 eqeltrd ${⊢}\left(\left({f}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {n}\in ℕ\right)\wedge ¬{1}^{st}\left({f}\left({n}\right)\right)\le {2}^{nd}\left({f}\left({n}\right)\right)\right)\to ⟨{1}^{st}\left({f}\left({n}\right)\right),if\left({1}^{st}\left({f}\left({n}\right)\right)\le {2}^{nd}\left({f}\left({n}\right)\right),{2}^{nd}\left({f}\left({n}\right)\right),{1}^{st}\left({f}\left({n}\right)\right)\right)⟩\in \le$
23 10 22 pm2.61dan ${⊢}\left({f}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {n}\in ℕ\right)\to ⟨{1}^{st}\left({f}\left({n}\right)\right),if\left({1}^{st}\left({f}\left({n}\right)\right)\le {2}^{nd}\left({f}\left({n}\right)\right),{2}^{nd}\left({f}\left({n}\right)\right),{1}^{st}\left({f}\left({n}\right)\right)\right)⟩\in \le$
24 xp2nd ${⊢}{f}\left({n}\right)\in {ℝ}^{2}\to {2}^{nd}\left({f}\left({n}\right)\right)\in ℝ$
25 15 24 syl ${⊢}\left({f}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {n}\in ℕ\right)\to {2}^{nd}\left({f}\left({n}\right)\right)\in ℝ$
26 25 17 ifcld ${⊢}\left({f}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {n}\in ℕ\right)\to if\left({1}^{st}\left({f}\left({n}\right)\right)\le {2}^{nd}\left({f}\left({n}\right)\right),{2}^{nd}\left({f}\left({n}\right)\right),{1}^{st}\left({f}\left({n}\right)\right)\right)\in ℝ$
27 opelxpi ${⊢}\left({1}^{st}\left({f}\left({n}\right)\right)\in ℝ\wedge if\left({1}^{st}\left({f}\left({n}\right)\right)\le {2}^{nd}\left({f}\left({n}\right)\right),{2}^{nd}\left({f}\left({n}\right)\right),{1}^{st}\left({f}\left({n}\right)\right)\right)\in ℝ\right)\to ⟨{1}^{st}\left({f}\left({n}\right)\right),if\left({1}^{st}\left({f}\left({n}\right)\right)\le {2}^{nd}\left({f}\left({n}\right)\right),{2}^{nd}\left({f}\left({n}\right)\right),{1}^{st}\left({f}\left({n}\right)\right)\right)⟩\in {ℝ}^{2}$
28 17 26 27 syl2anc ${⊢}\left({f}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {n}\in ℕ\right)\to ⟨{1}^{st}\left({f}\left({n}\right)\right),if\left({1}^{st}\left({f}\left({n}\right)\right)\le {2}^{nd}\left({f}\left({n}\right)\right),{2}^{nd}\left({f}\left({n}\right)\right),{1}^{st}\left({f}\left({n}\right)\right)\right)⟩\in {ℝ}^{2}$
29 23 28 elind ${⊢}\left({f}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {n}\in ℕ\right)\to ⟨{1}^{st}\left({f}\left({n}\right)\right),if\left({1}^{st}\left({f}\left({n}\right)\right)\le {2}^{nd}\left({f}\left({n}\right)\right),{2}^{nd}\left({f}\left({n}\right)\right),{1}^{st}\left({f}\left({n}\right)\right)\right)⟩\in \left(\le \cap {ℝ}^{2}\right)$
30 29 3 fmptd ${⊢}{f}\in \left({{ℝ}^{2}}^{ℕ}\right)\to {G}:ℕ⟶\le \cap {ℝ}^{2}$
31 reex ${⊢}ℝ\in \mathrm{V}$
32 31 31 xpex ${⊢}{ℝ}^{2}\in \mathrm{V}$
33 32 inex2 ${⊢}\le \cap {ℝ}^{2}\in \mathrm{V}$
34 33 a1i ${⊢}{f}\in \left({{ℝ}^{2}}^{ℕ}\right)\to \le \cap {ℝ}^{2}\in \mathrm{V}$
35 nnex ${⊢}ℕ\in \mathrm{V}$
36 35 a1i ${⊢}{f}\in \left({{ℝ}^{2}}^{ℕ}\right)\to ℕ\in \mathrm{V}$
37 34 36 elmapd ${⊢}{f}\in \left({{ℝ}^{2}}^{ℕ}\right)\to \left({G}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)↔{G}:ℕ⟶\le \cap {ℝ}^{2}\right)$
38 30 37 mpbird ${⊢}{f}\in \left({{ℝ}^{2}}^{ℕ}\right)\to {G}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)$
39 38 adantr ${⊢}\left({f}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge \left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {f}\right)\right)\right)\to {G}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)$
40 simpr ${⊢}\left({f}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\to {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)$
41 rexpssxrxp ${⊢}{ℝ}^{2}\subseteq {ℝ}^{*}×{ℝ}^{*}$
42 41 a1i ${⊢}{f}\in \left({{ℝ}^{2}}^{ℕ}\right)\to {ℝ}^{2}\subseteq {ℝ}^{*}×{ℝ}^{*}$
43 14 42 fssd ${⊢}{f}\in \left({{ℝ}^{2}}^{ℕ}\right)\to {f}:ℕ⟶{ℝ}^{*}×{ℝ}^{*}$
44 2fveq3 ${⊢}{k}={n}\to {1}^{st}\left({f}\left({k}\right)\right)={1}^{st}\left({f}\left({n}\right)\right)$
45 2fveq3 ${⊢}{k}={n}\to {2}^{nd}\left({f}\left({k}\right)\right)={2}^{nd}\left({f}\left({n}\right)\right)$
46 44 45 breq12d ${⊢}{k}={n}\to \left({1}^{st}\left({f}\left({k}\right)\right)\le {2}^{nd}\left({f}\left({k}\right)\right)↔{1}^{st}\left({f}\left({n}\right)\right)\le {2}^{nd}\left({f}\left({n}\right)\right)\right)$
47 46 cbvrabv ${⊢}\left\{{k}\in ℕ|{1}^{st}\left({f}\left({k}\right)\right)\le {2}^{nd}\left({f}\left({k}\right)\right)\right\}=\left\{{n}\in ℕ|{1}^{st}\left({f}\left({n}\right)\right)\le {2}^{nd}\left({f}\left({n}\right)\right)\right\}$
48 43 3 47 ovolval4lem1 ${⊢}{f}\in \left({{ℝ}^{2}}^{ℕ}\right)\to \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)=\bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)\wedge vol\circ \left(\left(.\right)\circ {f}\right)=vol\circ \left(\left(.\right)\circ {G}\right)\right)$
49 48 simpld ${⊢}{f}\in \left({{ℝ}^{2}}^{ℕ}\right)\to \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)=\bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)$
50 49 adantr ${⊢}\left({f}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\to \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)=\bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)$
51 40 50 sseqtrd ${⊢}\left({f}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\right)\to {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)$
52 51 adantrr ${⊢}\left({f}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge \left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {f}\right)\right)\right)\to {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)$
53 simpr ${⊢}\left({f}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {f}\right)\right)\to {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {f}\right)$
54 48 simprd ${⊢}{f}\in \left({{ℝ}^{2}}^{ℕ}\right)\to vol\circ \left(\left(.\right)\circ {f}\right)=vol\circ \left(\left(.\right)\circ {G}\right)$
55 coass ${⊢}\left(vol\circ \left(.\right)\right)\circ {f}=vol\circ \left(\left(.\right)\circ {f}\right)$
56 55 a1i ${⊢}{f}\in \left({{ℝ}^{2}}^{ℕ}\right)\to \left(vol\circ \left(.\right)\right)\circ {f}=vol\circ \left(\left(.\right)\circ {f}\right)$
57 coass ${⊢}\left(vol\circ \left(.\right)\right)\circ {G}=vol\circ \left(\left(.\right)\circ {G}\right)$
58 57 a1i ${⊢}{f}\in \left({{ℝ}^{2}}^{ℕ}\right)\to \left(vol\circ \left(.\right)\right)\circ {G}=vol\circ \left(\left(.\right)\circ {G}\right)$
59 54 56 58 3eqtr4d ${⊢}{f}\in \left({{ℝ}^{2}}^{ℕ}\right)\to \left(vol\circ \left(.\right)\right)\circ {f}=\left(vol\circ \left(.\right)\right)\circ {G}$
60 59 fveq2d ${⊢}{f}\in \left({{ℝ}^{2}}^{ℕ}\right)\to \mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {f}\right)=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {G}\right)$
61 60 adantr ${⊢}\left({f}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {f}\right)\right)\to \mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {f}\right)=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {G}\right)$
62 53 61 eqtrd ${⊢}\left({f}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {f}\right)\right)\to {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {G}\right)$
63 62 adantrl ${⊢}\left({f}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge \left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {f}\right)\right)\right)\to {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {G}\right)$
64 52 63 jca ${⊢}\left({f}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge \left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {f}\right)\right)\right)\to \left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {G}\right)\right)$
65 coeq2 ${⊢}{g}={G}\to \left(.\right)\circ {g}=\left(.\right)\circ {G}$
66 65 rneqd ${⊢}{g}={G}\to \mathrm{ran}\left(\left(.\right)\circ {g}\right)=\mathrm{ran}\left(\left(.\right)\circ {G}\right)$
67 66 unieqd ${⊢}{g}={G}\to \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)=\bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)$
68 67 sseq2d ${⊢}{g}={G}\to \left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)↔{A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)\right)$
69 coeq2 ${⊢}{g}={G}\to \left(vol\circ \left(.\right)\right)\circ {g}=\left(vol\circ \left(.\right)\right)\circ {G}$
70 69 fveq2d ${⊢}{g}={G}\to \mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {g}\right)=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {G}\right)$
71 70 eqeq2d ${⊢}{g}={G}\to \left({y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {g}\right)↔{y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {G}\right)\right)$
72 68 71 anbi12d ${⊢}{g}={G}\to \left(\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {g}\right)\right)↔\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {G}\right)\right)\right)$
73 72 rspcev ${⊢}\left({G}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\wedge \left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {G}\right)\right)\right)\to \exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {g}\right)\right)$
74 39 64 73 syl2anc ${⊢}\left({f}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge \left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {f}\right)\right)\right)\to \exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {g}\right)\right)$
75 74 rexlimiva ${⊢}\exists {f}\in \left({{ℝ}^{2}}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {f}\right)\right)\to \exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {g}\right)\right)$
76 inss2 ${⊢}\le \cap {ℝ}^{2}\subseteq {ℝ}^{2}$
77 mapss ${⊢}\left({ℝ}^{2}\in \mathrm{V}\wedge \le \cap {ℝ}^{2}\subseteq {ℝ}^{2}\right)\to {\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\subseteq {{ℝ}^{2}}^{ℕ}$
78 32 76 77 mp2an ${⊢}{\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\subseteq {{ℝ}^{2}}^{ℕ}$
79 78 sseli ${⊢}{g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\to {g}\in \left({{ℝ}^{2}}^{ℕ}\right)$
80 79 adantr ${⊢}\left({g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\wedge \left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {g}\right)\right)\right)\to {g}\in \left({{ℝ}^{2}}^{ℕ}\right)$
81 simpr ${⊢}\left({g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\wedge \left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {g}\right)\right)\right)\to \left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {g}\right)\right)$
82 coeq2 ${⊢}{f}={g}\to \left(.\right)\circ {f}=\left(.\right)\circ {g}$
83 82 rneqd ${⊢}{f}={g}\to \mathrm{ran}\left(\left(.\right)\circ {f}\right)=\mathrm{ran}\left(\left(.\right)\circ {g}\right)$
84 83 unieqd ${⊢}{f}={g}\to \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)=\bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)$
85 84 sseq2d ${⊢}{f}={g}\to \left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)↔{A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\right)$
86 coeq2 ${⊢}{f}={g}\to \left(vol\circ \left(.\right)\right)\circ {f}=\left(vol\circ \left(.\right)\right)\circ {g}$
87 86 fveq2d ${⊢}{f}={g}\to \mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {f}\right)=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {g}\right)$
88 87 eqeq2d ${⊢}{f}={g}\to \left({y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {f}\right)↔{y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {g}\right)\right)$
89 85 88 anbi12d ${⊢}{f}={g}\to \left(\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {f}\right)\right)↔\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {g}\right)\right)\right)$
90 89 rspcev ${⊢}\left({g}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge \left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {g}\right)\right)\right)\to \exists {f}\in \left({{ℝ}^{2}}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {f}\right)\right)$
91 80 81 90 syl2anc ${⊢}\left({g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\wedge \left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {g}\right)\right)\right)\to \exists {f}\in \left({{ℝ}^{2}}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {f}\right)\right)$
92 91 rexlimiva ${⊢}\exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {g}\right)\right)\to \exists {f}\in \left({{ℝ}^{2}}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {f}\right)\right)$
93 75 92 impbii ${⊢}\exists {f}\in \left({{ℝ}^{2}}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {f}\right)\right)↔\exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {g}\right)\right)$
94 93 rabbii ${⊢}\left\{{y}\in {ℝ}^{*}|\exists {f}\in \left({{ℝ}^{2}}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {f}\right)\right)\right\}=\left\{{y}\in {ℝ}^{*}|\exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {g}\right)\right)\right\}$
95 2 94 eqtri ${⊢}{M}=\left\{{y}\in {ℝ}^{*}|\exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {y}=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ {g}\right)\right)\right\}$
96 1 95 ovolval3 ${⊢}{\phi }\to {vol}^{*}\left({A}\right)=sup\left({M},{ℝ}^{*},<\right)$