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 · 𝐶 ) ) )