# Metamath Proof Explorer

## Theorem uniiccdif

Description: A union of closed intervals differs from the equivalent union of open intervals by a nullset. (Contributed by Mario Carneiro, 25-Mar-2015)

Ref Expression
Hypothesis uniioombl.1 ${⊢}{\phi }\to {F}:ℕ⟶\le \cap {ℝ}^{2}$
Assertion uniiccdif ${⊢}{\phi }\to \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\setminus \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)=0\right)$

### Proof

Step Hyp Ref Expression
1 uniioombl.1 ${⊢}{\phi }\to {F}:ℕ⟶\le \cap {ℝ}^{2}$
2 ssun1 ${⊢}\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\cup \left({1}^{st}\left[\mathrm{ran}{F}\right]\cup {2}^{nd}\left[\mathrm{ran}{F}\right]\right)$
3 ovolfcl ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {x}\in ℕ\right)\to \left({1}^{st}\left({F}\left({x}\right)\right)\in ℝ\wedge {2}^{nd}\left({F}\left({x}\right)\right)\in ℝ\wedge {1}^{st}\left({F}\left({x}\right)\right)\le {2}^{nd}\left({F}\left({x}\right)\right)\right)$
4 1 3 sylan ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left({1}^{st}\left({F}\left({x}\right)\right)\in ℝ\wedge {2}^{nd}\left({F}\left({x}\right)\right)\in ℝ\wedge {1}^{st}\left({F}\left({x}\right)\right)\le {2}^{nd}\left({F}\left({x}\right)\right)\right)$
5 rexr ${⊢}{1}^{st}\left({F}\left({x}\right)\right)\in ℝ\to {1}^{st}\left({F}\left({x}\right)\right)\in {ℝ}^{*}$
6 rexr ${⊢}{2}^{nd}\left({F}\left({x}\right)\right)\in ℝ\to {2}^{nd}\left({F}\left({x}\right)\right)\in {ℝ}^{*}$
7 id ${⊢}{1}^{st}\left({F}\left({x}\right)\right)\le {2}^{nd}\left({F}\left({x}\right)\right)\to {1}^{st}\left({F}\left({x}\right)\right)\le {2}^{nd}\left({F}\left({x}\right)\right)$
8 prunioo ${⊢}\left({1}^{st}\left({F}\left({x}\right)\right)\in {ℝ}^{*}\wedge {2}^{nd}\left({F}\left({x}\right)\right)\in {ℝ}^{*}\wedge {1}^{st}\left({F}\left({x}\right)\right)\le {2}^{nd}\left({F}\left({x}\right)\right)\right)\to \left({1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)\right)\cup \left\{{1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)\right\}=\left[{1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)\right]$
9 5 6 7 8 syl3an ${⊢}\left({1}^{st}\left({F}\left({x}\right)\right)\in ℝ\wedge {2}^{nd}\left({F}\left({x}\right)\right)\in ℝ\wedge {1}^{st}\left({F}\left({x}\right)\right)\le {2}^{nd}\left({F}\left({x}\right)\right)\right)\to \left({1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)\right)\cup \left\{{1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)\right\}=\left[{1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)\right]$
10 4 9 syl ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left({1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)\right)\cup \left\{{1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)\right\}=\left[{1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)\right]$
11 fvco3 ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {x}\in ℕ\right)\to \left(\left(.\right)\circ {F}\right)\left({x}\right)=\left(.\right)\left({F}\left({x}\right)\right)$
12 1 11 sylan ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left(\left(.\right)\circ {F}\right)\left({x}\right)=\left(.\right)\left({F}\left({x}\right)\right)$
13 1 ffvelrnda ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to {F}\left({x}\right)\in \left(\le \cap {ℝ}^{2}\right)$
14 13 elin2d ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to {F}\left({x}\right)\in {ℝ}^{2}$
15 1st2nd2 ${⊢}{F}\left({x}\right)\in {ℝ}^{2}\to {F}\left({x}\right)=⟨{1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)⟩$
16 14 15 syl ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to {F}\left({x}\right)=⟨{1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)⟩$
17 16 fveq2d ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left(.\right)\left({F}\left({x}\right)\right)=\left(.\right)\left(⟨{1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)⟩\right)$
18 df-ov ${⊢}\left({1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)\right)=\left(.\right)\left(⟨{1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)⟩\right)$
19 17 18 syl6eqr ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left(.\right)\left({F}\left({x}\right)\right)=\left({1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)\right)$
20 12 19 eqtrd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left(\left(.\right)\circ {F}\right)\left({x}\right)=\left({1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)\right)$
21 df-pr ${⊢}\left\{\left({1}^{st}\circ {F}\right)\left({x}\right),\left({2}^{nd}\circ {F}\right)\left({x}\right)\right\}=\left\{\left({1}^{st}\circ {F}\right)\left({x}\right)\right\}\cup \left\{\left({2}^{nd}\circ {F}\right)\left({x}\right)\right\}$
22 fvco3 ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {x}\in ℕ\right)\to \left({1}^{st}\circ {F}\right)\left({x}\right)={1}^{st}\left({F}\left({x}\right)\right)$
23 1 22 sylan ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left({1}^{st}\circ {F}\right)\left({x}\right)={1}^{st}\left({F}\left({x}\right)\right)$
24 fvco3 ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {x}\in ℕ\right)\to \left({2}^{nd}\circ {F}\right)\left({x}\right)={2}^{nd}\left({F}\left({x}\right)\right)$
25 1 24 sylan ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left({2}^{nd}\circ {F}\right)\left({x}\right)={2}^{nd}\left({F}\left({x}\right)\right)$
26 23 25 preq12d ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left\{\left({1}^{st}\circ {F}\right)\left({x}\right),\left({2}^{nd}\circ {F}\right)\left({x}\right)\right\}=\left\{{1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)\right\}$
27 21 26 syl5eqr ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left\{\left({1}^{st}\circ {F}\right)\left({x}\right)\right\}\cup \left\{\left({2}^{nd}\circ {F}\right)\left({x}\right)\right\}=\left\{{1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)\right\}$
28 20 27 uneq12d ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left(\left(.\right)\circ {F}\right)\left({x}\right)\cup \left(\left\{\left({1}^{st}\circ {F}\right)\left({x}\right)\right\}\cup \left\{\left({2}^{nd}\circ {F}\right)\left({x}\right)\right\}\right)=\left({1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)\right)\cup \left\{{1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)\right\}$
29 fvco3 ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {x}\in ℕ\right)\to \left(\left[.\right]\circ {F}\right)\left({x}\right)=\left[.\right]\left({F}\left({x}\right)\right)$
30 1 29 sylan ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left(\left[.\right]\circ {F}\right)\left({x}\right)=\left[.\right]\left({F}\left({x}\right)\right)$
31 16 fveq2d ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left[.\right]\left({F}\left({x}\right)\right)=\left[.\right]\left(⟨{1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)⟩\right)$
32 df-ov ${⊢}\left[{1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)\right]=\left[.\right]\left(⟨{1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)⟩\right)$
33 31 32 syl6eqr ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left[.\right]\left({F}\left({x}\right)\right)=\left[{1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)\right]$
34 30 33 eqtrd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left(\left[.\right]\circ {F}\right)\left({x}\right)=\left[{1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)\right]$
35 10 28 34 3eqtr4rd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left(\left[.\right]\circ {F}\right)\left({x}\right)=\left(\left(.\right)\circ {F}\right)\left({x}\right)\cup \left(\left\{\left({1}^{st}\circ {F}\right)\left({x}\right)\right\}\cup \left\{\left({2}^{nd}\circ {F}\right)\left({x}\right)\right\}\right)$
36 35 iuneq2dv ${⊢}{\phi }\to \bigcup _{{x}\in ℕ}\left(\left[.\right]\circ {F}\right)\left({x}\right)=\bigcup _{{x}\in ℕ}\left(\left(\left(.\right)\circ {F}\right)\left({x}\right)\cup \left(\left\{\left({1}^{st}\circ {F}\right)\left({x}\right)\right\}\cup \left\{\left({2}^{nd}\circ {F}\right)\left({x}\right)\right\}\right)\right)$
37 iccf ${⊢}\left[.\right]:{ℝ}^{*}×{ℝ}^{*}⟶𝒫{ℝ}^{*}$
38 ffn ${⊢}\left[.\right]:{ℝ}^{*}×{ℝ}^{*}⟶𝒫{ℝ}^{*}\to \left[.\right]Fn\left({ℝ}^{*}×{ℝ}^{*}\right)$
39 37 38 ax-mp ${⊢}\left[.\right]Fn\left({ℝ}^{*}×{ℝ}^{*}\right)$
40 inss2 ${⊢}\le \cap {ℝ}^{2}\subseteq {ℝ}^{2}$
41 rexpssxrxp ${⊢}{ℝ}^{2}\subseteq {ℝ}^{*}×{ℝ}^{*}$
42 40 41 sstri ${⊢}\le \cap {ℝ}^{2}\subseteq {ℝ}^{*}×{ℝ}^{*}$
43 fss ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge \le \cap {ℝ}^{2}\subseteq {ℝ}^{*}×{ℝ}^{*}\right)\to {F}:ℕ⟶{ℝ}^{*}×{ℝ}^{*}$
44 1 42 43 sylancl ${⊢}{\phi }\to {F}:ℕ⟶{ℝ}^{*}×{ℝ}^{*}$
45 fnfco ${⊢}\left(\left[.\right]Fn\left({ℝ}^{*}×{ℝ}^{*}\right)\wedge {F}:ℕ⟶{ℝ}^{*}×{ℝ}^{*}\right)\to \left(\left[.\right]\circ {F}\right)Fnℕ$
46 39 44 45 sylancr ${⊢}{\phi }\to \left(\left[.\right]\circ {F}\right)Fnℕ$
47 fniunfv ${⊢}\left(\left[.\right]\circ {F}\right)Fnℕ\to \bigcup _{{x}\in ℕ}\left(\left[.\right]\circ {F}\right)\left({x}\right)=\bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)$
48 46 47 syl ${⊢}{\phi }\to \bigcup _{{x}\in ℕ}\left(\left[.\right]\circ {F}\right)\left({x}\right)=\bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)$
49 iunun ${⊢}\bigcup _{{x}\in ℕ}\left(\left(\left(.\right)\circ {F}\right)\left({x}\right)\cup \left(\left\{\left({1}^{st}\circ {F}\right)\left({x}\right)\right\}\cup \left\{\left({2}^{nd}\circ {F}\right)\left({x}\right)\right\}\right)\right)=\bigcup _{{x}\in ℕ}\left(\left(.\right)\circ {F}\right)\left({x}\right)\cup \bigcup _{{x}\in ℕ}\left(\left\{\left({1}^{st}\circ {F}\right)\left({x}\right)\right\}\cup \left\{\left({2}^{nd}\circ {F}\right)\left({x}\right)\right\}\right)$
50 ioof ${⊢}\left(.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫ℝ$
51 ffn ${⊢}\left(.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫ℝ\to \left(.\right)Fn\left({ℝ}^{*}×{ℝ}^{*}\right)$
52 50 51 ax-mp ${⊢}\left(.\right)Fn\left({ℝ}^{*}×{ℝ}^{*}\right)$
53 fnfco ${⊢}\left(\left(.\right)Fn\left({ℝ}^{*}×{ℝ}^{*}\right)\wedge {F}:ℕ⟶{ℝ}^{*}×{ℝ}^{*}\right)\to \left(\left(.\right)\circ {F}\right)Fnℕ$
54 52 44 53 sylancr ${⊢}{\phi }\to \left(\left(.\right)\circ {F}\right)Fnℕ$
55 fniunfv ${⊢}\left(\left(.\right)\circ {F}\right)Fnℕ\to \bigcup _{{x}\in ℕ}\left(\left(.\right)\circ {F}\right)\left({x}\right)=\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)$
56 54 55 syl ${⊢}{\phi }\to \bigcup _{{x}\in ℕ}\left(\left(.\right)\circ {F}\right)\left({x}\right)=\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)$
57 iunun ${⊢}\bigcup _{{x}\in ℕ}\left(\left\{\left({1}^{st}\circ {F}\right)\left({x}\right)\right\}\cup \left\{\left({2}^{nd}\circ {F}\right)\left({x}\right)\right\}\right)=\bigcup _{{x}\in ℕ}\left\{\left({1}^{st}\circ {F}\right)\left({x}\right)\right\}\cup \bigcup _{{x}\in ℕ}\left\{\left({2}^{nd}\circ {F}\right)\left({x}\right)\right\}$
58 fo1st ${⊢}{1}^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$
59 fofn ${⊢}{1}^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\to {1}^{st}Fn\mathrm{V}$
60 58 59 ax-mp ${⊢}{1}^{st}Fn\mathrm{V}$
61 ssv ${⊢}\le \cap {ℝ}^{2}\subseteq \mathrm{V}$
62 fss ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge \le \cap {ℝ}^{2}\subseteq \mathrm{V}\right)\to {F}:ℕ⟶\mathrm{V}$
63 1 61 62 sylancl ${⊢}{\phi }\to {F}:ℕ⟶\mathrm{V}$
64 fnfco ${⊢}\left({1}^{st}Fn\mathrm{V}\wedge {F}:ℕ⟶\mathrm{V}\right)\to \left({1}^{st}\circ {F}\right)Fnℕ$
65 60 63 64 sylancr ${⊢}{\phi }\to \left({1}^{st}\circ {F}\right)Fnℕ$
66 fnfun ${⊢}\left({1}^{st}\circ {F}\right)Fnℕ\to \mathrm{Fun}\left({1}^{st}\circ {F}\right)$
67 65 66 syl ${⊢}{\phi }\to \mathrm{Fun}\left({1}^{st}\circ {F}\right)$
68 fndm ${⊢}\left({1}^{st}\circ {F}\right)Fnℕ\to \mathrm{dom}\left({1}^{st}\circ {F}\right)=ℕ$
69 eqimss2 ${⊢}\mathrm{dom}\left({1}^{st}\circ {F}\right)=ℕ\to ℕ\subseteq \mathrm{dom}\left({1}^{st}\circ {F}\right)$
70 65 68 69 3syl ${⊢}{\phi }\to ℕ\subseteq \mathrm{dom}\left({1}^{st}\circ {F}\right)$
71 dfimafn2 ${⊢}\left(\mathrm{Fun}\left({1}^{st}\circ {F}\right)\wedge ℕ\subseteq \mathrm{dom}\left({1}^{st}\circ {F}\right)\right)\to \left({1}^{st}\circ {F}\right)\left[ℕ\right]=\bigcup _{{x}\in ℕ}\left\{\left({1}^{st}\circ {F}\right)\left({x}\right)\right\}$
72 67 70 71 syl2anc ${⊢}{\phi }\to \left({1}^{st}\circ {F}\right)\left[ℕ\right]=\bigcup _{{x}\in ℕ}\left\{\left({1}^{st}\circ {F}\right)\left({x}\right)\right\}$
73 fnima ${⊢}\left({1}^{st}\circ {F}\right)Fnℕ\to \left({1}^{st}\circ {F}\right)\left[ℕ\right]=\mathrm{ran}\left({1}^{st}\circ {F}\right)$
74 65 73 syl ${⊢}{\phi }\to \left({1}^{st}\circ {F}\right)\left[ℕ\right]=\mathrm{ran}\left({1}^{st}\circ {F}\right)$
75 72 74 eqtr3d ${⊢}{\phi }\to \bigcup _{{x}\in ℕ}\left\{\left({1}^{st}\circ {F}\right)\left({x}\right)\right\}=\mathrm{ran}\left({1}^{st}\circ {F}\right)$
76 rnco2 ${⊢}\mathrm{ran}\left({1}^{st}\circ {F}\right)={1}^{st}\left[\mathrm{ran}{F}\right]$
77 75 76 syl6eq ${⊢}{\phi }\to \bigcup _{{x}\in ℕ}\left\{\left({1}^{st}\circ {F}\right)\left({x}\right)\right\}={1}^{st}\left[\mathrm{ran}{F}\right]$
78 fo2nd ${⊢}{2}^{nd}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$
79 fofn ${⊢}{2}^{nd}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\to {2}^{nd}Fn\mathrm{V}$
80 78 79 ax-mp ${⊢}{2}^{nd}Fn\mathrm{V}$
81 fnfco ${⊢}\left({2}^{nd}Fn\mathrm{V}\wedge {F}:ℕ⟶\mathrm{V}\right)\to \left({2}^{nd}\circ {F}\right)Fnℕ$
82 80 63 81 sylancr ${⊢}{\phi }\to \left({2}^{nd}\circ {F}\right)Fnℕ$
83 fnfun ${⊢}\left({2}^{nd}\circ {F}\right)Fnℕ\to \mathrm{Fun}\left({2}^{nd}\circ {F}\right)$
84 82 83 syl ${⊢}{\phi }\to \mathrm{Fun}\left({2}^{nd}\circ {F}\right)$
85 fndm ${⊢}\left({2}^{nd}\circ {F}\right)Fnℕ\to \mathrm{dom}\left({2}^{nd}\circ {F}\right)=ℕ$
86 eqimss2 ${⊢}\mathrm{dom}\left({2}^{nd}\circ {F}\right)=ℕ\to ℕ\subseteq \mathrm{dom}\left({2}^{nd}\circ {F}\right)$
87 82 85 86 3syl ${⊢}{\phi }\to ℕ\subseteq \mathrm{dom}\left({2}^{nd}\circ {F}\right)$
88 dfimafn2 ${⊢}\left(\mathrm{Fun}\left({2}^{nd}\circ {F}\right)\wedge ℕ\subseteq \mathrm{dom}\left({2}^{nd}\circ {F}\right)\right)\to \left({2}^{nd}\circ {F}\right)\left[ℕ\right]=\bigcup _{{x}\in ℕ}\left\{\left({2}^{nd}\circ {F}\right)\left({x}\right)\right\}$
89 84 87 88 syl2anc ${⊢}{\phi }\to \left({2}^{nd}\circ {F}\right)\left[ℕ\right]=\bigcup _{{x}\in ℕ}\left\{\left({2}^{nd}\circ {F}\right)\left({x}\right)\right\}$
90 fnima ${⊢}\left({2}^{nd}\circ {F}\right)Fnℕ\to \left({2}^{nd}\circ {F}\right)\left[ℕ\right]=\mathrm{ran}\left({2}^{nd}\circ {F}\right)$
91 82 90 syl ${⊢}{\phi }\to \left({2}^{nd}\circ {F}\right)\left[ℕ\right]=\mathrm{ran}\left({2}^{nd}\circ {F}\right)$
92 89 91 eqtr3d ${⊢}{\phi }\to \bigcup _{{x}\in ℕ}\left\{\left({2}^{nd}\circ {F}\right)\left({x}\right)\right\}=\mathrm{ran}\left({2}^{nd}\circ {F}\right)$
93 rnco2 ${⊢}\mathrm{ran}\left({2}^{nd}\circ {F}\right)={2}^{nd}\left[\mathrm{ran}{F}\right]$
94 92 93 syl6eq ${⊢}{\phi }\to \bigcup _{{x}\in ℕ}\left\{\left({2}^{nd}\circ {F}\right)\left({x}\right)\right\}={2}^{nd}\left[\mathrm{ran}{F}\right]$
95 77 94 uneq12d ${⊢}{\phi }\to \bigcup _{{x}\in ℕ}\left\{\left({1}^{st}\circ {F}\right)\left({x}\right)\right\}\cup \bigcup _{{x}\in ℕ}\left\{\left({2}^{nd}\circ {F}\right)\left({x}\right)\right\}={1}^{st}\left[\mathrm{ran}{F}\right]\cup {2}^{nd}\left[\mathrm{ran}{F}\right]$
96 57 95 syl5eq ${⊢}{\phi }\to \bigcup _{{x}\in ℕ}\left(\left\{\left({1}^{st}\circ {F}\right)\left({x}\right)\right\}\cup \left\{\left({2}^{nd}\circ {F}\right)\left({x}\right)\right\}\right)={1}^{st}\left[\mathrm{ran}{F}\right]\cup {2}^{nd}\left[\mathrm{ran}{F}\right]$
97 56 96 uneq12d ${⊢}{\phi }\to \bigcup _{{x}\in ℕ}\left(\left(.\right)\circ {F}\right)\left({x}\right)\cup \bigcup _{{x}\in ℕ}\left(\left\{\left({1}^{st}\circ {F}\right)\left({x}\right)\right\}\cup \left\{\left({2}^{nd}\circ {F}\right)\left({x}\right)\right\}\right)=\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\cup \left({1}^{st}\left[\mathrm{ran}{F}\right]\cup {2}^{nd}\left[\mathrm{ran}{F}\right]\right)$
98 49 97 syl5eq ${⊢}{\phi }\to \bigcup _{{x}\in ℕ}\left(\left(\left(.\right)\circ {F}\right)\left({x}\right)\cup \left(\left\{\left({1}^{st}\circ {F}\right)\left({x}\right)\right\}\cup \left\{\left({2}^{nd}\circ {F}\right)\left({x}\right)\right\}\right)\right)=\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\cup \left({1}^{st}\left[\mathrm{ran}{F}\right]\cup {2}^{nd}\left[\mathrm{ran}{F}\right]\right)$
99 36 48 98 3eqtr3d ${⊢}{\phi }\to \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)=\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\cup \left({1}^{st}\left[\mathrm{ran}{F}\right]\cup {2}^{nd}\left[\mathrm{ran}{F}\right]\right)$
100 2 99 sseqtrrid ${⊢}{\phi }\to \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)$
101 ovolficcss ${⊢}{F}:ℕ⟶\le \cap {ℝ}^{2}\to \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\subseteq ℝ$
102 1 101 syl ${⊢}{\phi }\to \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\subseteq ℝ$
103 102 ssdifssd ${⊢}{\phi }\to \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\setminus \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\subseteq ℝ$
104 omelon ${⊢}\mathrm{\omega }\in \mathrm{On}$
105 nnenom ${⊢}ℕ\approx \mathrm{\omega }$
106 105 ensymi ${⊢}\mathrm{\omega }\approx ℕ$
107 isnumi ${⊢}\left(\mathrm{\omega }\in \mathrm{On}\wedge \mathrm{\omega }\approx ℕ\right)\to ℕ\in \mathrm{dom}\mathrm{card}$
108 104 106 107 mp2an ${⊢}ℕ\in \mathrm{dom}\mathrm{card}$
109 fofun ${⊢}{1}^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\to \mathrm{Fun}{1}^{st}$
110 58 109 ax-mp ${⊢}\mathrm{Fun}{1}^{st}$
111 ssv ${⊢}\mathrm{ran}{F}\subseteq \mathrm{V}$
112 fof ${⊢}{1}^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\to {1}^{st}:\mathrm{V}⟶\mathrm{V}$
113 58 112 ax-mp ${⊢}{1}^{st}:\mathrm{V}⟶\mathrm{V}$
114 113 fdmi ${⊢}\mathrm{dom}{1}^{st}=\mathrm{V}$
115 111 114 sseqtrri ${⊢}\mathrm{ran}{F}\subseteq \mathrm{dom}{1}^{st}$
116 fores ${⊢}\left(\mathrm{Fun}{1}^{st}\wedge \mathrm{ran}{F}\subseteq \mathrm{dom}{1}^{st}\right)\to \left({{1}^{st}↾}_{\mathrm{ran}{F}}\right):\mathrm{ran}{F}\underset{onto}{⟶}{1}^{st}\left[\mathrm{ran}{F}\right]$
117 110 115 116 mp2an ${⊢}\left({{1}^{st}↾}_{\mathrm{ran}{F}}\right):\mathrm{ran}{F}\underset{onto}{⟶}{1}^{st}\left[\mathrm{ran}{F}\right]$
118 1 ffnd ${⊢}{\phi }\to {F}Fnℕ$
119 dffn4 ${⊢}{F}Fnℕ↔{F}:ℕ\underset{onto}{⟶}\mathrm{ran}{F}$
120 118 119 sylib ${⊢}{\phi }\to {F}:ℕ\underset{onto}{⟶}\mathrm{ran}{F}$
121 foco ${⊢}\left(\left({{1}^{st}↾}_{\mathrm{ran}{F}}\right):\mathrm{ran}{F}\underset{onto}{⟶}{1}^{st}\left[\mathrm{ran}{F}\right]\wedge {F}:ℕ\underset{onto}{⟶}\mathrm{ran}{F}\right)\to \left(\left({{1}^{st}↾}_{\mathrm{ran}{F}}\right)\circ {F}\right):ℕ\underset{onto}{⟶}{1}^{st}\left[\mathrm{ran}{F}\right]$
122 117 120 121 sylancr ${⊢}{\phi }\to \left(\left({{1}^{st}↾}_{\mathrm{ran}{F}}\right)\circ {F}\right):ℕ\underset{onto}{⟶}{1}^{st}\left[\mathrm{ran}{F}\right]$
123 fodomnum ${⊢}ℕ\in \mathrm{dom}\mathrm{card}\to \left(\left(\left({{1}^{st}↾}_{\mathrm{ran}{F}}\right)\circ {F}\right):ℕ\underset{onto}{⟶}{1}^{st}\left[\mathrm{ran}{F}\right]\to {1}^{st}\left[\mathrm{ran}{F}\right]\preccurlyeq ℕ\right)$
124 108 122 123 mpsyl ${⊢}{\phi }\to {1}^{st}\left[\mathrm{ran}{F}\right]\preccurlyeq ℕ$
125 domentr ${⊢}\left({1}^{st}\left[\mathrm{ran}{F}\right]\preccurlyeq ℕ\wedge ℕ\approx \mathrm{\omega }\right)\to {1}^{st}\left[\mathrm{ran}{F}\right]\preccurlyeq \mathrm{\omega }$
126 124 105 125 sylancl ${⊢}{\phi }\to {1}^{st}\left[\mathrm{ran}{F}\right]\preccurlyeq \mathrm{\omega }$
127 fofun ${⊢}{2}^{nd}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\to \mathrm{Fun}{2}^{nd}$
128 78 127 ax-mp ${⊢}\mathrm{Fun}{2}^{nd}$
129 fof ${⊢}{2}^{nd}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\to {2}^{nd}:\mathrm{V}⟶\mathrm{V}$
130 78 129 ax-mp ${⊢}{2}^{nd}:\mathrm{V}⟶\mathrm{V}$
131 130 fdmi ${⊢}\mathrm{dom}{2}^{nd}=\mathrm{V}$
132 111 131 sseqtrri ${⊢}\mathrm{ran}{F}\subseteq \mathrm{dom}{2}^{nd}$
133 fores ${⊢}\left(\mathrm{Fun}{2}^{nd}\wedge \mathrm{ran}{F}\subseteq \mathrm{dom}{2}^{nd}\right)\to \left({{2}^{nd}↾}_{\mathrm{ran}{F}}\right):\mathrm{ran}{F}\underset{onto}{⟶}{2}^{nd}\left[\mathrm{ran}{F}\right]$
134 128 132 133 mp2an ${⊢}\left({{2}^{nd}↾}_{\mathrm{ran}{F}}\right):\mathrm{ran}{F}\underset{onto}{⟶}{2}^{nd}\left[\mathrm{ran}{F}\right]$
135 foco ${⊢}\left(\left({{2}^{nd}↾}_{\mathrm{ran}{F}}\right):\mathrm{ran}{F}\underset{onto}{⟶}{2}^{nd}\left[\mathrm{ran}{F}\right]\wedge {F}:ℕ\underset{onto}{⟶}\mathrm{ran}{F}\right)\to \left(\left({{2}^{nd}↾}_{\mathrm{ran}{F}}\right)\circ {F}\right):ℕ\underset{onto}{⟶}{2}^{nd}\left[\mathrm{ran}{F}\right]$
136 134 120 135 sylancr ${⊢}{\phi }\to \left(\left({{2}^{nd}↾}_{\mathrm{ran}{F}}\right)\circ {F}\right):ℕ\underset{onto}{⟶}{2}^{nd}\left[\mathrm{ran}{F}\right]$
137 fodomnum ${⊢}ℕ\in \mathrm{dom}\mathrm{card}\to \left(\left(\left({{2}^{nd}↾}_{\mathrm{ran}{F}}\right)\circ {F}\right):ℕ\underset{onto}{⟶}{2}^{nd}\left[\mathrm{ran}{F}\right]\to {2}^{nd}\left[\mathrm{ran}{F}\right]\preccurlyeq ℕ\right)$
138 108 136 137 mpsyl ${⊢}{\phi }\to {2}^{nd}\left[\mathrm{ran}{F}\right]\preccurlyeq ℕ$
139 domentr ${⊢}\left({2}^{nd}\left[\mathrm{ran}{F}\right]\preccurlyeq ℕ\wedge ℕ\approx \mathrm{\omega }\right)\to {2}^{nd}\left[\mathrm{ran}{F}\right]\preccurlyeq \mathrm{\omega }$
140 138 105 139 sylancl ${⊢}{\phi }\to {2}^{nd}\left[\mathrm{ran}{F}\right]\preccurlyeq \mathrm{\omega }$
141 unctb ${⊢}\left({1}^{st}\left[\mathrm{ran}{F}\right]\preccurlyeq \mathrm{\omega }\wedge {2}^{nd}\left[\mathrm{ran}{F}\right]\preccurlyeq \mathrm{\omega }\right)\to \left({1}^{st}\left[\mathrm{ran}{F}\right]\cup {2}^{nd}\left[\mathrm{ran}{F}\right]\right)\preccurlyeq \mathrm{\omega }$
142 126 140 141 syl2anc ${⊢}{\phi }\to \left({1}^{st}\left[\mathrm{ran}{F}\right]\cup {2}^{nd}\left[\mathrm{ran}{F}\right]\right)\preccurlyeq \mathrm{\omega }$
143 ctex ${⊢}\left({1}^{st}\left[\mathrm{ran}{F}\right]\cup {2}^{nd}\left[\mathrm{ran}{F}\right]\right)\preccurlyeq \mathrm{\omega }\to {1}^{st}\left[\mathrm{ran}{F}\right]\cup {2}^{nd}\left[\mathrm{ran}{F}\right]\in \mathrm{V}$
144 142 143 syl ${⊢}{\phi }\to {1}^{st}\left[\mathrm{ran}{F}\right]\cup {2}^{nd}\left[\mathrm{ran}{F}\right]\in \mathrm{V}$
145 ssid ${⊢}\bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)$
146 145 99 sseqtrid ${⊢}{\phi }\to \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\cup \left({1}^{st}\left[\mathrm{ran}{F}\right]\cup {2}^{nd}\left[\mathrm{ran}{F}\right]\right)$
147 ssundif ${⊢}\bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\cup \left({1}^{st}\left[\mathrm{ran}{F}\right]\cup {2}^{nd}\left[\mathrm{ran}{F}\right]\right)↔\bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\setminus \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\subseteq {1}^{st}\left[\mathrm{ran}{F}\right]\cup {2}^{nd}\left[\mathrm{ran}{F}\right]$
148 146 147 sylib ${⊢}{\phi }\to \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\setminus \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\subseteq {1}^{st}\left[\mathrm{ran}{F}\right]\cup {2}^{nd}\left[\mathrm{ran}{F}\right]$
149 ssdomg ${⊢}{1}^{st}\left[\mathrm{ran}{F}\right]\cup {2}^{nd}\left[\mathrm{ran}{F}\right]\in \mathrm{V}\to \left(\bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\setminus \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\subseteq {1}^{st}\left[\mathrm{ran}{F}\right]\cup {2}^{nd}\left[\mathrm{ran}{F}\right]\to \left(\bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\setminus \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\preccurlyeq \left({1}^{st}\left[\mathrm{ran}{F}\right]\cup {2}^{nd}\left[\mathrm{ran}{F}\right]\right)\right)$
150 144 148 149 sylc ${⊢}{\phi }\to \left(\bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\setminus \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\preccurlyeq \left({1}^{st}\left[\mathrm{ran}{F}\right]\cup {2}^{nd}\left[\mathrm{ran}{F}\right]\right)$
151 domtr ${⊢}\left(\left(\bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\setminus \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\preccurlyeq \left({1}^{st}\left[\mathrm{ran}{F}\right]\cup {2}^{nd}\left[\mathrm{ran}{F}\right]\right)\wedge \left({1}^{st}\left[\mathrm{ran}{F}\right]\cup {2}^{nd}\left[\mathrm{ran}{F}\right]\right)\preccurlyeq \mathrm{\omega }\right)\to \left(\bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\setminus \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\preccurlyeq \mathrm{\omega }$
152 150 142 151 syl2anc ${⊢}{\phi }\to \left(\bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\setminus \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\preccurlyeq \mathrm{\omega }$
153 domentr ${⊢}\left(\left(\bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\setminus \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\preccurlyeq \mathrm{\omega }\wedge \mathrm{\omega }\approx ℕ\right)\to \left(\bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\setminus \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\preccurlyeq ℕ$
154 152 106 153 sylancl ${⊢}{\phi }\to \left(\bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\setminus \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\preccurlyeq ℕ$
155 ovolctb2 ${⊢}\left(\bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\setminus \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\subseteq ℝ\wedge \left(\bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\setminus \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\preccurlyeq ℕ\right)\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\setminus \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)=0$
156 103 154 155 syl2anc ${⊢}{\phi }\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\setminus \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)=0$
157 100 156 jca ${⊢}{\phi }\to \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\setminus \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)=0\right)$