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* ‘ ( 𝐾 ∩ 𝐿 ) ) + 𝐶 ) )