This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uniioombllem4

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

Ref Expression
Hypotheses uniioombl.1 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
uniioombl.2 ⊢ ( 𝜑 → Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) )
uniioombl.3 ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
uniioombl.a ⊢ 𝐴 = ∪ ran ( (,) ∘ 𝐹 )
uniioombl.e ⊢ ( 𝜑 → ( vol* ‘ 𝐸 ) ∈ ℝ )
uniioombl.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
uniioombl.g ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
uniioombl.s ⊢ ( 𝜑 → 𝐸 ⊆ ∪ ran ( (,) ∘ 𝐺 ) )
uniioombl.t ⊢ 𝑇 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) )
uniioombl.v ⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐸 ) + 𝐶 ) )
uniioombl.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
uniioombl.m2 ⊢ ( 𝜑 → ( abs ‘ ( ( 𝑇 ‘ 𝑀 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 )
uniioombl.k ⊢ 𝐾 = ∪ ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) )
uniioombl.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
uniioombl.n2 ⊢ ( 𝜑 → ∀ 𝑗 ∈ ( 1 ... 𝑀 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑀 ) )
uniioombl.l ⊢ 𝐿 = ∪ ( ( (,) ∘ 𝐹 ) “ ( 1 ... 𝑁 ) )
Assertion uniioombllem4 ( 𝜑 → ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) ≤ ( ( vol* ‘ ( 𝐾 ∩ 𝐿 ) ) + 𝐶 ) )

Proof

Step Hyp Ref Expression
1 uniioombl.1 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
2 uniioombl.2 ⊢ ( 𝜑 → Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) )
3 uniioombl.3 ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
4 uniioombl.a ⊢ 𝐴 = ∪ ran ( (,) ∘ 𝐹 )
5 uniioombl.e ⊢ ( 𝜑 → ( vol* ‘ 𝐸 ) ∈ ℝ )
6 uniioombl.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
7 uniioombl.g ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
8 uniioombl.s ⊢ ( 𝜑 → 𝐸 ⊆ ∪ ran ( (,) ∘ 𝐺 ) )
9 uniioombl.t ⊢ 𝑇 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) )
10 uniioombl.v ⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐸 ) + 𝐶 ) )
11 uniioombl.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
12 uniioombl.m2 ⊢ ( 𝜑 → ( abs ‘ ( ( 𝑇 ‘ 𝑀 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 )
13 uniioombl.k ⊢ 𝐾 = ∪ ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) )
14 uniioombl.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
15 uniioombl.n2 ⊢ ( 𝜑 → ∀ 𝑗 ∈ ( 1 ... 𝑀 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑀 ) )
16 uniioombl.l ⊢ 𝐿 = ∪ ( ( (,) ∘ 𝐹 ) “ ( 1 ... 𝑁 ) )
17 inss1 ⊢ ( 𝐾 ∩ 𝐴 ) ⊆ 𝐾
18 imassrn ⊢ ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) ) ⊆ ran ( (,) ∘ 𝐺 )
19 18 unissi ⊢ ∪ ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) ) ⊆ ∪ ran ( (,) ∘ 𝐺 )
20 13 19 eqsstri ⊢ 𝐾 ⊆ ∪ ran ( (,) ∘ 𝐺 )
21 7 uniiccdif ⊢ ( 𝜑 → ( ∪ ran ( (,) ∘ 𝐺 ) ⊆ ∪ ran ( [,] ∘ 𝐺 ) ∧ ( vol* ‘ ( ∪ ran ( [,] ∘ 𝐺 ) ∖ ∪ ran ( (,) ∘ 𝐺 ) ) ) = 0 ) )
22 21 simpld ⊢ ( 𝜑 → ∪ ran ( (,) ∘ 𝐺 ) ⊆ ∪ ran ( [,] ∘ 𝐺 ) )
23 ovolficcss ⊢ ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ∪ ran ( [,] ∘ 𝐺 ) ⊆ ℝ )
24 7 23 syl ⊢ ( 𝜑 → ∪ ran ( [,] ∘ 𝐺 ) ⊆ ℝ )
25 22 24 sstrd ⊢ ( 𝜑 → ∪ ran ( (,) ∘ 𝐺 ) ⊆ ℝ )
26 20 25 sstrid ⊢ ( 𝜑 → 𝐾 ⊆ ℝ )
27 1 2 3 4 5 6 7 8 9 10 uniioombllem1 ⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ )
28 ssid ⊢ ∪ ran ( (,) ∘ 𝐺 ) ⊆ ∪ ran ( (,) ∘ 𝐺 )
29 9 ovollb ⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ∪ ran ( (,) ∘ 𝐺 ) ⊆ ∪ ran ( (,) ∘ 𝐺 ) ) → ( vol* ‘ ∪ ran ( (,) ∘ 𝐺 ) ) ≤ sup ( ran 𝑇 , ℝ* , < ) )
30 7 28 29 sylancl ⊢ ( 𝜑 → ( vol* ‘ ∪ ran ( (,) ∘ 𝐺 ) ) ≤ sup ( ran 𝑇 , ℝ* , < ) )
31 ovollecl ⊢ ( ( ∪ ran ( (,) ∘ 𝐺 ) ⊆ ℝ ∧ sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ ∧ ( vol* ‘ ∪ ran ( (,) ∘ 𝐺 ) ) ≤ sup ( ran 𝑇 , ℝ* , < ) ) → ( vol* ‘ ∪ ran ( (,) ∘ 𝐺 ) ) ∈ ℝ )
32 25 27 30 31 syl3anc ⊢ ( 𝜑 → ( vol* ‘ ∪ ran ( (,) ∘ 𝐺 ) ) ∈ ℝ )
33 ovolsscl ⊢ ( ( 𝐾 ⊆ ∪ ran ( (,) ∘ 𝐺 ) ∧ ∪ ran ( (,) ∘ 𝐺 ) ⊆ ℝ ∧ ( vol* ‘ ∪ ran ( (,) ∘ 𝐺 ) ) ∈ ℝ ) → ( vol* ‘ 𝐾 ) ∈ ℝ )
34 20 25 32 33 mp3an2i ⊢ ( 𝜑 → ( vol* ‘ 𝐾 ) ∈ ℝ )
35 ovolsscl ⊢ ( ( ( 𝐾 ∩ 𝐴 ) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ ( vol* ‘ 𝐾 ) ∈ ℝ ) → ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) ∈ ℝ )
36 17 26 34 35 mp3an2i ⊢ ( 𝜑 → ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) ∈ ℝ )
37 inss1 ⊢ ( 𝐾 ∩ 𝐿 ) ⊆ 𝐾
38 ovolsscl ⊢ ( ( ( 𝐾 ∩ 𝐿 ) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ ( vol* ‘ 𝐾 ) ∈ ℝ ) → ( vol* ‘ ( 𝐾 ∩ 𝐿 ) ) ∈ ℝ )
39 37 26 34 38 mp3an2i ⊢ ( 𝜑 → ( vol* ‘ ( 𝐾 ∩ 𝐿 ) ) ∈ ℝ )
40 ssun2 ⊢ ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ⊆ ( ( 𝐾 ∩ 𝐿 ) ∪ ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
41 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
42 14 peano2nnd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ )
43 42 41 eleqtrdi ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
44 uzsplit ⊢ ( ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 1 ) → ( ℤ≥ ‘ 1 ) = ( ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
45 43 44 syl ⊢ ( 𝜑 → ( ℤ≥ ‘ 1 ) = ( ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
46 41 45 eqtrid ⊢ ( 𝜑 → ℕ = ( ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
47 14 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
48 ax-1cn ⊢ 1 ∈ ℂ
49 pncan ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
50 47 48 49 sylancl ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
51 50 oveq2d ⊢ ( 𝜑 → ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) = ( 1 ... 𝑁 ) )
52 51 uneq1d ⊢ ( 𝜑 → ( ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = ( ( 1 ... 𝑁 ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
53 46 52 eqtrd ⊢ ( 𝜑 → ℕ = ( ( 1 ... 𝑁 ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
54 53 iuneq1d ⊢ ( 𝜑 → ∪ 𝑖 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) = ∪ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) )
55 iunxun ⊢ ∪ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) = ( ∪ 𝑖 ∈ ( 1 ... 𝑁 ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∪ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) )
56 54 55 eqtrdi ⊢ ( 𝜑 → ∪ 𝑖 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) = ( ∪ 𝑖 ∈ ( 1 ... 𝑁 ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∪ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ) )
57 ioof ⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
58 inss2 ⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
59 rexpssxrxp ⊢ ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* )
60 58 59 sstri ⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ* × ℝ* )
61 fss ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ* × ℝ* ) ) → 𝐹 : ℕ ⟶ ( ℝ* × ℝ* ) )
62 1 60 61 sylancl ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ℝ* × ℝ* ) )
63 fco ⊢ ( ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ ∧ 𝐹 : ℕ ⟶ ( ℝ* × ℝ* ) ) → ( (,) ∘ 𝐹 ) : ℕ ⟶ 𝒫 ℝ )
64 57 62 63 sylancr ⊢ ( 𝜑 → ( (,) ∘ 𝐹 ) : ℕ ⟶ 𝒫 ℝ )
65 ffn ⊢ ( ( (,) ∘ 𝐹 ) : ℕ ⟶ 𝒫 ℝ → ( (,) ∘ 𝐹 ) Fn ℕ )
66 fniunfv ⊢ ( ( (,) ∘ 𝐹 ) Fn ℕ → ∪ 𝑖 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑖 ) = ∪ ran ( (,) ∘ 𝐹 ) )
67 64 65 66 3syl ⊢ ( 𝜑 → ∪ 𝑖 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑖 ) = ∪ ran ( (,) ∘ 𝐹 ) )
68 fvco3 ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑖 ∈ ℕ ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑖 ) = ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) )
69 1 68 sylan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑖 ) = ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) )
70 69 iuneq2dv ⊢ ( 𝜑 → ∪ 𝑖 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑖 ) = ∪ 𝑖 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) )
71 67 70 eqtr3d ⊢ ( 𝜑 → ∪ ran ( (,) ∘ 𝐹 ) = ∪ 𝑖 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) )
72 4 71 eqtrid ⊢ ( 𝜑 → 𝐴 = ∪ 𝑖 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) )
73 ffun ⊢ ( ( (,) ∘ 𝐹 ) : ℕ ⟶ 𝒫 ℝ → Fun ( (,) ∘ 𝐹 ) )
74 funiunfv ⊢ ( Fun ( (,) ∘ 𝐹 ) → ∪ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑖 ) = ∪ ( ( (,) ∘ 𝐹 ) “ ( 1 ... 𝑁 ) ) )
75 64 73 74 3syl ⊢ ( 𝜑 → ∪ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑖 ) = ∪ ( ( (,) ∘ 𝐹 ) “ ( 1 ... 𝑁 ) ) )
76 elfznn ⊢ ( 𝑖 ∈ ( 1 ... 𝑁 ) → 𝑖 ∈ ℕ )
77 1 76 68 syl2an ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑖 ) = ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) )
78 77 iuneq2dv ⊢ ( 𝜑 → ∪ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑖 ) = ∪ 𝑖 ∈ ( 1 ... 𝑁 ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) )
79 75 78 eqtr3d ⊢ ( 𝜑 → ∪ ( ( (,) ∘ 𝐹 ) “ ( 1 ... 𝑁 ) ) = ∪ 𝑖 ∈ ( 1 ... 𝑁 ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) )
80 16 79 eqtrid ⊢ ( 𝜑 → 𝐿 = ∪ 𝑖 ∈ ( 1 ... 𝑁 ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) )
81 80 uneq1d ⊢ ( 𝜑 → ( 𝐿 ∪ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ) = ( ∪ 𝑖 ∈ ( 1 ... 𝑁 ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∪ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ) )
82 56 72 81 3eqtr4d ⊢ ( 𝜑 → 𝐴 = ( 𝐿 ∪ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ) )
83 82 ineq2d ⊢ ( 𝜑 → ( 𝐾 ∩ 𝐴 ) = ( 𝐾 ∩ ( 𝐿 ∪ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) )
84 indi ⊢ ( 𝐾 ∩ ( 𝐿 ∪ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) = ( ( 𝐾 ∩ 𝐿 ) ∪ ( 𝐾 ∩ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ) )
85 83 84 eqtrdi ⊢ ( 𝜑 → ( 𝐾 ∩ 𝐴 ) = ( ( 𝐾 ∩ 𝐿 ) ∪ ( 𝐾 ∩ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) )
86 fss ⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ* × ℝ* ) ) → 𝐺 : ℕ ⟶ ( ℝ* × ℝ* ) )
87 7 60 86 sylancl ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ℝ* × ℝ* ) )
88 fco ⊢ ( ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ ∧ 𝐺 : ℕ ⟶ ( ℝ* × ℝ* ) ) → ( (,) ∘ 𝐺 ) : ℕ ⟶ 𝒫 ℝ )
89 57 87 88 sylancr ⊢ ( 𝜑 → ( (,) ∘ 𝐺 ) : ℕ ⟶ 𝒫 ℝ )
90 ffun ⊢ ( ( (,) ∘ 𝐺 ) : ℕ ⟶ 𝒫 ℝ → Fun ( (,) ∘ 𝐺 ) )
91 funiunfv ⊢ ( Fun ( (,) ∘ 𝐺 ) → ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( (,) ∘ 𝐺 ) ‘ 𝑗 ) = ∪ ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) ) )
92 89 90 91 3syl ⊢ ( 𝜑 → ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( (,) ∘ 𝐺 ) ‘ 𝑗 ) = ∪ ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) ) )
93 elfznn ⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ℕ )
94 fvco3 ⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑗 ∈ ℕ ) → ( ( (,) ∘ 𝐺 ) ‘ 𝑗 ) = ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) )
95 7 93 94 syl2an ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( (,) ∘ 𝐺 ) ‘ 𝑗 ) = ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) )
96 95 iuneq2dv ⊢ ( 𝜑 → ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( (,) ∘ 𝐺 ) ‘ 𝑗 ) = ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) )
97 92 96 eqtr3d ⊢ ( 𝜑 → ∪ ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) ) = ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) )
98 13 97 eqtrid ⊢ ( 𝜑 → 𝐾 = ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) )
99 98 ineq2d ⊢ ( 𝜑 → ( ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ 𝐾 ) = ( ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
100 incom ⊢ ( 𝐾 ∩ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ) = ( ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ 𝐾 )
101 iunin2 ⊢ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ) = ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) )
102 incom ⊢ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) )
103 102 a1i ⊢ ( 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) → ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ) )
104 103 iuneq2i ⊢ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) )
105 incom ⊢ ( ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) )
106 101 104 105 3eqtr4ri ⊢ ( ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) )
107 106 a1i ⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → ( ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
108 107 iuneq2i ⊢ ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) )
109 iunin2 ⊢ ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) )
110 108 109 eqtr3i ⊢ ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) )
111 99 100 110 3eqtr4g ⊢ ( 𝜑 → ( 𝐾 ∩ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ) = ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
112 111 uneq2d ⊢ ( 𝜑 → ( ( 𝐾 ∩ 𝐿 ) ∪ ( 𝐾 ∩ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) = ( ( 𝐾 ∩ 𝐿 ) ∪ ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) )
113 85 112 eqtrd ⊢ ( 𝜑 → ( 𝐾 ∩ 𝐴 ) = ( ( 𝐾 ∩ 𝐿 ) ∪ ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) )
114 40 113 sseqtrrid ⊢ ( 𝜑 → ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ⊆ ( 𝐾 ∩ 𝐴 ) )
115 114 17 sstrdi ⊢ ( 𝜑 → ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ⊆ 𝐾 )
116 ovolsscl ⊢ ( ( ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ ( vol* ‘ 𝐾 ) ∈ ℝ ) → ( vol* ‘ ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ∈ ℝ )
117 115 26 34 116 syl3anc ⊢ ( 𝜑 → ( vol* ‘ ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ∈ ℝ )
118 39 117 readdcld ⊢ ( 𝜑 → ( ( vol* ‘ ( 𝐾 ∩ 𝐿 ) ) + ( vol* ‘ ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ) ∈ ℝ )
119 6 rpred ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
120 39 119 readdcld ⊢ ( 𝜑 → ( ( vol* ‘ ( 𝐾 ∩ 𝐿 ) ) + 𝐶 ) ∈ ℝ )
121 113 fveq2d ⊢ ( 𝜑 → ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) = ( vol* ‘ ( ( 𝐾 ∩ 𝐿 ) ∪ ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ) )
122 37 26 sstrid ⊢ ( 𝜑 → ( 𝐾 ∩ 𝐿 ) ⊆ ℝ )
123 115 26 sstrd ⊢ ( 𝜑 → ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ⊆ ℝ )
124 ovolun ⊢ ( ( ( ( 𝐾 ∩ 𝐿 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝐾 ∩ 𝐿 ) ) ∈ ℝ ) ∧ ( ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ⊆ ℝ ∧ ( vol* ‘ ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ∈ ℝ ) ) → ( vol* ‘ ( ( 𝐾 ∩ 𝐿 ) ∪ ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ) ≤ ( ( vol* ‘ ( 𝐾 ∩ 𝐿 ) ) + ( vol* ‘ ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ) )
125 122 39 123 117 124 syl22anc ⊢ ( 𝜑 → ( vol* ‘ ( ( 𝐾 ∩ 𝐿 ) ∪ ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ) ≤ ( ( vol* ‘ ( 𝐾 ∩ 𝐿 ) ) + ( vol* ‘ ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ) )
126 121 125 eqbrtrd ⊢ ( 𝜑 → ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) ≤ ( ( vol* ‘ ( 𝐾 ∩ 𝐿 ) ) + ( vol* ‘ ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ) )
127 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑀 ) ∈ Fin )
128 iunss ⊢ ( ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ⊆ 𝐾 ↔ ∀ 𝑗 ∈ ( 1 ... 𝑀 ) ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ⊆ 𝐾 )
129 115 128 sylib ⊢ ( 𝜑 → ∀ 𝑗 ∈ ( 1 ... 𝑀 ) ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ⊆ 𝐾 )
130 129 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ⊆ 𝐾 )
131 26 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝐾 ⊆ ℝ )
132 34 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( vol* ‘ 𝐾 ) ∈ ℝ )
133 ovolsscl ⊢ ( ( ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ ( vol* ‘ 𝐾 ) ∈ ℝ ) → ( vol* ‘ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ∈ ℝ )
134 130 131 132 133 syl3anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( vol* ‘ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ∈ ℝ )
135 127 134 fsumrecl ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( vol* ‘ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ∈ ℝ )
136 130 131 sstrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ⊆ ℝ )
137 136 134 jca ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ⊆ ℝ ∧ ( vol* ‘ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ∈ ℝ ) )
138 137 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ ( 1 ... 𝑀 ) ( ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ⊆ ℝ ∧ ( vol* ‘ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ∈ ℝ ) )
139 ovolfiniun ⊢ ( ( ( 1 ... 𝑀 ) ∈ Fin ∧ ∀ 𝑗 ∈ ( 1 ... 𝑀 ) ( ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ⊆ ℝ ∧ ( vol* ‘ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ∈ ℝ ) ) → ( vol* ‘ ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ≤ Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( vol* ‘ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) )
140 127 138 139 syl2anc ⊢ ( 𝜑 → ( vol* ‘ ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ≤ Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( vol* ‘ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) )
141 119 11 nndivred ⊢ ( 𝜑 → ( 𝐶 / 𝑀 ) ∈ ℝ )
142 141 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝐶 / 𝑀 ) ∈ ℝ )
143 80 ineq2d ⊢ ( 𝜑 → ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) = ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ ∪ 𝑖 ∈ ( 1 ... 𝑁 ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ) )
144 143 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) = ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ ∪ 𝑖 ∈ ( 1 ... 𝑁 ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ) )
145 102 a1i ⊢ ( 𝑖 ∈ ( 1 ... 𝑁 ) → ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ) )
146 145 iuneq2i ⊢ ∪ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ∪ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) )
147 iunin2 ⊢ ∪ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ) = ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ ∪ 𝑖 ∈ ( 1 ... 𝑁 ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) )
148 146 147 eqtri ⊢ ∪ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ ∪ 𝑖 ∈ ( 1 ... 𝑁 ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) )
149 144 148 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) = ∪ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
150 fzfid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 1 ... 𝑁 ) ∈ Fin )
151 ffvelcdm ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑖 ∈ ℕ ) → ( 𝐹 ‘ 𝑖 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
152 1 76 151 syl2an ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑖 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
153 152 elin2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑖 ) ∈ ( ℝ × ℝ ) )
154 1st2nd2 ⊢ ( ( 𝐹 ‘ 𝑖 ) ∈ ( ℝ × ℝ ) → ( 𝐹 ‘ 𝑖 ) = ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑖 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑖 ) ) ⟩ )
155 153 154 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑖 ) = ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑖 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑖 ) ) ⟩ )
156 155 fveq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑖 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑖 ) ) ⟩ ) )
157 df-ov ⊢ ( ( 1st ‘ ( 𝐹 ‘ 𝑖 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑖 ) ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑖 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑖 ) ) ⟩ )
158 156 157 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) = ( ( 1st ‘ ( 𝐹 ‘ 𝑖 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑖 ) ) ) )
159 ioombl ⊢ ( ( 1st ‘ ( 𝐹 ‘ 𝑖 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑖 ) ) ) ∈ dom vol
160 158 159 eqeltrdi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∈ dom vol )
161 160 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∈ dom vol )
162 ffvelcdm ⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑗 ∈ ℕ ) → ( 𝐺 ‘ 𝑗 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
163 7 93 162 syl2an ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ 𝑗 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
164 163 elin2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ 𝑗 ) ∈ ( ℝ × ℝ ) )
165 1st2nd2 ⊢ ( ( 𝐺 ‘ 𝑗 ) ∈ ( ℝ × ℝ ) → ( 𝐺 ‘ 𝑗 ) = ⟨ ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ⟩ )
166 164 165 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ 𝑗 ) = ⟨ ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ⟩ )
167 166 fveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ⟩ ) )
168 df-ov ⊢ ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ⟩ )
169 167 168 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) = ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
170 ioombl ⊢ ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ dom vol
171 169 170 eqeltrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ dom vol )
172 171 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ dom vol )
173 inmbl ⊢ ( ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∈ dom vol ∧ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ dom vol ) → ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ dom vol )
174 161 172 173 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ dom vol )
175 174 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ dom vol )
176 finiunmbl ⊢ ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ dom vol ) → ∪ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ dom vol )
177 150 175 176 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ∪ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ dom vol )
178 149 177 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) ∈ dom vol )
179 inss2 ⊢ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ⊆ 𝐴
180 1 uniiccdif ⊢ ( 𝜑 → ( ∪ ran ( (,) ∘ 𝐹 ) ⊆ ∪ ran ( [,] ∘ 𝐹 ) ∧ ( vol* ‘ ( ∪ ran ( [,] ∘ 𝐹 ) ∖ ∪ ran ( (,) ∘ 𝐹 ) ) ) = 0 ) )
181 180 simpld ⊢ ( 𝜑 → ∪ ran ( (,) ∘ 𝐹 ) ⊆ ∪ ran ( [,] ∘ 𝐹 ) )
182 ovolficcss ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ∪ ran ( [,] ∘ 𝐹 ) ⊆ ℝ )
183 1 182 syl ⊢ ( 𝜑 → ∪ ran ( [,] ∘ 𝐹 ) ⊆ ℝ )
184 181 183 sstrd ⊢ ( 𝜑 → ∪ ran ( (,) ∘ 𝐹 ) ⊆ ℝ )
185 4 184 eqsstrid ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
186 185 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝐴 ⊆ ℝ )
187 179 186 sstrid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ⊆ ℝ )
188 inss1 ⊢ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ⊆ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) )
189 ioossre ⊢ ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) ⊆ ℝ
190 169 189 eqsstrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ⊆ ℝ )
191 169 fveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( vol* ‘ ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) )
192 ovolfcl ⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑗 ∈ ℕ ) → ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
193 7 93 192 syl2an ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
194 ovolioo ⊢ ( ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) → ( vol* ‘ ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) = ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
195 193 194 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( vol* ‘ ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) = ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
196 191 195 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
197 193 simp2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ )
198 193 simp1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ )
199 197 198 resubcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℝ )
200 196 199 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℝ )
201 ovolsscl ⊢ ( ( ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ⊆ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∧ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ⊆ ℝ ∧ ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℝ ) → ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ∈ ℝ )
202 188 190 200 201 mp3an2i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ∈ ℝ )
203 mblsplit ⊢ ( ( ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) ∈ dom vol ∧ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ⊆ ℝ ∧ ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ∈ ℝ ) → ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) = ( ( vol* ‘ ( ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ∩ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) ) ) + ( vol* ‘ ( ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ∖ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) ) ) ) )
204 178 187 202 203 syl3anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) = ( ( vol* ‘ ( ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ∩ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) ) ) + ( vol* ‘ ( ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ∖ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) ) ) ) )
205 imassrn ⊢ ( ( (,) ∘ 𝐹 ) “ ( 1 ... 𝑁 ) ) ⊆ ran ( (,) ∘ 𝐹 )
206 205 unissi ⊢ ∪ ( ( (,) ∘ 𝐹 ) “ ( 1 ... 𝑁 ) ) ⊆ ∪ ran ( (,) ∘ 𝐹 )
207 206 16 4 3sstr4i ⊢ 𝐿 ⊆ 𝐴
208 sslin ⊢ ( 𝐿 ⊆ 𝐴 → ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) ⊆ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) )
209 207 208 mp1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) ⊆ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) )
210 sseqin2 ⊢ ( ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) ⊆ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ↔ ( ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ∩ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) ) = ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) )
211 209 210 sylib ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ∩ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) ) = ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) )
212 211 fveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( vol* ‘ ( ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ∩ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) ) ) = ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) ) )
213 indifdir ⊢ ( ( 𝐴 ∖ 𝐿 ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( ( 𝐴 ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∖ ( 𝐿 ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
214 incom ⊢ ( 𝐴 ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 )
215 incom ⊢ ( 𝐿 ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 )
216 214 215 difeq12i ⊢ ( ( 𝐴 ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∖ ( 𝐿 ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) = ( ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ∖ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) )
217 213 216 eqtri ⊢ ( ( 𝐴 ∖ 𝐿 ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ∖ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) )
218 82 eqcomd ⊢ ( 𝜑 → ( 𝐿 ∪ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ) = 𝐴 )
219 80 ineq1d ⊢ ( 𝜑 → ( 𝐿 ∩ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ) = ( ∪ 𝑖 ∈ ( 1 ... 𝑁 ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ) )
220 2fveq3 ⊢ ( 𝑥 = 𝑖 → ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) = ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) )
221 220 cbvdisjv ⊢ ( Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) ↔ Disj 𝑖 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) )
222 2 221 sylib ⊢ ( 𝜑 → Disj 𝑖 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) )
223 fz1ssnn ⊢ ( 1 ... 𝑁 ) ⊆ ℕ
224 223 a1i ⊢ ( 𝜑 → ( 1 ... 𝑁 ) ⊆ ℕ )
225 uzss ⊢ ( ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 1 ) → ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ⊆ ( ℤ≥ ‘ 1 ) )
226 43 225 syl ⊢ ( 𝜑 → ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ⊆ ( ℤ≥ ‘ 1 ) )
227 226 41 sseqtrrdi ⊢ ( 𝜑 → ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ⊆ ℕ )
228 51 ineq1d ⊢ ( 𝜑 → ( ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = ( ( 1 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
229 uzdisj ⊢ ( ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = ∅
230 228 229 eqtr3di ⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = ∅ )
231 disjiun ⊢ ( ( Disj 𝑖 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∧ ( ( 1 ... 𝑁 ) ⊆ ℕ ∧ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ⊆ ℕ ∧ ( ( 1 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = ∅ ) ) → ( ∪ 𝑖 ∈ ( 1 ... 𝑁 ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ) = ∅ )
232 222 224 227 230 231 syl13anc ⊢ ( 𝜑 → ( ∪ 𝑖 ∈ ( 1 ... 𝑁 ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ) = ∅ )
233 219 232 eqtrd ⊢ ( 𝜑 → ( 𝐿 ∩ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ) = ∅ )
234 uneqdifeq ⊢ ( ( 𝐿 ⊆ 𝐴 ∧ ( 𝐿 ∩ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ) = ∅ ) → ( ( 𝐿 ∪ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ) = 𝐴 ↔ ( 𝐴 ∖ 𝐿 ) = ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ) )
235 207 233 234 sylancr ⊢ ( 𝜑 → ( ( 𝐿 ∪ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ) = 𝐴 ↔ ( 𝐴 ∖ 𝐿 ) = ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ) )
236 218 235 mpbid ⊢ ( 𝜑 → ( 𝐴 ∖ 𝐿 ) = ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) )
237 236 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝐴 ∖ 𝐿 ) = ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) )
238 237 ineq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ ( 𝐴 ∖ 𝐿 ) ) = ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ) )
239 incom ⊢ ( ( 𝐴 ∖ 𝐿 ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ ( 𝐴 ∖ 𝐿 ) )
240 104 101 eqtri ⊢ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) )
241 238 239 240 3eqtr4g ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐴 ∖ 𝐿 ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
242 217 241 eqtr3id ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ∖ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) ) = ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
243 242 fveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( vol* ‘ ( ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ∖ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) ) ) = ( vol* ‘ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) )
244 212 243 oveq12d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( vol* ‘ ( ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ∩ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) ) ) + ( vol* ‘ ( ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ∖ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) ) ) ) = ( ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) ) + ( vol* ‘ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ) )
245 204 244 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) = ( ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) ) + ( vol* ‘ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ) )
246 202 142 resubcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) − ( 𝐶 / 𝑀 ) ) ∈ ℝ )
247 inss2 ⊢ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ⊆ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) )
248 190 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ⊆ ℝ )
249 200 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℝ )
250 ovolsscl ⊢ ( ( ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ⊆ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∧ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ⊆ ℝ ∧ ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℝ ) → ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ∈ ℝ )
251 247 248 249 250 mp3an2i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ∈ ℝ )
252 150 251 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ∈ ℝ )
253 15 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑀 ) )
254 252 202 142 absdifltd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑀 ) ↔ ( ( ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) − ( 𝐶 / 𝑀 ) ) < Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) < ( ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) + ( 𝐶 / 𝑀 ) ) ) ) )
255 253 254 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) − ( 𝐶 / 𝑀 ) ) < Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) < ( ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) + ( 𝐶 / 𝑀 ) ) ) )
256 255 simpld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) − ( 𝐶 / 𝑀 ) ) < Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) )
257 246 252 256 ltled ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) − ( 𝐶 / 𝑀 ) ) ≤ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) )
258 149 fveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) ) = ( vol* ‘ ∪ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) )
259 mblvol ⊢ ( ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ dom vol → ( vol ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) = ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) )
260 174 259 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( vol ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) = ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) )
261 260 251 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( vol ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ∈ ℝ )
262 174 261 jca ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ dom vol ∧ ( vol ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ∈ ℝ ) )
263 262 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ dom vol ∧ ( vol ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ∈ ℝ ) )
264 inss1 ⊢ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ⊆ ( (,) ‘ ( 𝐹 ‘ 𝑖 ) )
265 264 rgenw ⊢ ∀ 𝑖 ∈ ℕ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ⊆ ( (,) ‘ ( 𝐹 ‘ 𝑖 ) )
266 222 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → Disj 𝑖 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) )
267 disjss2 ⊢ ( ∀ 𝑖 ∈ ℕ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ⊆ ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) → ( Disj 𝑖 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) → Disj 𝑖 ∈ ℕ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) )
268 265 266 267 mpsyl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → Disj 𝑖 ∈ ℕ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
269 disjss1 ⊢ ( ( 1 ... 𝑁 ) ⊆ ℕ → ( Disj 𝑖 ∈ ℕ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) → Disj 𝑖 ∈ ( 1 ... 𝑁 ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) )
270 223 268 269 mpsyl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → Disj 𝑖 ∈ ( 1 ... 𝑁 ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
271 volfiniun ⊢ ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ dom vol ∧ ( vol ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ∈ ℝ ) ∧ Disj 𝑖 ∈ ( 1 ... 𝑁 ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) → ( vol ‘ ∪ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( vol ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) )
272 150 263 270 271 syl3anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( vol ‘ ∪ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( vol ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) )
273 mblvol ⊢ ( ∪ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ dom vol → ( vol ‘ ∪ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) = ( vol* ‘ ∪ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) )
274 177 273 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( vol ‘ ∪ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) = ( vol* ‘ ∪ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) )
275 260 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( vol ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) )
276 272 274 275 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( vol* ‘ ∪ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) )
277 258 276 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) )
278 257 277 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) − ( 𝐶 / 𝑀 ) ) ≤ ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) ) )
279 277 252 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) ) ∈ ℝ )
280 202 142 279 lesubaddd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) − ( 𝐶 / 𝑀 ) ) ≤ ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) ) ↔ ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ≤ ( ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) ) + ( 𝐶 / 𝑀 ) ) ) )
281 278 280 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ≤ ( ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) ) + ( 𝐶 / 𝑀 ) ) )
282 245 281 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) ) + ( vol* ‘ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ) ≤ ( ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) ) + ( 𝐶 / 𝑀 ) ) )
283 134 142 279 leadd2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( vol* ‘ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ≤ ( 𝐶 / 𝑀 ) ↔ ( ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) ) + ( vol* ‘ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ) ≤ ( ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐿 ) ) + ( 𝐶 / 𝑀 ) ) ) )
284 282 283 mpbird ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( vol* ‘ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ≤ ( 𝐶 / 𝑀 ) )
285 127 134 142 284 fsumle ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( vol* ‘ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ≤ Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( 𝐶 / 𝑀 ) )
286 141 recnd ⊢ ( 𝜑 → ( 𝐶 / 𝑀 ) ∈ ℂ )
287 fsumconst ⊢ ( ( ( 1 ... 𝑀 ) ∈ Fin ∧ ( 𝐶 / 𝑀 ) ∈ ℂ ) → Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( 𝐶 / 𝑀 ) = ( ( ♯ ‘ ( 1 ... 𝑀 ) ) · ( 𝐶 / 𝑀 ) ) )
288 127 286 287 syl2anc ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( 𝐶 / 𝑀 ) = ( ( ♯ ‘ ( 1 ... 𝑀 ) ) · ( 𝐶 / 𝑀 ) ) )
289 nnnn0 ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℕ0 )
290 hashfz1 ⊢ ( 𝑀 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑀 ) ) = 𝑀 )
291 11 289 290 3syl ⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... 𝑀 ) ) = 𝑀 )
292 291 oveq1d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 1 ... 𝑀 ) ) · ( 𝐶 / 𝑀 ) ) = ( 𝑀 · ( 𝐶 / 𝑀 ) ) )
293 119 recnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
294 11 nncnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
295 11 nnne0d ⊢ ( 𝜑 → 𝑀 ≠ 0 )
296 293 294 295 divcan2d ⊢ ( 𝜑 → ( 𝑀 · ( 𝐶 / 𝑀 ) ) = 𝐶 )
297 288 292 296 3eqtrd ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( 𝐶 / 𝑀 ) = 𝐶 )
298 285 297 breqtrd ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( vol* ‘ ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ≤ 𝐶 )
299 117 135 119 140 298 letrd ⊢ ( 𝜑 → ( vol* ‘ ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ≤ 𝐶 )
300 117 119 39 299 leadd2dd ⊢ ( 𝜑 → ( ( vol* ‘ ( 𝐾 ∩ 𝐿 ) ) + ( vol* ‘ ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ∪ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ) ≤ ( ( vol* ‘ ( 𝐾 ∩ 𝐿 ) ) + 𝐶 ) )
301 36 118 120 126 300 letrd ⊢ ( 𝜑 → ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) ≤ ( ( vol* ‘ ( 𝐾 ∩ 𝐿 ) ) + 𝐶 ) )