Metamath Proof Explorer

Theorem uniioombllem6

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* ‘ 𝐸 ) + 𝐶 ) )
Assertion uniioombllem6 ( 𝜑 → ( ( vol* ‘ ( 𝐸 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐸 ∖ 𝐴 ) ) ) ≤ ( ( vol* ‘ 𝐸 ) + ( 4 · 𝐶 ) ) )

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 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
12 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
13 eqidd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑇 ‘ 𝑚 ) = ( 𝑇 ‘ 𝑚 ) )
14 eqidd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑎 ) = ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑎 ) )
15 eqid ⊢ ( ( abs ∘ − ) ∘ 𝐺 ) = ( ( abs ∘ − ) ∘ 𝐺 )
16 15 ovolfsf ⊢ ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( ( abs ∘ − ) ∘ 𝐺 ) : ℕ ⟶ ( 0 [,) +∞ ) )
17 7 16 syl ⊢ ( 𝜑 → ( ( abs ∘ − ) ∘ 𝐺 ) : ℕ ⟶ ( 0 [,) +∞ ) )
18 17 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑎 ) ∈ ( 0 [,) +∞ ) )
19 elrege0 ⊢ ( ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑎 ) ∈ ( 0 [,) +∞ ) ↔ ( ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑎 ) ∈ ℝ ∧ 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑎 ) ) )
20 18 19 sylib ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) → ( ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑎 ) ∈ ℝ ∧ 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑎 ) ) )
21 20 simpld ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑎 ) ∈ ℝ )
22 20 simprd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) → 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑎 ) )
23 1 2 3 4 5 6 7 8 9 10 uniioombllem1 ⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ )
24 15 9 ovolsf ⊢ ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝑇 : ℕ ⟶ ( 0 [,) +∞ ) )
25 7 24 syl ⊢ ( 𝜑 → 𝑇 : ℕ ⟶ ( 0 [,) +∞ ) )
26 25 frnd ⊢ ( 𝜑 → ran 𝑇 ⊆ ( 0 [,) +∞ ) )
27 icossxr ⊢ ( 0 [,) +∞ ) ⊆ ℝ*
28 26 27 sstrdi ⊢ ( 𝜑 → ran 𝑇 ⊆ ℝ* )
29 supxrub ⊢ ( ( ran 𝑇 ⊆ ℝ* ∧ 𝑥 ∈ ran 𝑇 ) → 𝑥 ≤ sup ( ran 𝑇 , ℝ* , < ) )
30 28 29 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran 𝑇 ) → 𝑥 ≤ sup ( ran 𝑇 , ℝ* , < ) )
31 30 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ran 𝑇 𝑥 ≤ sup ( ran 𝑇 , ℝ* , < ) )
32 25 ffnd ⊢ ( 𝜑 → 𝑇 Fn ℕ )
33 breq1 ⊢ ( 𝑥 = ( 𝑇 ‘ 𝑚 ) → ( 𝑥 ≤ sup ( ran 𝑇 , ℝ* , < ) ↔ ( 𝑇 ‘ 𝑚 ) ≤ sup ( ran 𝑇 , ℝ* , < ) ) )
34 33 ralrn ⊢ ( 𝑇 Fn ℕ → ( ∀ 𝑥 ∈ ran 𝑇 𝑥 ≤ sup ( ran 𝑇 , ℝ* , < ) ↔ ∀ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ≤ sup ( ran 𝑇 , ℝ* , < ) ) )
35 32 34 syl ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ran 𝑇 𝑥 ≤ sup ( ran 𝑇 , ℝ* , < ) ↔ ∀ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ≤ sup ( ran 𝑇 , ℝ* , < ) ) )
36 31 35 mpbid ⊢ ( 𝜑 → ∀ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ≤ sup ( ran 𝑇 , ℝ* , < ) )
37 brralrspcev ⊢ ( ( sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ ∧ ∀ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ≤ sup ( ran 𝑇 , ℝ* , < ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ≤ 𝑥 )
38 23 36 37 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ≤ 𝑥 )
39 11 9 12 14 21 22 38 isumsup2 ⊢ ( 𝜑 → 𝑇 ⇝ sup ( ran 𝑇 , ℝ , < ) )
40 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
41 26 40 sstrdi ⊢ ( 𝜑 → ran 𝑇 ⊆ ℝ )
42 1nn ⊢ 1 ∈ ℕ
43 25 fdmd ⊢ ( 𝜑 → dom 𝑇 = ℕ )
44 42 43 eleqtrrid ⊢ ( 𝜑 → 1 ∈ dom 𝑇 )
45 44 ne0d ⊢ ( 𝜑 → dom 𝑇 ≠ ∅ )
46 dm0rn0 ⊢ ( dom 𝑇 = ∅ ↔ ran 𝑇 = ∅ )
47 46 necon3bii ⊢ ( dom 𝑇 ≠ ∅ ↔ ran 𝑇 ≠ ∅ )
48 45 47 sylib ⊢ ( 𝜑 → ran 𝑇 ≠ ∅ )
49 brralrspcev ⊢ ( ( sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ ∧ ∀ 𝑥 ∈ ran 𝑇 𝑥 ≤ sup ( ran 𝑇 , ℝ* , < ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ ran 𝑇 𝑥 ≤ 𝑦 )
50 23 31 49 syl2anc ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ ran 𝑇 𝑥 ≤ 𝑦 )
51 supxrre ⊢ ( ( ran 𝑇 ⊆ ℝ ∧ ran 𝑇 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ ran 𝑇 𝑥 ≤ 𝑦 ) → sup ( ran 𝑇 , ℝ* , < ) = sup ( ran 𝑇 , ℝ , < ) )
52 41 48 50 51 syl3anc ⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) = sup ( ran 𝑇 , ℝ , < ) )
53 39 52 breqtrrd ⊢ ( 𝜑 → 𝑇 ⇝ sup ( ran 𝑇 , ℝ* , < ) )
54 11 12 6 13 53 climi2 ⊢ ( 𝜑 → ∃ 𝑗 ∈ ℕ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 )
55 11 r19.2uz ⊢ ( ∃ 𝑗 ∈ ℕ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 → ∃ 𝑚 ∈ ℕ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 )
56 54 55 syl ⊢ ( 𝜑 → ∃ 𝑚 ∈ ℕ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 )
57 1zzd ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) → 1 ∈ ℤ )
58 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) → 𝐶 ∈ ℝ+ )
59 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) → 𝑚 ∈ ℕ )
60 59 nnrpd ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) → 𝑚 ∈ ℝ+ )
61 58 60 rpdivcld ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) → ( 𝐶 / 𝑚 ) ∈ ℝ+ )
62 fvex ⊢ ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ V
63 62 inex1 ⊢ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ V
64 63 rgenw ⊢ ∀ 𝑧 ∈ ℕ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ V
65 eqid ⊢ ( 𝑧 ∈ ℕ ↦ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) = ( 𝑧 ∈ ℕ ↦ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
66 65 fnmpt ⊢ ( ∀ 𝑧 ∈ ℕ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ V → ( 𝑧 ∈ ℕ ↦ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) Fn ℕ )
67 64 66 mp1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑧 ∈ ℕ ↦ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) Fn ℕ )
68 elfznn ⊢ ( 𝑖 ∈ ( 1 ... 𝑛 ) → 𝑖 ∈ ℕ )
69 fvco2 ⊢ ( ( ( 𝑧 ∈ ℕ ↦ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) Fn ℕ ∧ 𝑖 ∈ ℕ ) → ( ( vol* ∘ ( 𝑧 ∈ ℕ ↦ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ) ‘ 𝑖 ) = ( vol* ‘ ( ( 𝑧 ∈ ℕ ↦ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ‘ 𝑖 ) ) )
70 67 68 69 syl2an ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ... 𝑛 ) ) → ( ( vol* ∘ ( 𝑧 ∈ ℕ ↦ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ) ‘ 𝑖 ) = ( vol* ‘ ( ( 𝑧 ∈ ℕ ↦ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ‘ 𝑖 ) ) )
71 68 adantl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ... 𝑛 ) ) → 𝑖 ∈ ℕ )
72 2fveq3 ⊢ ( 𝑧 = 𝑖 → ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) = ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) )
73 72 ineq1d ⊢ ( 𝑧 = 𝑖 → ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
74 fvex ⊢ ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∈ V
75 74 inex1 ⊢ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ V
76 73 65 75 fvmpt ⊢ ( 𝑖 ∈ ℕ → ( ( 𝑧 ∈ ℕ ↦ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ‘ 𝑖 ) = ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
77 71 76 syl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ... 𝑛 ) ) → ( ( 𝑧 ∈ ℕ ↦ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ‘ 𝑖 ) = ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
78 77 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ... 𝑛 ) ) → ( vol* ‘ ( ( 𝑧 ∈ ℕ ↦ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ‘ 𝑖 ) ) = ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) )
79 70 78 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ... 𝑛 ) ) → ( ( vol* ∘ ( 𝑧 ∈ ℕ ↦ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ) ‘ 𝑖 ) = ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) )
80 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
81 80 11 eleqtrdi ⊢ ( ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ( ℤ≥ ‘ 1 ) )
82 inss2 ⊢ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ⊆ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) )
83 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
84 elfznn ⊢ ( 𝑗 ∈ ( 1 ... 𝑚 ) → 𝑗 ∈ ℕ )
85 ffvelcdm ⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑗 ∈ ℕ ) → ( 𝐺 ‘ 𝑗 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
86 83 84 85 syl2an ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) → ( 𝐺 ‘ 𝑗 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
87 86 elin2d ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) → ( 𝐺 ‘ 𝑗 ) ∈ ( ℝ × ℝ ) )
88 1st2nd2 ⊢ ( ( 𝐺 ‘ 𝑗 ) ∈ ( ℝ × ℝ ) → ( 𝐺 ‘ 𝑗 ) = ⟨ ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ⟩ )
89 87 88 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) → ( 𝐺 ‘ 𝑗 ) = ⟨ ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ⟩ )
90 89 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) → ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ⟩ ) )
91 df-ov ⊢ ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ⟩ )
92 90 91 eqtr4di ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) → ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) = ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
93 ioossre ⊢ ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) ⊆ ℝ
94 92 93 eqsstrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) → ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ⊆ ℝ )
95 94 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ... 𝑛 ) ) → ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ⊆ ℝ )
96 92 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) → ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( vol* ‘ ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) )
97 ovolfcl ⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑗 ∈ ℕ ) → ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
98 83 84 97 syl2an ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) → ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
99 ovolioo ⊢ ( ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) → ( vol* ‘ ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) = ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
100 98 99 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) → ( vol* ‘ ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) = ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
101 96 100 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) → ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
102 98 simp2d ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) → ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ )
103 98 simp1d ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) → ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ )
104 102 103 resubcld ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) → ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℝ )
105 101 104 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) → ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℝ )
106 105 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ... 𝑛 ) ) → ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℝ )
107 ovolsscl ⊢ ( ( ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ⊆ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∧ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ⊆ ℝ ∧ ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℝ ) → ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ∈ ℝ )
108 82 95 106 107 mp3an2i ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ... 𝑛 ) ) → ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ∈ ℝ )
109 108 recnd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ... 𝑛 ) ) → ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ∈ ℂ )
110 79 81 109 fsumser ⊢ ( ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) ∧ 𝑛 ∈ ℕ ) → Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) = ( seq 1 ( + , ( vol* ∘ ( 𝑧 ∈ ℕ ↦ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ) ) ‘ 𝑛 ) )
111 110 eqcomd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) ∧ 𝑛 ∈ ℕ ) → ( seq 1 ( + , ( vol* ∘ ( 𝑧 ∈ ℕ ↦ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ) ) ‘ 𝑛 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) )
112 2fveq3 ⊢ ( 𝑧 = 𝑘 → ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) = ( (,) ‘ ( 𝐹 ‘ 𝑘 ) ) )
113 112 ineq1d ⊢ ( 𝑧 = 𝑘 → ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( ( (,) ‘ ( 𝐹 ‘ 𝑘 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
114 113 cbvmptv ⊢ ( 𝑧 ∈ ℕ ↦ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) = ( 𝑘 ∈ ℕ ↦ ( ( (,) ‘ ( 𝐹 ‘ 𝑘 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
115 eqeq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 = ∅ ↔ 𝑥 = ∅ ) )
116 infeq1 ⊢ ( 𝑧 = 𝑥 → inf ( 𝑧 , ℝ* , < ) = inf ( 𝑥 , ℝ* , < ) )
117 supeq1 ⊢ ( 𝑧 = 𝑥 → sup ( 𝑧 , ℝ* , < ) = sup ( 𝑥 , ℝ* , < ) )
118 116 117 opeq12d ⊢ ( 𝑧 = 𝑥 → ⟨ inf ( 𝑧 , ℝ* , < ) , sup ( 𝑧 , ℝ* , < ) ⟩ = ⟨ inf ( 𝑥 , ℝ* , < ) , sup ( 𝑥 , ℝ* , < ) ⟩ )
119 115 118 ifbieq2d ⊢ ( 𝑧 = 𝑥 → if ( 𝑧 = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( 𝑧 , ℝ* , < ) , sup ( 𝑧 , ℝ* , < ) ⟩ ) = if ( 𝑥 = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( 𝑥 , ℝ* , < ) , sup ( 𝑥 , ℝ* , < ) ⟩ ) )
120 119 cbvmptv ⊢ ( 𝑧 ∈ ran (,) ↦ if ( 𝑧 = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( 𝑧 , ℝ* , < ) , sup ( 𝑧 , ℝ* , < ) ⟩ ) ) = ( 𝑥 ∈ ran (,) ↦ if ( 𝑥 = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( 𝑥 , ℝ* , < ) , sup ( 𝑥 , ℝ* , < ) ⟩ ) )
121 1 2 3 4 5 6 7 8 9 10 114 120 uniioombllem2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → seq 1 ( + , ( vol* ∘ ( 𝑧 ∈ ℕ ↦ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ) ) ⇝ ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) )
122 84 121 sylan2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) → seq 1 ( + , ( vol* ∘ ( 𝑧 ∈ ℕ ↦ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ) ) ⇝ ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) )
123 122 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) → seq 1 ( + , ( vol* ∘ ( 𝑧 ∈ ℕ ↦ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ) ) ⇝ ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) )
124 11 57 61 111 123 climi2 ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) → ∃ 𝑎 ∈ ℕ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑎 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) )
125 1z ⊢ 1 ∈ ℤ
126 11 rexuz3 ⊢ ( 1 ∈ ℤ → ( ∃ 𝑎 ∈ ℕ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑎 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) ↔ ∃ 𝑎 ∈ ℤ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑎 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) ) )
127 125 126 ax-mp ⊢ ( ∃ 𝑎 ∈ ℕ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑎 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) ↔ ∃ 𝑎 ∈ ℤ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑎 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) )
128 124 127 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑚 ) ) → ∃ 𝑎 ∈ ℤ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑎 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) )
129 128 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) → ∀ 𝑗 ∈ ( 1 ... 𝑚 ) ∃ 𝑎 ∈ ℤ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑎 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) )
130 fzfi ⊢ ( 1 ... 𝑚 ) ∈ Fin
131 rexfiuz ⊢ ( ( 1 ... 𝑚 ) ∈ Fin → ( ∃ 𝑎 ∈ ℤ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑎 ) ∀ 𝑗 ∈ ( 1 ... 𝑚 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) ↔ ∀ 𝑗 ∈ ( 1 ... 𝑚 ) ∃ 𝑎 ∈ ℤ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑎 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) ) )
132 130 131 ax-mp ⊢ ( ∃ 𝑎 ∈ ℤ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑎 ) ∀ 𝑗 ∈ ( 1 ... 𝑚 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) ↔ ∀ 𝑗 ∈ ( 1 ... 𝑚 ) ∃ 𝑎 ∈ ℤ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑎 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) )
133 129 132 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) → ∃ 𝑎 ∈ ℤ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑎 ) ∀ 𝑗 ∈ ( 1 ... 𝑚 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) )
134 11 rexuz3 ⊢ ( 1 ∈ ℤ → ( ∃ 𝑎 ∈ ℕ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑎 ) ∀ 𝑗 ∈ ( 1 ... 𝑚 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) ↔ ∃ 𝑎 ∈ ℤ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑎 ) ∀ 𝑗 ∈ ( 1 ... 𝑚 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) ) )
135 125 134 ax-mp ⊢ ( ∃ 𝑎 ∈ ℕ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑎 ) ∀ 𝑗 ∈ ( 1 ... 𝑚 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) ↔ ∃ 𝑎 ∈ ℤ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑎 ) ∀ 𝑗 ∈ ( 1 ... 𝑚 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) )
136 133 135 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) → ∃ 𝑎 ∈ ℕ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑎 ) ∀ 𝑗 ∈ ( 1 ... 𝑚 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) )
137 11 r19.2uz ⊢ ( ∃ 𝑎 ∈ ℕ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑎 ) ∀ 𝑗 ∈ ( 1 ... 𝑚 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) → ∃ 𝑛 ∈ ℕ ∀ 𝑗 ∈ ( 1 ... 𝑚 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) )
138 136 137 syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) → ∃ 𝑛 ∈ ℕ ∀ 𝑗 ∈ ( 1 ... 𝑚 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) )
139 1 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ∧ ( 𝑛 ∈ ℕ ∧ ∀ 𝑗 ∈ ( 1 ... 𝑚 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) ) ) ) → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
140 2 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ∧ ( 𝑛 ∈ ℕ ∧ ∀ 𝑗 ∈ ( 1 ... 𝑚 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) ) ) ) → Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) )
141 5 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ∧ ( 𝑛 ∈ ℕ ∧ ∀ 𝑗 ∈ ( 1 ... 𝑚 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) ) ) ) → ( vol* ‘ 𝐸 ) ∈ ℝ )
142 6 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ∧ ( 𝑛 ∈ ℕ ∧ ∀ 𝑗 ∈ ( 1 ... 𝑚 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) ) ) ) → 𝐶 ∈ ℝ+ )
143 7 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ∧ ( 𝑛 ∈ ℕ ∧ ∀ 𝑗 ∈ ( 1 ... 𝑚 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) ) ) ) → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
144 8 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ∧ ( 𝑛 ∈ ℕ ∧ ∀ 𝑗 ∈ ( 1 ... 𝑚 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) ) ) ) → 𝐸 ⊆ ∪ ran ( (,) ∘ 𝐺 ) )
145 10 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ∧ ( 𝑛 ∈ ℕ ∧ ∀ 𝑗 ∈ ( 1 ... 𝑚 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) ) ) ) → sup ( ran 𝑇 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐸 ) + 𝐶 ) )
146 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ∧ ( 𝑛 ∈ ℕ ∧ ∀ 𝑗 ∈ ( 1 ... 𝑚 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) ) ) ) → 𝑚 ∈ ℕ )
147 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ∧ ( 𝑛 ∈ ℕ ∧ ∀ 𝑗 ∈ ( 1 ... 𝑚 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) ) ) ) → ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 )
148 eqid ⊢ ∪ ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑚 ) ) = ∪ ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑚 ) )
149 simprrl ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ∧ ( 𝑛 ∈ ℕ ∧ ∀ 𝑗 ∈ ( 1 ... 𝑚 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) ) ) ) → 𝑛 ∈ ℕ )
150 simprrr ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ∧ ( 𝑛 ∈ ℕ ∧ ∀ 𝑗 ∈ ( 1 ... 𝑚 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) ) ) ) → ∀ 𝑗 ∈ ( 1 ... 𝑚 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) )
151 2fveq3 ⊢ ( 𝑖 = 𝑧 → ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) = ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) )
152 151 ineq1d ⊢ ( 𝑖 = 𝑧 → ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
153 152 fveq2d ⊢ ( 𝑖 = 𝑧 → ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) = ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) )
154 153 cbvsumv ⊢ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) = Σ 𝑧 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
155 2fveq3 ⊢ ( 𝑗 = 𝑘 → ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) = ( (,) ‘ ( 𝐺 ‘ 𝑘 ) ) )
156 155 ineq2d ⊢ ( 𝑗 = 𝑘 → ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑘 ) ) ) )
157 156 fveq2d ⊢ ( 𝑗 = 𝑘 → ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) = ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑘 ) ) ) ) )
158 157 sumeq2sdv ⊢ ( 𝑗 = 𝑘 → Σ 𝑧 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) = Σ 𝑧 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑘 ) ) ) ) )
159 154 158 eqtrid ⊢ ( 𝑗 = 𝑘 → Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) = Σ 𝑧 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑘 ) ) ) ) )
160 155 ineq1d ⊢ ( 𝑗 = 𝑘 → ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) = ( ( (,) ‘ ( 𝐺 ‘ 𝑘 ) ) ∩ 𝐴 ) )
161 160 fveq2d ⊢ ( 𝑗 = 𝑘 → ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) = ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑘 ) ) ∩ 𝐴 ) ) )
162 159 161 oveq12d ⊢ ( 𝑗 = 𝑘 → ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) = ( Σ 𝑧 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑘 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑘 ) ) ∩ 𝐴 ) ) ) )
163 162 fveq2d ⊢ ( 𝑗 = 𝑘 → ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) = ( abs ‘ ( Σ 𝑧 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑘 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑘 ) ) ∩ 𝐴 ) ) ) ) )
164 163 breq1d ⊢ ( 𝑗 = 𝑘 → ( ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) ↔ ( abs ‘ ( Σ 𝑧 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑘 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑘 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) ) )
165 164 cbvralvw ⊢ ( ∀ 𝑗 ∈ ( 1 ... 𝑚 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) ↔ ∀ 𝑘 ∈ ( 1 ... 𝑚 ) ( abs ‘ ( Σ 𝑧 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑘 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑘 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) )
166 150 165 sylib ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ∧ ( 𝑛 ∈ ℕ ∧ ∀ 𝑗 ∈ ( 1 ... 𝑚 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) ) ) ) → ∀ 𝑘 ∈ ( 1 ... 𝑚 ) ( abs ‘ ( Σ 𝑧 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑘 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑘 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) )
167 eqid ⊢ ∪ ( ( (,) ∘ 𝐹 ) “ ( 1 ... 𝑛 ) ) = ∪ ( ( (,) ∘ 𝐹 ) “ ( 1 ... 𝑛 ) )
168 139 140 3 4 141 142 143 144 9 145 146 147 148 149 166 167 uniioombllem5 ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ∧ ( 𝑛 ∈ ℕ ∧ ∀ 𝑗 ∈ ( 1 ... 𝑚 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) ) ) ) → ( ( vol* ‘ ( 𝐸 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐸 ∖ 𝐴 ) ) ) ≤ ( ( vol* ‘ 𝐸 ) + ( 4 · 𝐶 ) ) )
169 168 anassrs ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ∀ 𝑗 ∈ ( 1 ... 𝑚 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑚 ) ) ) → ( ( vol* ‘ ( 𝐸 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐸 ∖ 𝐴 ) ) ) ≤ ( ( vol* ‘ 𝐸 ) + ( 4 · 𝐶 ) ) )
170 138 169 rexlimddv ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( abs ‘ ( ( 𝑇 ‘ 𝑚 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) ) → ( ( vol* ‘ ( 𝐸 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐸 ∖ 𝐴 ) ) ) ≤ ( ( vol* ‘ 𝐸 ) + ( 4 · 𝐶 ) ) )
171 56 170 rexlimddv ⊢ ( 𝜑 → ( ( vol* ‘ ( 𝐸 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐸 ∖ 𝐴 ) ) ) ≤ ( ( vol* ‘ 𝐸 ) + ( 4 · 𝐶 ) ) )