uniioombllem6

	Ref	Expression
Hypotheses	uniioombl.1	$⊢ φ \to F : ℕ ⟶ \leq \cap ℝ^{2}$
	uniioombl.2	$⊢ φ \to \underset{x \in ℕ}{Disj} (.) (F (x))$
	uniioombl.3	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
	uniioombl.a	$⊢ A = ⋃ ran ((.) \circ F)$
	uniioombl.e	$⊢ φ \to {vol}^{*} (E) \in ℝ$
	uniioombl.c	$⊢ φ \to C \in ℝ^{+}$
	uniioombl.g	$⊢ φ \to G : ℕ ⟶ \leq \cap ℝ^{2}$
	uniioombl.s	$⊢ φ \to E \subseteq ⋃ ran ((.) \circ G)$
	uniioombl.t	$⊢ T = seq 1 (+ ((abs \circ -) \circ G))$
	uniioombl.v	$⊢ φ \to sup (ran T ℝ^{} <) \leq {vol}^{} (E) + C$
Assertion	uniioombllem6	$⊢ φ \to {vol}^{} (E \cap A) + {vol}^{} (E ∖ A) \leq {vol}^{*} (E) + 4 C$

Proof

Step	Hyp	Ref	Expression
1		uniioombl.1	$⊢ φ \to F : ℕ ⟶ \leq \cap ℝ^{2}$
2		uniioombl.2	$⊢ φ \to \underset{x \in ℕ}{Disj} (.) (F (x))$
3		uniioombl.3	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
4		uniioombl.a	$⊢ A = ⋃ ran ((.) \circ F)$
5		uniioombl.e	$⊢ φ \to {vol}^{*} (E) \in ℝ$
6		uniioombl.c	$⊢ φ \to C \in ℝ^{+}$
7		uniioombl.g	$⊢ φ \to G : ℕ ⟶ \leq \cap ℝ^{2}$
8		uniioombl.s	$⊢ φ \to E \subseteq ⋃ ran ((.) \circ G)$
9		uniioombl.t	$⊢ T = seq 1 (+ ((abs \circ -) \circ G))$
10		uniioombl.v	$⊢ φ \to sup (ran T ℝ^{} <) \leq {vol}^{} (E) + C$
11		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
12		1zzd	$⊢ φ \to 1 \in ℤ$
13		eqidd	$⊢ (φ \land m \in ℕ) \to T (m) = T (m)$
14		eqidd	$⊢ (φ \land a \in ℕ) \to ((abs \circ -) \circ G) (a) = ((abs \circ -) \circ G) (a)$
15		eqid	$⊢ (abs \circ -) \circ G = (abs \circ -) \circ G$
16	15	ovolfsf	$⊢ G : ℕ ⟶ \leq \cap ℝ^{2} \to ((abs \circ -) \circ G) : ℕ ⟶ [0, +∞)$
17	7 16	syl	$⊢ φ \to ((abs \circ -) \circ G) : ℕ ⟶ [0, +∞)$
18	17	ffvelcdmda	$⊢ (φ \land a \in ℕ) \to ((abs \circ -) \circ G) (a) \in [0, +∞)$
19		elrege0	$⊢ ((abs \circ -) \circ G) (a) \in [0, +∞) \leftrightarrow (((abs \circ -) \circ G) (a) \in ℝ \land 0 \leq ((abs \circ -) \circ G) (a))$
20	18 19	sylib	$⊢ (φ \land a \in ℕ) \to (((abs \circ -) \circ G) (a) \in ℝ \land 0 \leq ((abs \circ -) \circ G) (a))$
21	20	simpld	$⊢ (φ \land a \in ℕ) \to ((abs \circ -) \circ G) (a) \in ℝ$
22	20	simprd	$⊢ (φ \land a \in ℕ) \to 0 \leq ((abs \circ -) \circ G) (a)$
23	1 2 3 4 5 6 7 8 9 10	uniioombllem1	$⊢ φ \to sup (ran T ℝ^{*} <) \in ℝ$
24	15 9	ovolsf	$⊢ G : ℕ ⟶ \leq \cap ℝ^{2} \to T : ℕ ⟶ [0, +∞)$
25	7 24	syl	$⊢ φ \to T : ℕ ⟶ [0, +∞)$
26	25	frnd	$⊢ φ \to ran T \subseteq [0, +∞)$
27		icossxr	$⊢ [0, +∞) \subseteq ℝ^{*}$
28	26 27	sstrdi	$⊢ φ \to ran T \subseteq ℝ^{*}$
29		supxrub	$⊢ (ran T \subseteq ℝ^{} \land x \in ran T) \to x \leq sup (ran T ℝ^{} <)$
30	28 29	sylan	$⊢ (φ \land x \in ran T) \to x \leq sup (ran T ℝ^{*} <)$
31	30	ralrimiva	$⊢ φ \to \forall x \in ran T x \leq sup (ran T ℝ^{*} <)$
32	25	ffnd	$⊢ φ \to T Fn ℕ$
33		breq1	$⊢ x = T (m) \to (x \leq sup (ran T ℝ^{} <) \leftrightarrow T (m) \leq sup (ran T ℝ^{} <))$
34	33	ralrn	$⊢ T Fn ℕ \to (\forall x \in ran T x \leq sup (ran T ℝ^{} <) \leftrightarrow \forall m \in ℕ T (m) \leq sup (ran T ℝ^{} <))$
35	32 34	syl	$⊢ φ \to (\forall x \in ran T x \leq sup (ran T ℝ^{} <) \leftrightarrow \forall m \in ℕ T (m) \leq sup (ran T ℝ^{} <))$
36	31 35	mpbid	$⊢ φ \to \forall m \in ℕ T (m) \leq sup (ran T ℝ^{*} <)$
37		brralrspcev	$⊢ (sup (ran T ℝ^{} <) \in ℝ \land \forall m \in ℕ T (m) \leq sup (ran T ℝ^{} <)) \to \exists x \in ℝ \forall m \in ℕ T (m) \leq x$
38	23 36 37	syl2anc	$⊢ φ \to \exists x \in ℝ \forall m \in ℕ T (m) \leq x$
39	11 9 12 14 21 22 38	isumsup2	$⊢ φ \to T ⇝ sup (ran T ℝ <)$
40		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
41	26 40	sstrdi	$⊢ φ \to ran T \subseteq ℝ$
42		1nn	$⊢ 1 \in ℕ$
43	25	fdmd	$⊢ φ \to dom T = ℕ$
44	42 43	eleqtrrid	$⊢ φ \to 1 \in dom T$
45	44	ne0d	$⊢ φ \to dom T \neq \emptyset$
46		dm0rn0	$⊢ dom T = \emptyset \leftrightarrow ran T = \emptyset$
47	46	necon3bii	$⊢ dom T \neq \emptyset \leftrightarrow ran T \neq \emptyset$
48	45 47	sylib	$⊢ φ \to ran T \neq \emptyset$
49		brralrspcev	$⊢ (sup (ran T ℝ^{} <) \in ℝ \land \forall x \in ran T x \leq sup (ran T ℝ^{} <)) \to \exists y \in ℝ \forall x \in ran T x \leq y$
50	23 31 49	syl2anc	$⊢ φ \to \exists y \in ℝ \forall x \in ran T x \leq y$
51		supxrre	$⊢ (ran T \subseteq ℝ \land ran T \neq \emptyset \land \exists y \in ℝ \forall x \in ran T x \leq y) \to sup (ran T ℝ^{*} <) = sup (ran T ℝ <)$
52	41 48 50 51	syl3anc	$⊢ φ \to sup (ran T ℝ^{*} <) = sup (ran T ℝ <)$
53	39 52	breqtrrd	$⊢ φ \to T ⇝ sup (ran T ℝ^{*} <)$
54	11 12 6 13 53	climi2	$⊢ φ \to \exists j \in ℕ \forall m \in ℤ_{\geq j} \|T (m) - sup (ran T ℝ^{*} <)\| < C$
55	11	r19.2uz	$⊢ \exists j \in ℕ \forall m \in ℤ_{\geq j} \|T (m) - sup (ran T ℝ^{} <)\| < C \to \exists m \in ℕ \|T (m) - sup (ran T ℝ^{} <)\| < C$
56	54 55	syl	$⊢ φ \to \exists m \in ℕ \|T (m) - sup (ran T ℝ^{*} <)\| < C$
57		1zzd	$⊢ ((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{*} <)\| < C)) \land j \in (1 \dots m)) \to 1 \in ℤ$
58	6	ad2antrr	$⊢ ((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{*} <)\| < C)) \land j \in (1 \dots m)) \to C \in ℝ^{+}$
59		simplrl	$⊢ ((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{*} <)\| < C)) \land j \in (1 \dots m)) \to m \in ℕ$
60	59	nnrpd	$⊢ ((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{*} <)\| < C)) \land j \in (1 \dots m)) \to m \in ℝ^{+}$
61	58 60	rpdivcld	$⊢ ((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{*} <)\| < C)) \land j \in (1 \dots m)) \to \frac{C}{m} \in ℝ^{+}$
62		fvex	$⊢ (.) (F (z)) \in V$
63	62	inex1	$⊢ (.) (F (z)) \cap (.) (G (j)) \in V$
64	63	rgenw	$⊢ \forall z \in ℕ (.) (F (z)) \cap (.) (G (j)) \in V$
65		eqid	$⊢ (z \in ℕ ⟼ (.) (F (z)) \cap (.) (G (j))) = (z \in ℕ ⟼ (.) (F (z)) \cap (.) (G (j)))$
66	65	fnmpt	$⊢ \forall z \in ℕ (.) (F (z)) \cap (.) (G (j)) \in V \to (z \in ℕ ⟼ (.) (F (z)) \cap (.) (G (j))) Fn ℕ$
67	64 66	mp1i	$⊢ (((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{*} <)\| < C)) \land j \in (1 \dots m)) \land n \in ℕ) \to (z \in ℕ ⟼ (.) (F (z)) \cap (.) (G (j))) Fn ℕ$
68		elfznn	$⊢ i \in (1 \dots n) \to i \in ℕ$
69		fvco2	$⊢ ((z \in ℕ ⟼ (.) (F (z)) \cap (.) (G (j))) Fn ℕ \land i \in ℕ) \to ({vol}^{} \circ (z \in ℕ ⟼ (.) (F (z)) \cap (.) (G (j)))) (i) = {vol}^{} ((z \in ℕ ⟼ (.) (F (z)) \cap (.) (G (j))) (i))$
70	67 68 69	syl2an	$⊢ ((((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C)) \land j \in (1 \dots m)) \land n \in ℕ) \land i \in (1 \dots n)) \to ({vol}^{} \circ (z \in ℕ ⟼ (.) (F (z)) \cap (.) (G (j)))) (i) = {vol}^{*} ((z \in ℕ ⟼ (.) (F (z)) \cap (.) (G (j))) (i))$
71	68	adantl	$⊢ ((((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{*} <)\| < C)) \land j \in (1 \dots m)) \land n \in ℕ) \land i \in (1 \dots n)) \to i \in ℕ$
72		2fveq3	$⊢ z = i \to (.) (F (z)) = (.) (F (i))$
73	72	ineq1d	$⊢ z = i \to (.) (F (z)) \cap (.) (G (j)) = (.) (F (i)) \cap (.) (G (j))$
74		fvex	$⊢ (.) (F (i)) \in V$
75	74	inex1	$⊢ (.) (F (i)) \cap (.) (G (j)) \in V$
76	73 65 75	fvmpt	$⊢ i \in ℕ \to (z \in ℕ ⟼ (.) (F (z)) \cap (.) (G (j))) (i) = (.) (F (i)) \cap (.) (G (j))$
77	71 76	syl	$⊢ ((((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{*} <)\| < C)) \land j \in (1 \dots m)) \land n \in ℕ) \land i \in (1 \dots n)) \to (z \in ℕ ⟼ (.) (F (z)) \cap (.) (G (j))) (i) = (.) (F (i)) \cap (.) (G (j))$
78	77	fveq2d	$⊢ ((((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C)) \land j \in (1 \dots m)) \land n \in ℕ) \land i \in (1 \dots n)) \to {vol}^{} ((z \in ℕ ⟼ (.) (F (z)) \cap (.) (G (j))) (i)) = {vol}^{*} ((.) (F (i)) \cap (.) (G (j)))$
79	70 78	eqtrd	$⊢ ((((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C)) \land j \in (1 \dots m)) \land n \in ℕ) \land i \in (1 \dots n)) \to ({vol}^{} \circ (z \in ℕ ⟼ (.) (F (z)) \cap (.) (G (j)))) (i) = {vol}^{*} ((.) (F (i)) \cap (.) (G (j)))$
80		simpr	$⊢ (((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{*} <)\| < C)) \land j \in (1 \dots m)) \land n \in ℕ) \to n \in ℕ$
81	80 11	eleqtrdi	$⊢ (((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{*} <)\| < C)) \land j \in (1 \dots m)) \land n \in ℕ) \to n \in ℤ_{\geq 1}$
82		inss2	$⊢ (.) (F (i)) \cap (.) (G (j)) \subseteq (.) (G (j))$
83	7	adantr	$⊢ (φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{*} <)\| < C)) \to G : ℕ ⟶ \leq \cap ℝ^{2}$
84		elfznn	$⊢ j \in (1 \dots m) \to j \in ℕ$
85		ffvelcdm	$⊢ (G : ℕ ⟶ \leq \cap ℝ^{2} \land j \in ℕ) \to G (j) \in (\leq \cap ℝ^{2})$
86	83 84 85	syl2an	$⊢ ((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{*} <)\| < C)) \land j \in (1 \dots m)) \to G (j) \in (\leq \cap ℝ^{2})$
87	86	elin2d	$⊢ ((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{*} <)\| < C)) \land j \in (1 \dots m)) \to G (j) \in ℝ^{2}$
88		1st2nd2	$⊢ G (j) \in ℝ^{2} \to G (j) = ⟨1^{st} (G (j)), 2^{nd} (G (j))⟩$
89	87 88	syl	$⊢ ((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{*} <)\| < C)) \land j \in (1 \dots m)) \to G (j) = ⟨1^{st} (G (j)), 2^{nd} (G (j))⟩$
90	89	fveq2d	$⊢ ((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{*} <)\| < C)) \land j \in (1 \dots m)) \to (.) (G (j)) = (.) (⟨1^{st} (G (j)), 2^{nd} (G (j))⟩)$
91		df-ov	$⊢ (1^{st} (G (j)), 2^{nd} (G (j))) = (.) (⟨1^{st} (G (j)), 2^{nd} (G (j))⟩)$
92	90 91	eqtr4di	$⊢ ((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{*} <)\| < C)) \land j \in (1 \dots m)) \to (.) (G (j)) = (1^{st} (G (j)), 2^{nd} (G (j)))$
93		ioossre	$⊢ (1^{st} (G (j)), 2^{nd} (G (j))) \subseteq ℝ$
94	92 93	eqsstrdi	$⊢ ((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{*} <)\| < C)) \land j \in (1 \dots m)) \to (.) (G (j)) \subseteq ℝ$
95	94	ad2antrr	$⊢ ((((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{*} <)\| < C)) \land j \in (1 \dots m)) \land n \in ℕ) \land i \in (1 \dots n)) \to (.) (G (j)) \subseteq ℝ$
96	92	fveq2d	$⊢ ((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C)) \land j \in (1 \dots m)) \to {vol}^{} ((.) (G (j))) = {vol}^{*} ((1^{st} (G (j)), 2^{nd} (G (j))))$
97		ovolfcl	$⊢ (G : ℕ ⟶ \leq \cap ℝ^{2} \land j \in ℕ) \to (1^{st} (G (j)) \in ℝ \land 2^{nd} (G (j)) \in ℝ \land 1^{st} (G (j)) \leq 2^{nd} (G (j)))$
98	83 84 97	syl2an	$⊢ ((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{*} <)\| < C)) \land j \in (1 \dots m)) \to (1^{st} (G (j)) \in ℝ \land 2^{nd} (G (j)) \in ℝ \land 1^{st} (G (j)) \leq 2^{nd} (G (j)))$
99		ovolioo	$⊢ (1^{st} (G (j)) \in ℝ \land 2^{nd} (G (j)) \in ℝ \land 1^{st} (G (j)) \leq 2^{nd} (G (j))) \to {vol}^{*} ((1^{st} (G (j)), 2^{nd} (G (j)))) = 2^{nd} (G (j)) - 1^{st} (G (j))$
100	98 99	syl	$⊢ ((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C)) \land j \in (1 \dots m)) \to {vol}^{} ((1^{st} (G (j)), 2^{nd} (G (j)))) = 2^{nd} (G (j)) - 1^{st} (G (j))$
101	96 100	eqtrd	$⊢ ((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C)) \land j \in (1 \dots m)) \to {vol}^{} ((.) (G (j))) = 2^{nd} (G (j)) - 1^{st} (G (j))$
102	98	simp2d	$⊢ ((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{*} <)\| < C)) \land j \in (1 \dots m)) \to 2^{nd} (G (j)) \in ℝ$
103	98	simp1d	$⊢ ((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{*} <)\| < C)) \land j \in (1 \dots m)) \to 1^{st} (G (j)) \in ℝ$
104	102 103	resubcld	$⊢ ((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{*} <)\| < C)) \land j \in (1 \dots m)) \to 2^{nd} (G (j)) - 1^{st} (G (j)) \in ℝ$
105	101 104	eqeltrd	$⊢ ((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C)) \land j \in (1 \dots m)) \to {vol}^{} ((.) (G (j))) \in ℝ$
106	105	ad2antrr	$⊢ ((((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C)) \land j \in (1 \dots m)) \land n \in ℕ) \land i \in (1 \dots n)) \to {vol}^{} ((.) (G (j))) \in ℝ$
107		ovolsscl	$⊢ ((.) (F (i)) \cap (.) (G (j)) \subseteq (.) (G (j)) \land (.) (G (j)) \subseteq ℝ \land {vol}^{} ((.) (G (j))) \in ℝ) \to {vol}^{} ((.) (F (i)) \cap (.) (G (j))) \in ℝ$
108	82 95 106 107	mp3an2i	$⊢ ((((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C)) \land j \in (1 \dots m)) \land n \in ℕ) \land i \in (1 \dots n)) \to {vol}^{} ((.) (F (i)) \cap (.) (G (j))) \in ℝ$
109	108	recnd	$⊢ ((((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C)) \land j \in (1 \dots m)) \land n \in ℕ) \land i \in (1 \dots n)) \to {vol}^{} ((.) (F (i)) \cap (.) (G (j))) \in ℂ$
110	79 81 109	fsumser	$⊢ (((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C)) \land j \in (1 \dots m)) \land n \in ℕ) \to \sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) = seq 1 (+ ({vol}^{*} \circ (z \in ℕ ⟼ (.) (F (z)) \cap (.) (G (j))))) (n)$
111	110	eqcomd	$⊢ (((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C)) \land j \in (1 \dots m)) \land n \in ℕ) \to seq 1 (+ ({vol}^{} \circ (z \in ℕ ⟼ (.) (F (z)) \cap (.) (G (j))))) (n) = \sum_{i = 1}^{n} {vol}^{*} ((.) (F (i)) \cap (.) (G (j)))$
112		2fveq3	$⊢ z = k \to (.) (F (z)) = (.) (F (k))$
113	112	ineq1d	$⊢ z = k \to (.) (F (z)) \cap (.) (G (j)) = (.) (F (k)) \cap (.) (G (j))$
114	113	cbvmptv	$⊢ (z \in ℕ ⟼ (.) (F (z)) \cap (.) (G (j))) = (k \in ℕ ⟼ (.) (F (k)) \cap (.) (G (j)))$
115		eqeq1	$⊢ z = x \to (z = \emptyset \leftrightarrow x = \emptyset)$
116		infeq1	$⊢ z = x \to inf (z ℝ^{} <) = inf (x ℝ^{} <)$
117		supeq1	$⊢ z = x \to sup (z ℝ^{} <) = sup (x ℝ^{} <)$
118	116 117	opeq12d	$⊢ z = x \to ⟨inf (z ℝ^{} <), sup (z ℝ^{} <)⟩ = ⟨inf (x ℝ^{} <), sup (x ℝ^{} <)⟩$
119	115 118	ifbieq2d	$⊢ z = x \to if (z = \emptyset, ⟨0, 0⟩, ⟨inf (z ℝ^{} <), sup (z ℝ^{} <)⟩) = if (x = \emptyset, ⟨0, 0⟩, ⟨inf (x ℝ^{} <), sup (x ℝ^{} <)⟩)$
120	119	cbvmptv	$⊢ (z \in ran (.) ⟼ if (z = \emptyset, ⟨0, 0⟩, ⟨inf (z ℝ^{} <), sup (z ℝ^{} <)⟩)) = (x \in ran (.) ⟼ if (x = \emptyset, ⟨0, 0⟩, ⟨inf (x ℝ^{} <), sup (x ℝ^{} <)⟩))$
121	1 2 3 4 5 6 7 8 9 10 114 120	uniioombllem2	$⊢ (φ \land j \in ℕ) \to seq 1 (+ ({vol}^{} \circ (z \in ℕ ⟼ (.) (F (z)) \cap (.) (G (j))))) ⇝ {vol}^{} ((.) (G (j)) \cap A)$
122	84 121	sylan2	$⊢ (φ \land j \in (1 \dots m)) \to seq 1 (+ ({vol}^{} \circ (z \in ℕ ⟼ (.) (F (z)) \cap (.) (G (j))))) ⇝ {vol}^{} ((.) (G (j)) \cap A)$
123	122	adantlr	$⊢ ((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C)) \land j \in (1 \dots m)) \to seq 1 (+ ({vol}^{} \circ (z \in ℕ ⟼ (.) (F (z)) \cap (.) (G (j))))) ⇝ {vol}^{*} ((.) (G (j)) \cap A)$
124	11 57 61 111 123	climi2	$⊢ ((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C)) \land j \in (1 \dots m)) \to \exists a \in ℕ \forall n \in ℤ_{\geq a} \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{*} ((.) (G (j)) \cap A)\| < \frac{C}{m}$
125		1z	$⊢ 1 \in ℤ$
126	11	rexuz3	$⊢ 1 \in ℤ \to (\exists a \in ℕ \forall n \in ℤ_{\geq a} \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{} ((.) (G (j)) \cap A)\| < \frac{C}{m} \leftrightarrow \exists a \in ℤ \forall n \in ℤ_{\geq a} \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{} ((.) (G (j)) \cap A)\| < \frac{C}{m})$
127	125 126	ax-mp	$⊢ \exists a \in ℕ \forall n \in ℤ_{\geq a} \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{} ((.) (G (j)) \cap A)\| < \frac{C}{m} \leftrightarrow \exists a \in ℤ \forall n \in ℤ_{\geq a} \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{} ((.) (G (j)) \cap A)\| < \frac{C}{m}$
128	124 127	sylib	$⊢ ((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C)) \land j \in (1 \dots m)) \to \exists a \in ℤ \forall n \in ℤ_{\geq a} \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{*} ((.) (G (j)) \cap A)\| < \frac{C}{m}$
129	128	ralrimiva	$⊢ (φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C)) \to \forall j \in (1 \dots m) \exists a \in ℤ \forall n \in ℤ_{\geq a} \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{*} ((.) (G (j)) \cap A)\| < \frac{C}{m}$
130		fzfi	$⊢ (1 \dots m) \in Fin$
131		rexfiuz	$⊢ (1 \dots m) \in Fin \to (\exists a \in ℤ \forall n \in ℤ_{\geq a} \forall j \in (1 \dots m) \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{} ((.) (G (j)) \cap A)\| < \frac{C}{m} \leftrightarrow \forall j \in (1 \dots m) \exists a \in ℤ \forall n \in ℤ_{\geq a} \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{} ((.) (G (j)) \cap A)\| < \frac{C}{m})$
132	130 131	ax-mp	$⊢ \exists a \in ℤ \forall n \in ℤ_{\geq a} \forall j \in (1 \dots m) \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{} ((.) (G (j)) \cap A)\| < \frac{C}{m} \leftrightarrow \forall j \in (1 \dots m) \exists a \in ℤ \forall n \in ℤ_{\geq a} \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{} ((.) (G (j)) \cap A)\| < \frac{C}{m}$
133	129 132	sylibr	$⊢ (φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C)) \to \exists a \in ℤ \forall n \in ℤ_{\geq a} \forall j \in (1 \dots m) \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{*} ((.) (G (j)) \cap A)\| < \frac{C}{m}$
134	11	rexuz3	$⊢ 1 \in ℤ \to (\exists a \in ℕ \forall n \in ℤ_{\geq a} \forall j \in (1 \dots m) \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{} ((.) (G (j)) \cap A)\| < \frac{C}{m} \leftrightarrow \exists a \in ℤ \forall n \in ℤ_{\geq a} \forall j \in (1 \dots m) \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{} ((.) (G (j)) \cap A)\| < \frac{C}{m})$
135	125 134	ax-mp	$⊢ \exists a \in ℕ \forall n \in ℤ_{\geq a} \forall j \in (1 \dots m) \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{} ((.) (G (j)) \cap A)\| < \frac{C}{m} \leftrightarrow \exists a \in ℤ \forall n \in ℤ_{\geq a} \forall j \in (1 \dots m) \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{} ((.) (G (j)) \cap A)\| < \frac{C}{m}$
136	133 135	sylibr	$⊢ (φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C)) \to \exists a \in ℕ \forall n \in ℤ_{\geq a} \forall j \in (1 \dots m) \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{*} ((.) (G (j)) \cap A)\| < \frac{C}{m}$
137	11	r19.2uz	$⊢ \exists a \in ℕ \forall n \in ℤ_{\geq a} \forall j \in (1 \dots m) \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{} ((.) (G (j)) \cap A)\| < \frac{C}{m} \to \exists n \in ℕ \forall j \in (1 \dots m) \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{} ((.) (G (j)) \cap A)\| < \frac{C}{m}$
138	136 137	syl	$⊢ (φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C)) \to \exists n \in ℕ \forall j \in (1 \dots m) \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{*} ((.) (G (j)) \cap A)\| < \frac{C}{m}$
139	1	adantr	$⊢ (φ \land ((m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C) \land (n \in ℕ \land \forall j \in (1 \dots m) \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{*} ((.) (G (j)) \cap A)\| < \frac{C}{m}))) \to F : ℕ ⟶ \leq \cap ℝ^{2}$
140	2	adantr	$⊢ (φ \land ((m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C) \land (n \in ℕ \land \forall j \in (1 \dots m) \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{*} ((.) (G (j)) \cap A)\| < \frac{C}{m}))) \to \underset{x \in ℕ}{Disj} (.) (F (x))$
141	5	adantr	$⊢ (φ \land ((m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C) \land (n \in ℕ \land \forall j \in (1 \dots m) \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{} ((.) (G (j)) \cap A)\| < \frac{C}{m}))) \to {vol}^{} (E) \in ℝ$
142	6	adantr	$⊢ (φ \land ((m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C) \land (n \in ℕ \land \forall j \in (1 \dots m) \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{*} ((.) (G (j)) \cap A)\| < \frac{C}{m}))) \to C \in ℝ^{+}$
143	7	adantr	$⊢ (φ \land ((m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C) \land (n \in ℕ \land \forall j \in (1 \dots m) \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{*} ((.) (G (j)) \cap A)\| < \frac{C}{m}))) \to G : ℕ ⟶ \leq \cap ℝ^{2}$
144	8	adantr	$⊢ (φ \land ((m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C) \land (n \in ℕ \land \forall j \in (1 \dots m) \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{*} ((.) (G (j)) \cap A)\| < \frac{C}{m}))) \to E \subseteq ⋃ ran ((.) \circ G)$
145	10	adantr	$⊢ (φ \land ((m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C) \land (n \in ℕ \land \forall j \in (1 \dots m) \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{} ((.) (G (j)) \cap A)\| < \frac{C}{m}))) \to sup (ran T ℝ^{} <) \leq {vol}^{*} (E) + C$
146		simprll	$⊢ (φ \land ((m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C) \land (n \in ℕ \land \forall j \in (1 \dots m) \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{*} ((.) (G (j)) \cap A)\| < \frac{C}{m}))) \to m \in ℕ$
147		simprlr	$⊢ (φ \land ((m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C) \land (n \in ℕ \land \forall j \in (1 \dots m) \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{} ((.) (G (j)) \cap A)\| < \frac{C}{m}))) \to \|T (m) - sup (ran T ℝ^{} <)\| < C$
148		eqid	$⊢ ⋃ ((.) \circ G) [(1 \dots m)] = ⋃ ((.) \circ G) [(1 \dots m)]$
149		simprrl	$⊢ (φ \land ((m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C) \land (n \in ℕ \land \forall j \in (1 \dots m) \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{*} ((.) (G (j)) \cap A)\| < \frac{C}{m}))) \to n \in ℕ$
150		simprrr	$⊢ (φ \land ((m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C) \land (n \in ℕ \land \forall j \in (1 \dots m) \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{} ((.) (G (j)) \cap A)\| < \frac{C}{m}))) \to \forall j \in (1 \dots m) \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{*} ((.) (G (j)) \cap A)\| < \frac{C}{m}$
151		2fveq3	$⊢ i = z \to (.) (F (i)) = (.) (F (z))$
152	151	ineq1d	$⊢ i = z \to (.) (F (i)) \cap (.) (G (j)) = (.) (F (z)) \cap (.) (G (j))$
153	152	fveq2d	$⊢ i = z \to {vol}^{} ((.) (F (i)) \cap (.) (G (j))) = {vol}^{} ((.) (F (z)) \cap (.) (G (j)))$
154	153	cbvsumv	$⊢ \sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) = \sum_{z = 1}^{n} {vol}^{} ((.) (F (z)) \cap (.) (G (j)))$
155		2fveq3	$⊢ j = k \to (.) (G (j)) = (.) (G (k))$
156	155	ineq2d	$⊢ j = k \to (.) (F (z)) \cap (.) (G (j)) = (.) (F (z)) \cap (.) (G (k))$
157	156	fveq2d	$⊢ j = k \to {vol}^{} ((.) (F (z)) \cap (.) (G (j))) = {vol}^{} ((.) (F (z)) \cap (.) (G (k)))$
158	157	sumeq2sdv	$⊢ j = k \to \sum_{z = 1}^{n} {vol}^{} ((.) (F (z)) \cap (.) (G (j))) = \sum_{z = 1}^{n} {vol}^{} ((.) (F (z)) \cap (.) (G (k)))$
159	154 158	eqtrid	$⊢ j = k \to \sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) = \sum_{z = 1}^{n} {vol}^{} ((.) (F (z)) \cap (.) (G (k)))$
160	155	ineq1d	$⊢ j = k \to (.) (G (j)) \cap A = (.) (G (k)) \cap A$
161	160	fveq2d	$⊢ j = k \to {vol}^{} ((.) (G (j)) \cap A) = {vol}^{} ((.) (G (k)) \cap A)$
162	159 161	oveq12d	$⊢ j = k \to \sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{} ((.) (G (j)) \cap A) = \sum_{z = 1}^{n} {vol}^{} ((.) (F (z)) \cap (.) (G (k))) - {vol}^{} ((.) (G (k)) \cap A)$
163	162	fveq2d	$⊢ j = k \to \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{} ((.) (G (j)) \cap A)\| = \|\sum_{z = 1}^{n} {vol}^{} ((.) (F (z)) \cap (.) (G (k))) - {vol}^{} ((.) (G (k)) \cap A)\|$
164	163	breq1d	$⊢ j = k \to (\|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{} ((.) (G (j)) \cap A)\| < \frac{C}{m} \leftrightarrow \|\sum_{z = 1}^{n} {vol}^{} ((.) (F (z)) \cap (.) (G (k))) - {vol}^{} ((.) (G (k)) \cap A)\| < \frac{C}{m})$
165	164	cbvralvw	$⊢ \forall j \in (1 \dots m) \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{} ((.) (G (j)) \cap A)\| < \frac{C}{m} \leftrightarrow \forall k \in (1 \dots m) \|\sum_{z = 1}^{n} {vol}^{} ((.) (F (z)) \cap (.) (G (k))) - {vol}^{} ((.) (G (k)) \cap A)\| < \frac{C}{m}$
166	150 165	sylib	$⊢ (φ \land ((m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C) \land (n \in ℕ \land \forall j \in (1 \dots m) \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{} ((.) (G (j)) \cap A)\| < \frac{C}{m}))) \to \forall k \in (1 \dots m) \|\sum_{z = 1}^{n} {vol}^{} ((.) (F (z)) \cap (.) (G (k))) - {vol}^{*} ((.) (G (k)) \cap A)\| < \frac{C}{m}$
167		eqid	$⊢ ⋃ ((.) \circ F) [(1 \dots n)] = ⋃ ((.) \circ F) [(1 \dots n)]$
168	139 140 3 4 141 142 143 144 9 145 146 147 148 149 166 167	uniioombllem5	$⊢ (φ \land ((m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C) \land (n \in ℕ \land \forall j \in (1 \dots m) \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{} ((.) (G (j)) \cap A)\| < \frac{C}{m}))) \to {vol}^{} (E \cap A) + {vol}^{} (E ∖ A) \leq {vol}^{} (E) + 4 C$
169	168	anassrs	$⊢ ((φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C)) \land (n \in ℕ \land \forall j \in (1 \dots m) \|\sum_{i = 1}^{n} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{} ((.) (G (j)) \cap A)\| < \frac{C}{m})) \to {vol}^{} (E \cap A) + {vol}^{} (E ∖ A) \leq {vol}^{} (E) + 4 C$
170	138 169	rexlimddv	$⊢ (φ \land (m \in ℕ \land \|T (m) - sup (ran T ℝ^{} <)\| < C)) \to {vol}^{} (E \cap A) + {vol}^{} (E ∖ A) \leq {vol}^{} (E) + 4 C$
171	56 170	rexlimddv	$⊢ φ \to {vol}^{} (E \cap A) + {vol}^{} (E ∖ A) \leq {vol}^{*} (E) + 4 C$

Metamath Proof Explorer

Theorem uniioombllem6

Proof