mblfinlem3

Description: The difference between two sets measurable by the criterion in ismblfin is itself measurable by the same. Corollary 0.3 of Viaclovsky7 p. 3. (Contributed by Brendan Leahy, 25-Mar-2018) (Revised by Brendan Leahy, 13-Jul-2018)

		Ref	Expression
	Assertion	mblfinlem3	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land ({vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <) \land {vol}^{} (B) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} ℝ <))) \to sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land y = vol (b))\} ℝ <) = {vol}^{*} (A ∖ B)$

Proof

Step	Hyp	Ref	Expression
1		ltso	$⊢ < Or ℝ$
2	1	a1i	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land ({vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <) \land {vol}^{} (B) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} ℝ <))) \to < Or ℝ$
3		difss	$⊢ A ∖ B \subseteq A$
4		ovolsscl	$⊢ (A ∖ B \subseteq A \land A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} (A ∖ B) \in ℝ$
5	3 4	mp3an1	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} (A ∖ B) \in ℝ$
6	5	3ad2ant1	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land ({vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <) \land {vol}^{} (B) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} ℝ <))) \to {vol}^{*} (A ∖ B) \in ℝ$
7		vex	$⊢ u \in V$
8		eqeq1	$⊢ y = u \to (y = vol (b) \leftrightarrow u = vol (b))$
9	8	anbi2d	$⊢ y = u \to ((b \subseteq A ∖ B \land y = vol (b)) \leftrightarrow (b \subseteq A ∖ B \land u = vol (b)))$
10	9	rexbidv	$⊢ y = u \to (\exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land y = vol (b)) \leftrightarrow \exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land u = vol (b)))$
11	7 10	elab	$⊢ u \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land y = vol (b))\} \leftrightarrow \exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land u = vol (b))$
12		simprl	$⊢ (b \in Clsd (topGen (ran (.))) \land (b \subseteq A ∖ B \land u = vol (b))) \to b \subseteq A ∖ B$
13		ssdifss	$⊢ A \subseteq ℝ \to A ∖ B \subseteq ℝ$
14		ovolss	$⊢ (b \subseteq A ∖ B \land A ∖ B \subseteq ℝ) \to {vol}^{} (b) \leq {vol}^{} (A ∖ B)$
15	12 13 14	syl2anr	$⊢ (A \subseteq ℝ \land (b \in Clsd (topGen (ran (.))) \land (b \subseteq A ∖ B \land u = vol (b)))) \to {vol}^{} (b) \leq {vol}^{} (A ∖ B)$
16		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
17	16	cldss	$⊢ b \in Clsd (topGen (ran (.))) \to b \subseteq ℝ$
18		ovolcl	$⊢ b \subseteq ℝ \to {vol}^{} (b) \in ℝ^{}$
19	17 18	syl	$⊢ b \in Clsd (topGen (ran (.))) \to {vol}^{} (b) \in ℝ^{}$
20		ovolcl	$⊢ A ∖ B \subseteq ℝ \to {vol}^{} (A ∖ B) \in ℝ^{}$
21	13 20	syl	$⊢ A \subseteq ℝ \to {vol}^{} (A ∖ B) \in ℝ^{}$
22		xrlenlt	$⊢ ({vol}^{} (b) \in ℝ^{} \land {vol}^{} (A ∖ B) \in ℝ^{}) \to ({vol}^{} (b) \leq {vol}^{} (A ∖ B) \leftrightarrow \neg {vol}^{} (A ∖ B) < {vol}^{} (b))$
23	19 21 22	syl2anr	$⊢ (A \subseteq ℝ \land b \in Clsd (topGen (ran (.)))) \to ({vol}^{} (b) \leq {vol}^{} (A ∖ B) \leftrightarrow \neg {vol}^{} (A ∖ B) < {vol}^{} (b))$
24	23	adantrr	$⊢ (A \subseteq ℝ \land (b \in Clsd (topGen (ran (.))) \land (b \subseteq A ∖ B \land u = vol (b)))) \to ({vol}^{} (b) \leq {vol}^{} (A ∖ B) \leftrightarrow \neg {vol}^{} (A ∖ B) < {vol}^{} (b))$
25		id	$⊢ u = vol (b) \to u = vol (b)$
26		dfss4	$⊢ b \subseteq ℝ \leftrightarrow ℝ ∖ (ℝ ∖ b) = b$
27	17 26	sylib	$⊢ b \in Clsd (topGen (ran (.))) \to ℝ ∖ (ℝ ∖ b) = b$
28		rembl	$⊢ ℝ \in dom vol$
29	16	cldopn	$⊢ b \in Clsd (topGen (ran (.))) \to ℝ ∖ b \in topGen (ran (.))$
30		opnmbl	$⊢ ℝ ∖ b \in topGen (ran (.)) \to ℝ ∖ b \in dom vol$
31	29 30	syl	$⊢ b \in Clsd (topGen (ran (.))) \to ℝ ∖ b \in dom vol$
32		difmbl	$⊢ (ℝ \in dom vol \land ℝ ∖ b \in dom vol) \to ℝ ∖ (ℝ ∖ b) \in dom vol$
33	28 31 32	sylancr	$⊢ b \in Clsd (topGen (ran (.))) \to ℝ ∖ (ℝ ∖ b) \in dom vol$
34	27 33	eqeltrrd	$⊢ b \in Clsd (topGen (ran (.))) \to b \in dom vol$
35		mblvol	$⊢ b \in dom vol \to vol (b) = {vol}^{*} (b)$
36	34 35	syl	$⊢ b \in Clsd (topGen (ran (.))) \to vol (b) = {vol}^{*} (b)$
37	25 36	sylan9eqr	$⊢ (b \in Clsd (topGen (ran (.))) \land u = vol (b)) \to u = {vol}^{*} (b)$
38	37	breq2d	$⊢ (b \in Clsd (topGen (ran (.))) \land u = vol (b)) \to ({vol}^{} (A ∖ B) < u \leftrightarrow {vol}^{} (A ∖ B) < {vol}^{*} (b))$
39	38	notbid	$⊢ (b \in Clsd (topGen (ran (.))) \land u = vol (b)) \to (\neg {vol}^{} (A ∖ B) < u \leftrightarrow \neg {vol}^{} (A ∖ B) < {vol}^{*} (b))$
40	39	adantrl	$⊢ (b \in Clsd (topGen (ran (.))) \land (b \subseteq A ∖ B \land u = vol (b))) \to (\neg {vol}^{} (A ∖ B) < u \leftrightarrow \neg {vol}^{} (A ∖ B) < {vol}^{*} (b))$
41	40	adantl	$⊢ (A \subseteq ℝ \land (b \in Clsd (topGen (ran (.))) \land (b \subseteq A ∖ B \land u = vol (b)))) \to (\neg {vol}^{} (A ∖ B) < u \leftrightarrow \neg {vol}^{} (A ∖ B) < {vol}^{*} (b))$
42	24 41	bitr4d	$⊢ (A \subseteq ℝ \land (b \in Clsd (topGen (ran (.))) \land (b \subseteq A ∖ B \land u = vol (b)))) \to ({vol}^{} (b) \leq {vol}^{} (A ∖ B) \leftrightarrow \neg {vol}^{*} (A ∖ B) < u)$
43	15 42	mpbid	$⊢ (A \subseteq ℝ \land (b \in Clsd (topGen (ran (.))) \land (b \subseteq A ∖ B \land u = vol (b)))) \to \neg {vol}^{*} (A ∖ B) < u$
44	43	rexlimdvaa	$⊢ A \subseteq ℝ \to (\exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land u = vol (b)) \to \neg {vol}^{*} (A ∖ B) < u)$
45	44	imp	$⊢ (A \subseteq ℝ \land \exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land u = vol (b))) \to \neg {vol}^{*} (A ∖ B) < u$
46	11 45	sylan2b	$⊢ (A \subseteq ℝ \land u \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land y = vol (b))\}) \to \neg {vol}^{*} (A ∖ B) < u$
47	46	adantlr	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land u \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land y = vol (b))\}) \to \neg {vol}^{} (A ∖ B) < u$
48	47	3ad2antl1	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land ({vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <) \land {vol}^{} (B) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} ℝ <))) \land u \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land y = vol (b))\}) \to \neg {vol}^{*} (A ∖ B) < u$
49		simplr	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to {vol}^{*} (A) \in ℝ$
50		resubcl	$⊢ ({vol}^{} (A ∖ B) \in ℝ \land u \in ℝ) \to {vol}^{} (A ∖ B) - u \in ℝ$
51	50	adantrr	$⊢ ({vol}^{} (A ∖ B) \in ℝ \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to {vol}^{*} (A ∖ B) - u \in ℝ$
52		posdif	$⊢ (u \in ℝ \land {vol}^{} (A ∖ B) \in ℝ) \to (u < {vol}^{} (A ∖ B) \leftrightarrow 0 < {vol}^{*} (A ∖ B) - u)$
53	52	ancoms	$⊢ ({vol}^{} (A ∖ B) \in ℝ \land u \in ℝ) \to (u < {vol}^{} (A ∖ B) \leftrightarrow 0 < {vol}^{*} (A ∖ B) - u)$
54	53	biimpd	$⊢ ({vol}^{} (A ∖ B) \in ℝ \land u \in ℝ) \to (u < {vol}^{} (A ∖ B) \to 0 < {vol}^{*} (A ∖ B) - u)$
55	54	impr	$⊢ ({vol}^{} (A ∖ B) \in ℝ \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to 0 < {vol}^{*} (A ∖ B) - u$
56	51 55	elrpd	$⊢ ({vol}^{} (A ∖ B) \in ℝ \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to {vol}^{*} (A ∖ B) - u \in ℝ^{+}$
57		3nn	$⊢ 3 \in ℕ$
58		nnrp	$⊢ 3 \in ℕ \to 3 \in ℝ^{+}$
59	57 58	ax-mp	$⊢ 3 \in ℝ^{+}$
60		rpdivcl	$⊢ ({vol}^{} (A ∖ B) - u \in ℝ^{+} \land 3 \in ℝ^{+}) \to \frac{{vol}^{} (A ∖ B) - u}{3} \in ℝ^{+}$
61	56 59 60	sylancl	$⊢ ({vol}^{} (A ∖ B) \in ℝ \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to \frac{{vol}^{*} (A ∖ B) - u}{3} \in ℝ^{+}$
62	5 61	sylan	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to \frac{{vol}^{*} (A ∖ B) - u}{3} \in ℝ^{+}$
63	49 62	ltsubrpd	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < {vol}^{*} (A)$
64	63	adantr	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \to {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < {vol}^{} (A)$
65		simpr	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \to {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)$
66	64 65	breqtrd	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \to {vol}^{} (A) - (\frac{{vol}^{*} (A ∖ B) - u}{3}) < sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)$
67		reex	$⊢ ℝ \in V$
68	67	ssex	$⊢ A \subseteq ℝ \to A \in V$
69	68	adantr	$⊢ (A \subseteq ℝ \land {vol}^{*} (A) \in ℝ) \to A \in V$
70		sseq1	$⊢ v = A \to (v \subseteq ℝ \leftrightarrow A \subseteq ℝ)$
71		fveq2	$⊢ v = A \to {vol}^{} (v) = {vol}^{} (A)$
72	71	eleq1d	$⊢ v = A \to ({vol}^{} (v) \in ℝ \leftrightarrow {vol}^{} (A) \in ℝ)$
73	70 72	anbi12d	$⊢ v = A \to ((v \subseteq ℝ \land {vol}^{} (v) \in ℝ) \leftrightarrow (A \subseteq ℝ \land {vol}^{} (A) \in ℝ))$
74		sseq2	$⊢ v = A \to (b \subseteq v \leftrightarrow b \subseteq A)$
75	74	anbi1d	$⊢ v = A \to ((b \subseteq v \land y = vol (b)) \leftrightarrow (b \subseteq A \land y = vol (b)))$
76	75	rexbidv	$⊢ v = A \to (\exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b)) \leftrightarrow \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b)))$
77	76	abbidv	$⊢ v = A \to \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} = \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\}$
78	77	sseq1d	$⊢ v = A \to (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} \subseteq ℝ \leftrightarrow \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} \subseteq ℝ)$
79	77	neeq1d	$⊢ v = A \to (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} \neq \emptyset \leftrightarrow \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} \neq \emptyset)$
80	77	raleqdv	$⊢ v = A \to (\forall z \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} z \leq x \leftrightarrow \forall z \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} z \leq x)$
81	80	rexbidv	$⊢ v = A \to (\exists x \in ℝ \forall z \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} z \leq x \leftrightarrow \exists x \in ℝ \forall z \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} z \leq x)$
82	78 79 81	3anbi123d	$⊢ v = A \to ((\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} \subseteq ℝ \land \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} \neq \emptyset \land \exists x \in ℝ \forall z \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} z \leq x) \leftrightarrow (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} \subseteq ℝ \land \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} \neq \emptyset \land \exists x \in ℝ \forall z \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} z \leq x))$
83	73 82	imbi12d	$⊢ v = A \to (((v \subseteq ℝ \land {vol}^{} (v) \in ℝ) \to (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} \subseteq ℝ \land \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} \neq \emptyset \land \exists x \in ℝ \forall z \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} z \leq x)) \leftrightarrow ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} \subseteq ℝ \land \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} \neq \emptyset \land \exists x \in ℝ \forall z \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} z \leq x)))$
84		simpr	$⊢ (b \subseteq v \land y = vol (b)) \to y = vol (b)$
85	84 36	sylan9eqr	$⊢ (b \in Clsd (topGen (ran (.))) \land (b \subseteq v \land y = vol (b))) \to y = {vol}^{*} (b)$
86	85	adantl	$⊢ ((v \subseteq ℝ \land {vol}^{} (v) \in ℝ) \land (b \in Clsd (topGen (ran (.))) \land (b \subseteq v \land y = vol (b)))) \to y = {vol}^{} (b)$
87		simprl	$⊢ (b \in Clsd (topGen (ran (.))) \land (b \subseteq v \land y = vol (b))) \to b \subseteq v$
88		ovolsscl	$⊢ (b \subseteq v \land v \subseteq ℝ \land {vol}^{} (v) \in ℝ) \to {vol}^{} (b) \in ℝ$
89	88	3expb	$⊢ (b \subseteq v \land (v \subseteq ℝ \land {vol}^{} (v) \in ℝ)) \to {vol}^{} (b) \in ℝ$
90	89	ancoms	$⊢ ((v \subseteq ℝ \land {vol}^{} (v) \in ℝ) \land b \subseteq v) \to {vol}^{} (b) \in ℝ$
91	87 90	sylan2	$⊢ ((v \subseteq ℝ \land {vol}^{} (v) \in ℝ) \land (b \in Clsd (topGen (ran (.))) \land (b \subseteq v \land y = vol (b)))) \to {vol}^{} (b) \in ℝ$
92	86 91	eqeltrd	$⊢ ((v \subseteq ℝ \land {vol}^{*} (v) \in ℝ) \land (b \in Clsd (topGen (ran (.))) \land (b \subseteq v \land y = vol (b)))) \to y \in ℝ$
93	92	rexlimdvaa	$⊢ (v \subseteq ℝ \land {vol}^{*} (v) \in ℝ) \to (\exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b)) \to y \in ℝ)$
94	93	abssdv	$⊢ (v \subseteq ℝ \land {vol}^{*} (v) \in ℝ) \to \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} \subseteq ℝ$
95		retop	$⊢ topGen (ran (.)) \in Top$
96		0cld	$⊢ topGen (ran (.)) \in Top \to \emptyset \in Clsd (topGen (ran (.)))$
97	95 96	ax-mp	$⊢ \emptyset \in Clsd (topGen (ran (.)))$
98		0ss	$⊢ \emptyset \subseteq v$
99		0mbl	$⊢ \emptyset \in dom vol$
100		mblvol	$⊢ \emptyset \in dom vol \to vol (\emptyset) = {vol}^{*} (\emptyset)$
101	99 100	ax-mp	$⊢ vol (\emptyset) = {vol}^{*} (\emptyset)$
102		ovol0	$⊢ {vol}^{*} (\emptyset) = 0$
103	101 102	eqtr2i	$⊢ 0 = vol (\emptyset)$
104	98 103	pm3.2i	$⊢ (\emptyset \subseteq v \land 0 = vol (\emptyset))$
105		sseq1	$⊢ b = \emptyset \to (b \subseteq v \leftrightarrow \emptyset \subseteq v)$
106		fveq2	$⊢ b = \emptyset \to vol (b) = vol (\emptyset)$
107	106	eqeq2d	$⊢ b = \emptyset \to (0 = vol (b) \leftrightarrow 0 = vol (\emptyset))$
108	105 107	anbi12d	$⊢ b = \emptyset \to ((b \subseteq v \land 0 = vol (b)) \leftrightarrow (\emptyset \subseteq v \land 0 = vol (\emptyset)))$
109	108	rspcev	$⊢ (\emptyset \in Clsd (topGen (ran (.))) \land (\emptyset \subseteq v \land 0 = vol (\emptyset))) \to \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land 0 = vol (b))$
110	97 104 109	mp2an	$⊢ \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land 0 = vol (b))$
111		c0ex	$⊢ 0 \in V$
112		eqeq1	$⊢ y = 0 \to (y = vol (b) \leftrightarrow 0 = vol (b))$
113	112	anbi2d	$⊢ y = 0 \to ((b \subseteq v \land y = vol (b)) \leftrightarrow (b \subseteq v \land 0 = vol (b)))$
114	113	rexbidv	$⊢ y = 0 \to (\exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b)) \leftrightarrow \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land 0 = vol (b)))$
115	111 114	spcev	$⊢ \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land 0 = vol (b)) \to \exists y \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))$
116	110 115	ax-mp	$⊢ \exists y \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))$
117		abn0	$⊢ \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} \neq \emptyset \leftrightarrow \exists y \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))$
118	117	biimpri	$⊢ \exists y \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b)) \to \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} \neq \emptyset$
119	116 118	mp1i	$⊢ (v \subseteq ℝ \land {vol}^{*} (v) \in ℝ) \to \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} \neq \emptyset$
120		simpr	$⊢ (b \subseteq v \land z = vol (b)) \to z = vol (b)$
121	120 36	sylan9eqr	$⊢ (b \in Clsd (topGen (ran (.))) \land (b \subseteq v \land z = vol (b))) \to z = {vol}^{*} (b)$
122	121	adantl	$⊢ (v \subseteq ℝ \land (b \in Clsd (topGen (ran (.))) \land (b \subseteq v \land z = vol (b)))) \to z = {vol}^{*} (b)$
123		simprl	$⊢ (b \in Clsd (topGen (ran (.))) \land (b \subseteq v \land z = vol (b))) \to b \subseteq v$
124		ovolss	$⊢ (b \subseteq v \land v \subseteq ℝ) \to {vol}^{} (b) \leq {vol}^{} (v)$
125	124	ancoms	$⊢ (v \subseteq ℝ \land b \subseteq v) \to {vol}^{} (b) \leq {vol}^{} (v)$
126	123 125	sylan2	$⊢ (v \subseteq ℝ \land (b \in Clsd (topGen (ran (.))) \land (b \subseteq v \land z = vol (b)))) \to {vol}^{} (b) \leq {vol}^{} (v)$
127	122 126	eqbrtrd	$⊢ (v \subseteq ℝ \land (b \in Clsd (topGen (ran (.))) \land (b \subseteq v \land z = vol (b)))) \to z \leq {vol}^{*} (v)$
128	127	rexlimdvaa	$⊢ v \subseteq ℝ \to (\exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land z = vol (b)) \to z \leq {vol}^{*} (v))$
129	128	alrimiv	$⊢ v \subseteq ℝ \to \forall z (\exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land z = vol (b)) \to z \leq {vol}^{*} (v))$
130		eqeq1	$⊢ y = z \to (y = vol (b) \leftrightarrow z = vol (b))$
131	130	anbi2d	$⊢ y = z \to ((b \subseteq v \land y = vol (b)) \leftrightarrow (b \subseteq v \land z = vol (b)))$
132	131	rexbidv	$⊢ y = z \to (\exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b)) \leftrightarrow \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land z = vol (b)))$
133	132	ralab	$⊢ \forall z \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} z \leq {vol}^{} (v) \leftrightarrow \forall z (\exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land z = vol (b)) \to z \leq {vol}^{} (v))$
134	129 133	sylibr	$⊢ v \subseteq ℝ \to \forall z \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} z \leq {vol}^{*} (v)$
135		brralrspcev	$⊢ ({vol}^{} (v) \in ℝ \land \forall z \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} z \leq {vol}^{} (v)) \to \exists x \in ℝ \forall z \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} z \leq x$
136	134 135	sylan2	$⊢ ({vol}^{*} (v) \in ℝ \land v \subseteq ℝ) \to \exists x \in ℝ \forall z \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} z \leq x$
137	136	ancoms	$⊢ (v \subseteq ℝ \land {vol}^{*} (v) \in ℝ) \to \exists x \in ℝ \forall z \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} z \leq x$
138	94 119 137	3jca	$⊢ (v \subseteq ℝ \land {vol}^{*} (v) \in ℝ) \to (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} \subseteq ℝ \land \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} \neq \emptyset \land \exists x \in ℝ \forall z \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} z \leq x)$
139	83 138	vtoclg	$⊢ A \in V \to ((A \subseteq ℝ \land {vol}^{*} (A) \in ℝ) \to (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} \subseteq ℝ \land \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} \neq \emptyset \land \exists x \in ℝ \forall z \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} z \leq x))$
140	69 139	mpcom	$⊢ (A \subseteq ℝ \land {vol}^{*} (A) \in ℝ) \to (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} \subseteq ℝ \land \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} \neq \emptyset \land \exists x \in ℝ \forall z \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} z \leq x)$
141	140	adantr	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} \subseteq ℝ \land \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} \neq \emptyset \land \exists x \in ℝ \forall z \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} z \leq x)$
142	62	rpred	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to \frac{{vol}^{*} (A ∖ B) - u}{3} \in ℝ$
143	49 142	resubcld	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) \in ℝ$
144		suprlub	$⊢ ((\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} \subseteq ℝ \land \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} \neq \emptyset \land \exists x \in ℝ \forall z \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} z \leq x) \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) \in ℝ) \to ({vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <) \leftrightarrow \exists v \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < v)$
145	141 143 144	syl2anc	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to ({vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <) \leftrightarrow \exists v \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < v)$
146	145	adantr	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \to ({vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <) \leftrightarrow \exists v \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} {vol}^{} (A) - (\frac{{vol}^{*} (A ∖ B) - u}{3}) < v)$
147	66 146	mpbid	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \to \exists v \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} {vol}^{} (A) - (\frac{{vol}^{*} (A ∖ B) - u}{3}) < v$
148		eqeq1	$⊢ y = v \to (y = vol (b) \leftrightarrow v = vol (b))$
149	148	anbi2d	$⊢ y = v \to ((b \subseteq A \land y = vol (b)) \leftrightarrow (b \subseteq A \land v = vol (b)))$
150	149	rexbidv	$⊢ y = v \to (\exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b)) \leftrightarrow \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land v = vol (b)))$
151	150	rexab	$⊢ \exists v \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < v \leftrightarrow \exists v (\exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land v = vol (b)) \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < v)$
152		breq2	$⊢ v = vol (b) \to ({vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < v \leftrightarrow {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (b))$
153	152	ad2antll	$⊢ (b \in Clsd (topGen (ran (.))) \land (b \subseteq A \land v = vol (b))) \to ({vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < v \leftrightarrow {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (b))$
154		sseq1	$⊢ s = b \to (s \subseteq A \leftrightarrow b \subseteq A)$
155		fveq2	$⊢ s = b \to vol (s) = vol (b)$
156	155	breq2d	$⊢ s = b \to ({vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s) \leftrightarrow {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (b))$
157	154 156	anbi12d	$⊢ s = b \to ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \leftrightarrow (b \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (b)))$
158	157	rspcev	$⊢ (b \in Clsd (topGen (ran (.))) \land (b \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (b))) \to \exists s \in Clsd (topGen (ran (.))) (s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s))$
159	158	expr	$⊢ (b \in Clsd (topGen (ran (.))) \land b \subseteq A) \to ({vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (b) \to \exists s \in Clsd (topGen (ran (.))) (s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)))$
160	159	adantrr	$⊢ (b \in Clsd (topGen (ran (.))) \land (b \subseteq A \land v = vol (b))) \to ({vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (b) \to \exists s \in Clsd (topGen (ran (.))) (s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)))$
161	153 160	sylbid	$⊢ (b \in Clsd (topGen (ran (.))) \land (b \subseteq A \land v = vol (b))) \to ({vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < v \to \exists s \in Clsd (topGen (ran (.))) (s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)))$
162	161	rexlimiva	$⊢ \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land v = vol (b)) \to ({vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < v \to \exists s \in Clsd (topGen (ran (.))) (s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)))$
163	162	imp	$⊢ (\exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land v = vol (b)) \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < v) \to \exists s \in Clsd (topGen (ran (.))) (s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s))$
164	163	exlimiv	$⊢ \exists v (\exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land v = vol (b)) \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < v) \to \exists s \in Clsd (topGen (ran (.))) (s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s))$
165	151 164	sylbi	$⊢ \exists v \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < v \to \exists s \in Clsd (topGen (ran (.))) (s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s))$
166	147 165	syl	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \to \exists s \in Clsd (topGen (ran (.))) (s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{*} (A ∖ B) - u}{3}) < vol (s))$
167	166	ex	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to ({vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <) \to \exists s \in Clsd (topGen (ran (.))) (s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{*} (A ∖ B) - u}{3}) < vol (s)))$
168	167	adantlr	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to ({vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <) \to \exists s \in Clsd (topGen (ran (.))) (s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)))$
169		simplrr	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to {vol}^{} (B) \in ℝ$
170	62	adantlr	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to \frac{{vol}^{} (A ∖ B) - u}{3} \in ℝ^{+}$
171	169 170	ltsubrpd	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < {vol}^{} (B)$
172	171	adantr	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land {vol}^{} (B) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} ℝ <)) \to {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < {vol}^{*} (B)$
173		simpr	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land {vol}^{} (B) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} ℝ <)) \to {vol}^{*} (B) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} ℝ <)$
174	172 173	breqtrd	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land {vol}^{} (B) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} ℝ <)) \to {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} ℝ <)$
175	67	ssex	$⊢ B \subseteq ℝ \to B \in V$
176	175	adantr	$⊢ (B \subseteq ℝ \land {vol}^{*} (B) \in ℝ) \to B \in V$
177		sseq1	$⊢ v = B \to (v \subseteq ℝ \leftrightarrow B \subseteq ℝ)$
178		fveq2	$⊢ v = B \to {vol}^{} (v) = {vol}^{} (B)$
179	178	eleq1d	$⊢ v = B \to ({vol}^{} (v) \in ℝ \leftrightarrow {vol}^{} (B) \in ℝ)$
180	177 179	anbi12d	$⊢ v = B \to ((v \subseteq ℝ \land {vol}^{} (v) \in ℝ) \leftrightarrow (B \subseteq ℝ \land {vol}^{} (B) \in ℝ))$
181		sseq2	$⊢ v = B \to (b \subseteq v \leftrightarrow b \subseteq B)$
182	181	anbi1d	$⊢ v = B \to ((b \subseteq v \land y = vol (b)) \leftrightarrow (b \subseteq B \land y = vol (b)))$
183	182	rexbidv	$⊢ v = B \to (\exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b)) \leftrightarrow \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b)))$
184	183	abbidv	$⊢ v = B \to \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} = \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\}$
185	184	sseq1d	$⊢ v = B \to (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} \subseteq ℝ \leftrightarrow \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} \subseteq ℝ)$
186	184	neeq1d	$⊢ v = B \to (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} \neq \emptyset \leftrightarrow \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} \neq \emptyset)$
187	184	raleqdv	$⊢ v = B \to (\forall z \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} z \leq x \leftrightarrow \forall z \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} z \leq x)$
188	187	rexbidv	$⊢ v = B \to (\exists x \in ℝ \forall z \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} z \leq x \leftrightarrow \exists x \in ℝ \forall z \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} z \leq x)$
189	185 186 188	3anbi123d	$⊢ v = B \to ((\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} \subseteq ℝ \land \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} \neq \emptyset \land \exists x \in ℝ \forall z \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} z \leq x) \leftrightarrow (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} \subseteq ℝ \land \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} \neq \emptyset \land \exists x \in ℝ \forall z \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} z \leq x))$
190	180 189	imbi12d	$⊢ v = B \to (((v \subseteq ℝ \land {vol}^{} (v) \in ℝ) \to (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} \subseteq ℝ \land \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} \neq \emptyset \land \exists x \in ℝ \forall z \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq v \land y = vol (b))\} z \leq x)) \leftrightarrow ((B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \to (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} \subseteq ℝ \land \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} \neq \emptyset \land \exists x \in ℝ \forall z \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} z \leq x)))$
191	190 138	vtoclg	$⊢ B \in V \to ((B \subseteq ℝ \land {vol}^{*} (B) \in ℝ) \to (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} \subseteq ℝ \land \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} \neq \emptyset \land \exists x \in ℝ \forall z \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} z \leq x))$
192	176 191	mpcom	$⊢ (B \subseteq ℝ \land {vol}^{*} (B) \in ℝ) \to (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} \subseteq ℝ \land \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} \neq \emptyset \land \exists x \in ℝ \forall z \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} z \leq x)$
193	192	ad2antlr	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{*} (A ∖ B))) \to (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} \subseteq ℝ \land \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} \neq \emptyset \land \exists x \in ℝ \forall z \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} z \leq x)$
194	142	adantlr	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to \frac{{vol}^{} (A ∖ B) - u}{3} \in ℝ$
195	169 194	resubcld	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to {vol}^{} (B) - (\frac{{vol}^{*} (A ∖ B) - u}{3}) \in ℝ$
196		suprlub	$⊢ ((\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} \subseteq ℝ \land \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} \neq \emptyset \land \exists x \in ℝ \forall z \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} z \leq x) \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) \in ℝ) \to ({vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} ℝ <) \leftrightarrow \exists v \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < v)$
197	193 195 196	syl2anc	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to ({vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} ℝ <) \leftrightarrow \exists v \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} {vol}^{} (B) - (\frac{{vol}^{*} (A ∖ B) - u}{3}) < v)$
198	197	adantr	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land {vol}^{} (B) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} ℝ <)) \to ({vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} ℝ <) \leftrightarrow \exists v \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < v)$
199	174 198	mpbid	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land {vol}^{} (B) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} ℝ <)) \to \exists v \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < v$
200	148	anbi2d	$⊢ y = v \to ((b \subseteq B \land y = vol (b)) \leftrightarrow (b \subseteq B \land v = vol (b)))$
201	200	rexbidv	$⊢ y = v \to (\exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b)) \leftrightarrow \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land v = vol (b)))$
202	201	rexab	$⊢ \exists v \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < v \leftrightarrow \exists v (\exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land v = vol (b)) \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < v)$
203		breq2	$⊢ v = vol (b) \to ({vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < v \leftrightarrow {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (b))$
204	203	ad2antll	$⊢ (b \in Clsd (topGen (ran (.))) \land (b \subseteq B \land v = vol (b))) \to ({vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < v \leftrightarrow {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (b))$
205		sseq1	$⊢ w = b \to (w \subseteq B \leftrightarrow b \subseteq B)$
206		fveq2	$⊢ w = b \to vol (w) = vol (b)$
207	206	breq2d	$⊢ w = b \to ({vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w) \leftrightarrow {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (b))$
208	205 207	anbi12d	$⊢ w = b \to ((w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)) \leftrightarrow (b \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (b)))$
209	208	rspcev	$⊢ (b \in Clsd (topGen (ran (.))) \land (b \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (b))) \to \exists w \in Clsd (topGen (ran (.))) (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w))$
210	209	expr	$⊢ (b \in Clsd (topGen (ran (.))) \land b \subseteq B) \to ({vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (b) \to \exists w \in Clsd (topGen (ran (.))) (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))$
211	210	adantrr	$⊢ (b \in Clsd (topGen (ran (.))) \land (b \subseteq B \land v = vol (b))) \to ({vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (b) \to \exists w \in Clsd (topGen (ran (.))) (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))$
212	204 211	sylbid	$⊢ (b \in Clsd (topGen (ran (.))) \land (b \subseteq B \land v = vol (b))) \to ({vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < v \to \exists w \in Clsd (topGen (ran (.))) (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))$
213	212	rexlimiva	$⊢ \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land v = vol (b)) \to ({vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < v \to \exists w \in Clsd (topGen (ran (.))) (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))$
214	213	imp	$⊢ (\exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land v = vol (b)) \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < v) \to \exists w \in Clsd (topGen (ran (.))) (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w))$
215	214	exlimiv	$⊢ \exists v (\exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land v = vol (b)) \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < v) \to \exists w \in Clsd (topGen (ran (.))) (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w))$
216	202 215	sylbi	$⊢ \exists v \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < v \to \exists w \in Clsd (topGen (ran (.))) (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w))$
217	199 216	syl	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land {vol}^{} (B) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} ℝ <)) \to \exists w \in Clsd (topGen (ran (.))) (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w))$
218	217	ex	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to ({vol}^{} (B) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} ℝ <) \to \exists w \in Clsd (topGen (ran (.))) (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))$
219	168 218	anim12d	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to (({vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <) \land {vol}^{} (B) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} ℝ <)) \to (\exists s \in Clsd (topGen (ran (.))) (s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land \exists w \in Clsd (topGen (ran (.))) (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{*} (A ∖ B) - u}{3}) < vol (w))))$
220		reeanv	$⊢ \exists s \in Clsd (topGen (ran (.))) \exists w \in Clsd (topGen (ran (.))) ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w))) \leftrightarrow (\exists s \in Clsd (topGen (ran (.))) (s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land \exists w \in Clsd (topGen (ran (.))) (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))$
221	219 220	syl6ibr	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to (({vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <) \land {vol}^{} (B) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} ℝ <)) \to \exists s \in Clsd (topGen (ran (.))) \exists w \in Clsd (topGen (ran (.))) ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{*} (A ∖ B) - u}{3}) < vol (w))))$
222		eqid	$⊢ seq 1 (+ ((abs \circ -) \circ f)) = seq 1 (+ ((abs \circ -) \circ f))$
223	222	ovolgelb	$⊢ (B \subseteq ℝ \land {vol}^{} (B) \in ℝ \land \frac{{vol}^{} (A ∖ B) - u}{3} \in ℝ^{+}) \to \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (B \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (B) + (\frac{{vol}^{*} (A ∖ B) - u}{3}))$
224	223	3expa	$⊢ ((B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land \frac{{vol}^{} (A ∖ B) - u}{3} \in ℝ^{+}) \to \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (B \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (B) + (\frac{{vol}^{*} (A ∖ B) - u}{3}))$
225	62 224	sylan2	$⊢ ((B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (u \in ℝ \land u < {vol}^{} (A ∖ B)))) \to \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (B \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))$
226	225	ancoms	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \to \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (B \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))$
227	226	an32s	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (B \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))$
228		elmapi	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to f : ℕ ⟶ \leq \cap ℝ^{2}$
229		ssid	$⊢ ⋃ ran ((.) \circ f) \subseteq ⋃ ran ((.) \circ f)$
230	222	ovollb	$⊢ (f : ℕ ⟶ \leq \cap ℝ^{2} \land ⋃ ran ((.) \circ f) \subseteq ⋃ ran ((.) \circ f)) \to {vol}^{} (⋃ ran ((.) \circ f)) \leq sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <)$
231	229 230	mpan2	$⊢ f : ℕ ⟶ \leq \cap ℝ^{2} \to {vol}^{} (⋃ ran ((.) \circ f)) \leq sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <)$
232	231	adantl	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land f : ℕ ⟶ \leq \cap ℝ^{2}) \to {vol}^{} (⋃ ran ((.) \circ f)) \leq sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <)$
233		eqid	$⊢ (abs \circ -) \circ f = (abs \circ -) \circ f$
234	233 222	ovolsf	$⊢ f : ℕ ⟶ \leq \cap ℝ^{2} \to seq 1 (+ ((abs \circ -) \circ f)) : ℕ ⟶ [0, +∞)$
235		frn	$⊢ seq 1 (+ ((abs \circ -) \circ f)) : ℕ ⟶ [0, +∞) \to ran seq 1 (+ ((abs \circ -) \circ f)) \subseteq [0, +∞)$
236		icossxr	$⊢ [0, +∞) \subseteq ℝ^{*}$
237	235 236	sstrdi	$⊢ seq 1 (+ ((abs \circ -) \circ f)) : ℕ ⟶ [0, +∞) \to ran seq 1 (+ ((abs \circ -) \circ f)) \subseteq ℝ^{*}$
238		supxrcl	$⊢ ran seq 1 (+ ((abs \circ -) \circ f)) \subseteq ℝ^{} \to sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \in ℝ^{*}$
239	234 237 238	3syl	$⊢ f : ℕ ⟶ \leq \cap ℝ^{2} \to sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \in ℝ^{}$
240		simpr	$⊢ (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \to {vol}^{} (B) \in ℝ$
241		readdcl	$⊢ ({vol}^{} (B) \in ℝ \land \frac{{vol}^{} (A ∖ B) - u}{3} \in ℝ) \to {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}) \in ℝ$
242	240 142 241	syl2anr	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \to {vol}^{} (B) + (\frac{{vol}^{*} (A ∖ B) - u}{3}) \in ℝ$
243	242	rexrd	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \to {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}) \in ℝ^{}$
244	243	an32s	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}) \in ℝ^{}$
245		rncoss	$⊢ ran ((.) \circ f) \subseteq ran (.)$
246	245	unissi	$⊢ ⋃ ran ((.) \circ f) \subseteq ⋃ ran (.)$
247		unirnioo	$⊢ ℝ = ⋃ ran (.)$
248	246 247	sseqtrri	$⊢ ⋃ ran ((.) \circ f) \subseteq ℝ$
249		ovolcl	$⊢ ⋃ ran ((.) \circ f) \subseteq ℝ \to {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ^{}$
250	248 249	ax-mp	$⊢ {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ^{}$
251		xrletr	$⊢ ({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ^{} \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \in ℝ^{} \land {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}) \in ℝ^{}) \to (({vol}^{} (⋃ ran ((.) \circ f)) \leq sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3})) \to {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{*} (A ∖ B) - u}{3}))$
252	250 251	mp3an1	$⊢ (sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \in ℝ^{} \land {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}) \in ℝ^{}) \to (({vol}^{} (⋃ ran ((.) \circ f)) \leq sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3})) \to {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{*} (A ∖ B) - u}{3}))$
253	239 244 252	syl2anr	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land f : ℕ ⟶ \leq \cap ℝ^{2}) \to (({vol}^{} (⋃ ran ((.) \circ f)) \leq sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3})) \to {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{*} (A ∖ B) - u}{3}))$
254	232 253	mpand	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land f : ℕ ⟶ \leq \cap ℝ^{2}) \to (sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}) \to {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{*} (A ∖ B) - u}{3}))$
255	228 254	sylan2	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \to (sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}) \to {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{*} (A ∖ B) - u}{3}))$
256	255	anim2d	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \to ((B \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3})) \to (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{*} (A ∖ B) - u}{3})))$
257	256	reximdva	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to (\exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (B \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3})) \to \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{*} (A ∖ B) - u}{3})))$
258	227 257	mpd	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))$
259		rexex	$⊢ \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3})) \to \exists f (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))$
260	258 259	syl	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to \exists f (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))$
261	16	cldss	$⊢ s \in Clsd (topGen (ran (.))) \to s \subseteq ℝ$
262		indif2	$⊢ s \cap (ℝ ∖ ⋃ ran ((.) \circ f)) = (s \cap ℝ) ∖ ⋃ ran ((.) \circ f)$
263		df-ss	$⊢ s \subseteq ℝ \leftrightarrow s \cap ℝ = s$
264	263	biimpi	$⊢ s \subseteq ℝ \to s \cap ℝ = s$
265	264	difeq1d	$⊢ s \subseteq ℝ \to (s \cap ℝ) ∖ ⋃ ran ((.) \circ f) = s ∖ ⋃ ran ((.) \circ f)$
266	262 265	syl5eq	$⊢ s \subseteq ℝ \to s \cap (ℝ ∖ ⋃ ran ((.) \circ f)) = s ∖ ⋃ ran ((.) \circ f)$
267	261 266	syl	$⊢ s \in Clsd (topGen (ran (.))) \to s \cap (ℝ ∖ ⋃ ran ((.) \circ f)) = s ∖ ⋃ ran ((.) \circ f)$
268		retopbas	$⊢ ran (.) \in TopBases$
269		bastg	$⊢ ran (.) \in TopBases \to ran (.) \subseteq topGen (ran (.))$
270	268 269	ax-mp	$⊢ ran (.) \subseteq topGen (ran (.))$
271	245 270	sstri	$⊢ ran ((.) \circ f) \subseteq topGen (ran (.))$
272		uniopn	$⊢ (topGen (ran (.)) \in Top \land ran ((.) \circ f) \subseteq topGen (ran (.))) \to ⋃ ran ((.) \circ f) \in topGen (ran (.))$
273	95 271 272	mp2an	$⊢ ⋃ ran ((.) \circ f) \in topGen (ran (.))$
274	16	opncld	$⊢ (topGen (ran (.)) \in Top \land ⋃ ran ((.) \circ f) \in topGen (ran (.))) \to ℝ ∖ ⋃ ran ((.) \circ f) \in Clsd (topGen (ran (.)))$
275	95 273 274	mp2an	$⊢ ℝ ∖ ⋃ ran ((.) \circ f) \in Clsd (topGen (ran (.)))$
276		incld	$⊢ (s \in Clsd (topGen (ran (.))) \land ℝ ∖ ⋃ ran ((.) \circ f) \in Clsd (topGen (ran (.)))) \to s \cap (ℝ ∖ ⋃ ran ((.) \circ f)) \in Clsd (topGen (ran (.)))$
277	275 276	mpan2	$⊢ s \in Clsd (topGen (ran (.))) \to s \cap (ℝ ∖ ⋃ ran ((.) \circ f)) \in Clsd (topGen (ran (.)))$
278	267 277	eqeltrrd	$⊢ s \in Clsd (topGen (ran (.))) \to s ∖ ⋃ ran ((.) \circ f) \in Clsd (topGen (ran (.)))$
279	278	adantr	$⊢ (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.)))) \to s ∖ ⋃ ran ((.) \circ f) \in Clsd (topGen (ran (.)))$
280	279	ad2antlr	$⊢ (((B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3})) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{*} (A ∖ B) - u}{3}) < vol (w)))) \to s ∖ ⋃ ran ((.) \circ f) \in Clsd (topGen (ran (.)))$
281		simprll	$⊢ (((B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3})) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{*} (A ∖ B) - u}{3}) < vol (w)))) \to s \subseteq A$
282		simplll	$⊢ (((B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3})) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{*} (A ∖ B) - u}{3}) < vol (w)))) \to B \subseteq ⋃ ran ((.) \circ f)$
283	281 282	ssdif2d	$⊢ (((B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3})) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{*} (A ∖ B) - u}{3}) < vol (w)))) \to s ∖ ⋃ ran ((.) \circ f) \subseteq A ∖ B$
284		fveq2	$⊢ s ∖ ⋃ ran ((.) \circ f) = b \to vol (s ∖ ⋃ ran ((.) \circ f)) = vol (b)$
285	284	eqcoms	$⊢ b = s ∖ ⋃ ran ((.) \circ f) \to vol (s ∖ ⋃ ran ((.) \circ f)) = vol (b)$
286	285	biantrud	$⊢ b = s ∖ ⋃ ran ((.) \circ f) \to (b \subseteq A ∖ B \leftrightarrow (b \subseteq A ∖ B \land vol (s ∖ ⋃ ran ((.) \circ f)) = vol (b)))$
287		sseq1	$⊢ b = s ∖ ⋃ ran ((.) \circ f) \to (b \subseteq A ∖ B \leftrightarrow s ∖ ⋃ ran ((.) \circ f) \subseteq A ∖ B)$
288	286 287	bitr3d	$⊢ b = s ∖ ⋃ ran ((.) \circ f) \to ((b \subseteq A ∖ B \land vol (s ∖ ⋃ ran ((.) \circ f)) = vol (b)) \leftrightarrow s ∖ ⋃ ran ((.) \circ f) \subseteq A ∖ B)$
289	288	rspcev	$⊢ (s ∖ ⋃ ran ((.) \circ f) \in Clsd (topGen (ran (.))) \land s ∖ ⋃ ran ((.) \circ f) \subseteq A ∖ B) \to \exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land vol (s ∖ ⋃ ran ((.) \circ f)) = vol (b))$
290	280 283 289	syl2anc	$⊢ (((B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3})) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{*} (A ∖ B) - u}{3}) < vol (w)))) \to \exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land vol (s ∖ ⋃ ran ((.) \circ f)) = vol (b))$
291	290	adantlll	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to \exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land vol (s ∖ ⋃ ran ((.) \circ f)) = vol (b))$
292		difss	$⊢ (A ∖ B) ∖ (s ∖ ⋃ ran ((.) \circ f)) \subseteq A ∖ B$
293	292 3	sstri	$⊢ (A ∖ B) ∖ (s ∖ ⋃ ran ((.) \circ f)) \subseteq A$
294		ovolsscl	$⊢ ((A ∖ B) ∖ (s ∖ ⋃ ran ((.) \circ f)) \subseteq A \land A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} ((A ∖ B) ∖ (s ∖ ⋃ ran ((.) \circ f))) \in ℝ$
295	293 294	mp3an1	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} ((A ∖ B) ∖ (s ∖ ⋃ ran ((.) \circ f))) \in ℝ$
296	295	ad5antr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{*} ((A ∖ B) ∖ (s ∖ ⋃ ran ((.) \circ f))) \in ℝ$
297	5	ad5antr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{*} (A ∖ B) \in ℝ$
298		simpl	$⊢ (u \in ℝ \land u < {vol}^{*} (A ∖ B)) \to u \in ℝ$
299	298	ad4antlr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to u \in ℝ$
300		difdif2	$⊢ (A ∖ B) ∖ (s ∖ ⋃ ran ((.) \circ f)) = ((A ∖ B) ∖ s) \cup ((A ∖ B) \cap ⋃ ran ((.) \circ f))$
301	300	fveq2i	$⊢ {vol}^{} ((A ∖ B) ∖ (s ∖ ⋃ ran ((.) \circ f))) = {vol}^{} (((A ∖ B) ∖ s) \cup ((A ∖ B) \cap ⋃ ran ((.) \circ f)))$
302		difss	$⊢ (A ∖ B) ∖ s \subseteq A ∖ B$
303	302 3	sstri	$⊢ (A ∖ B) ∖ s \subseteq A$
304		inss1	$⊢ (A ∖ B) \cap ⋃ ran ((.) \circ f) \subseteq A ∖ B$
305	304 3	sstri	$⊢ (A ∖ B) \cap ⋃ ran ((.) \circ f) \subseteq A$
306	303 305	unssi	$⊢ ((A ∖ B) ∖ s) \cup ((A ∖ B) \cap ⋃ ran ((.) \circ f)) \subseteq A$
307		ovolsscl	$⊢ (((A ∖ B) ∖ s) \cup ((A ∖ B) \cap ⋃ ran ((.) \circ f)) \subseteq A \land A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} (((A ∖ B) ∖ s) \cup ((A ∖ B) \cap ⋃ ran ((.) \circ f))) \in ℝ$
308	306 307	mp3an1	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} (((A ∖ B) ∖ s) \cup ((A ∖ B) \cap ⋃ ran ((.) \circ f))) \in ℝ$
309	308	ad5antr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{*} (((A ∖ B) ∖ s) \cup ((A ∖ B) \cap ⋃ ran ((.) \circ f))) \in ℝ$
310		difss	$⊢ A ∖ s \subseteq A$
311		ovolsscl	$⊢ (A ∖ s \subseteq A \land A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} (A ∖ s) \in ℝ$
312	310 311	mp3an1	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} (A ∖ s) \in ℝ$
313	312	ad5antr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{*} (A ∖ s) \in ℝ$
314	169 194	readdcld	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to {vol}^{} (B) + (\frac{{vol}^{*} (A ∖ B) - u}{3}) \in ℝ$
315	314 250	jctil	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to ({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ^{} \land {vol}^{} (B) + (\frac{{vol}^{*} (A ∖ B) - u}{3}) \in ℝ)$
316		simpr	$⊢ (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3})) \to {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3})$
317		ovolge0	$⊢ ⋃ ran ((.) \circ f) \subseteq ℝ \to 0 \leq {vol}^{*} (⋃ ran ((.) \circ f))$
318	248 317	ax-mp	$⊢ 0 \leq {vol}^{*} (⋃ ran ((.) \circ f))$
319	316 318	jctil	$⊢ (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3})) \to (0 \leq {vol}^{} (⋃ ran ((.) \circ f)) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{*} (A ∖ B) - u}{3}))$
320		xrrege0	$⊢ (({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ^{} \land {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}) \in ℝ) \land (0 \leq {vol}^{} (⋃ ran ((.) \circ f)) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \to {vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ$
321	315 319 320	syl2an	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \to {vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ$
322		difss	$⊢ ⋃ ran ((.) \circ f) ∖ w \subseteq ⋃ ran ((.) \circ f)$
323		ovolsscl	$⊢ (⋃ ran ((.) \circ f) ∖ w \subseteq ⋃ ran ((.) \circ f) \land ⋃ ran ((.) \circ f) \subseteq ℝ \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{} (⋃ ran ((.) \circ f) ∖ w) \in ℝ$
324	322 248 323	mp3an12	$⊢ {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \to {vol}^{} (⋃ ran ((.) \circ f) ∖ w) \in ℝ$
325	321 324	syl	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \to {vol}^{*} (⋃ ran ((.) \circ f) ∖ w) \in ℝ$
326	325	ad2antrr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{*} (⋃ ran ((.) \circ f) ∖ w) \in ℝ$
327	313 326	readdcld	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{} (A ∖ s) + {vol}^{} (⋃ ran ((.) \circ f) ∖ w) \in ℝ$
328	5 50	sylan	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land u \in ℝ) \to {vol}^{} (A ∖ B) - u \in ℝ$
329	328	adantrr	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to {vol}^{*} (A ∖ B) - u \in ℝ$
330	329	adantlr	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to {vol}^{} (A ∖ B) - u \in ℝ$
331	330	ad3antrrr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{*} (A ∖ B) - u \in ℝ$
332		ssdifss	$⊢ A \subseteq ℝ \to A ∖ s \subseteq ℝ$
333	322 248	sstri	$⊢ ⋃ ran ((.) \circ f) ∖ w \subseteq ℝ$
334		unss	$⊢ (A ∖ s \subseteq ℝ \land ⋃ ran ((.) \circ f) ∖ w \subseteq ℝ) \leftrightarrow (A ∖ s) \cup (⋃ ran ((.) \circ f) ∖ w) \subseteq ℝ$
335	332 333 334	sylanblc	$⊢ A \subseteq ℝ \to (A ∖ s) \cup (⋃ ran ((.) \circ f) ∖ w) \subseteq ℝ$
336		ovolcl	$⊢ (A ∖ s) \cup (⋃ ran ((.) \circ f) ∖ w) \subseteq ℝ \to {vol}^{} ((A ∖ s) \cup (⋃ ran ((.) \circ f) ∖ w)) \in ℝ^{}$
337	335 336	syl	$⊢ A \subseteq ℝ \to {vol}^{} ((A ∖ s) \cup (⋃ ran ((.) \circ f) ∖ w)) \in ℝ^{}$
338	337	ad4antr	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \to {vol}^{} ((A ∖ s) \cup (⋃ ran ((.) \circ f) ∖ w)) \in ℝ^{}$
339	312	ad3antrrr	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \to {vol}^{*} (A ∖ s) \in ℝ$
340	339 325	readdcld	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \to {vol}^{} (A ∖ s) + {vol}^{} (⋃ ran ((.) \circ f) ∖ w) \in ℝ$
341		ovolge0	$⊢ (A ∖ s) \cup (⋃ ran ((.) \circ f) ∖ w) \subseteq ℝ \to 0 \leq {vol}^{*} ((A ∖ s) \cup (⋃ ran ((.) \circ f) ∖ w))$
342	335 341	syl	$⊢ A \subseteq ℝ \to 0 \leq {vol}^{*} ((A ∖ s) \cup (⋃ ran ((.) \circ f) ∖ w))$
343	342	ad4antr	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \to 0 \leq {vol}^{*} ((A ∖ s) \cup (⋃ ran ((.) \circ f) ∖ w))$
344	332	adantr	$⊢ (A \subseteq ℝ \land {vol}^{*} (A) \in ℝ) \to A ∖ s \subseteq ℝ$
345	344 312	jca	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to (A ∖ s \subseteq ℝ \land {vol}^{} (A ∖ s) \in ℝ)$
346	345	ad3antrrr	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \to (A ∖ s \subseteq ℝ \land {vol}^{*} (A ∖ s) \in ℝ)$
347	325 333	jctil	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \to (⋃ ran ((.) \circ f) ∖ w \subseteq ℝ \land {vol}^{*} (⋃ ran ((.) \circ f) ∖ w) \in ℝ)$
348		ovolun	$⊢ ((A ∖ s \subseteq ℝ \land {vol}^{} (A ∖ s) \in ℝ) \land (⋃ ran ((.) \circ f) ∖ w \subseteq ℝ \land {vol}^{} (⋃ ran ((.) \circ f) ∖ w) \in ℝ)) \to {vol}^{} ((A ∖ s) \cup (⋃ ran ((.) \circ f) ∖ w)) \leq {vol}^{} (A ∖ s) + {vol}^{*} (⋃ ran ((.) \circ f) ∖ w)$
349	346 347 348	syl2anc	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \to {vol}^{} ((A ∖ s) \cup (⋃ ran ((.) \circ f) ∖ w)) \leq {vol}^{} (A ∖ s) + {vol}^{*} (⋃ ran ((.) \circ f) ∖ w)$
350		xrrege0	$⊢ (({vol}^{} ((A ∖ s) \cup (⋃ ran ((.) \circ f) ∖ w)) \in ℝ^{} \land {vol}^{} (A ∖ s) + {vol}^{} (⋃ ran ((.) \circ f) ∖ w) \in ℝ) \land (0 \leq {vol}^{} ((A ∖ s) \cup (⋃ ran ((.) \circ f) ∖ w)) \land {vol}^{} ((A ∖ s) \cup (⋃ ran ((.) \circ f) ∖ w)) \leq {vol}^{} (A ∖ s) + {vol}^{} (⋃ ran ((.) \circ f) ∖ w))) \to {vol}^{*} ((A ∖ s) \cup (⋃ ran ((.) \circ f) ∖ w)) \in ℝ$
351	338 340 343 349 350	syl22anc	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \to {vol}^{*} ((A ∖ s) \cup (⋃ ran ((.) \circ f) ∖ w)) \in ℝ$
352	351	ad2antrr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{*} ((A ∖ s) \cup (⋃ ran ((.) \circ f) ∖ w)) \in ℝ$
353		ssdif	$⊢ A ∖ B \subseteq A \to (A ∖ B) ∖ s \subseteq A ∖ s$
354	3 353	ax-mp	$⊢ (A ∖ B) ∖ s \subseteq A ∖ s$
355		incom	$⊢ (A ∖ B) \cap ⋃ ran ((.) \circ f) = ⋃ ran ((.) \circ f) \cap (A ∖ B)$
356		indif2	$⊢ ⋃ ran ((.) \circ f) \cap (A ∖ B) = (⋃ ran ((.) \circ f) \cap A) ∖ B$
357	355 356	eqtri	$⊢ (A ∖ B) \cap ⋃ ran ((.) \circ f) = (⋃ ran ((.) \circ f) \cap A) ∖ B$
358		inss1	$⊢ ⋃ ran ((.) \circ f) \cap A \subseteq ⋃ ran ((.) \circ f)$
359	358	a1i	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to ⋃ ran ((.) \circ f) \cap A \subseteq ⋃ ran ((.) \circ f)$
360		simprrl	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to w \subseteq B$
361	359 360	ssdif2d	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to (⋃ ran ((.) \circ f) \cap A) ∖ B \subseteq ⋃ ran ((.) \circ f) ∖ w$
362	357 361	eqsstrid	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to (A ∖ B) \cap ⋃ ran ((.) \circ f) \subseteq ⋃ ran ((.) \circ f) ∖ w$
363		unss12	$⊢ ((A ∖ B) ∖ s \subseteq A ∖ s \land (A ∖ B) \cap ⋃ ran ((.) \circ f) \subseteq ⋃ ran ((.) \circ f) ∖ w) \to ((A ∖ B) ∖ s) \cup ((A ∖ B) \cap ⋃ ran ((.) \circ f)) \subseteq (A ∖ s) \cup (⋃ ran ((.) \circ f) ∖ w)$
364	354 362 363	sylancr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to ((A ∖ B) ∖ s) \cup ((A ∖ B) \cap ⋃ ran ((.) \circ f)) \subseteq (A ∖ s) \cup (⋃ ran ((.) \circ f) ∖ w)$
365	335	ad6antr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to (A ∖ s) \cup (⋃ ran ((.) \circ f) ∖ w) \subseteq ℝ$
366		ovolss	$⊢ (((A ∖ B) ∖ s) \cup ((A ∖ B) \cap ⋃ ran ((.) \circ f)) \subseteq (A ∖ s) \cup (⋃ ran ((.) \circ f) ∖ w) \land (A ∖ s) \cup (⋃ ran ((.) \circ f) ∖ w) \subseteq ℝ) \to {vol}^{} (((A ∖ B) ∖ s) \cup ((A ∖ B) \cap ⋃ ran ((.) \circ f))) \leq {vol}^{} ((A ∖ s) \cup (⋃ ran ((.) \circ f) ∖ w))$
367	364 365 366	syl2anc	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{} (((A ∖ B) ∖ s) \cup ((A ∖ B) \cap ⋃ ran ((.) \circ f))) \leq {vol}^{} ((A ∖ s) \cup (⋃ ran ((.) \circ f) ∖ w))$
368	332	ad6antr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to A ∖ s \subseteq ℝ$
369	326 333	jctil	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to (⋃ ran ((.) \circ f) ∖ w \subseteq ℝ \land {vol}^{*} (⋃ ran ((.) \circ f) ∖ w) \in ℝ)$
370	368 313 369 348	syl21anc	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{} ((A ∖ s) \cup (⋃ ran ((.) \circ f) ∖ w)) \leq {vol}^{} (A ∖ s) + {vol}^{*} (⋃ ran ((.) \circ f) ∖ w)$
371	309 352 327 367 370	letrd	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{} (((A ∖ B) ∖ s) \cup ((A ∖ B) \cap ⋃ ran ((.) \circ f))) \leq {vol}^{} (A ∖ s) + {vol}^{*} (⋃ ran ((.) \circ f) ∖ w)$
372	194	ad3antrrr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to \frac{{vol}^{*} (A ∖ B) - u}{3} \in ℝ$
373	194 194	readdcld	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to (\frac{{vol}^{} (A ∖ B) - u}{3}) + (\frac{{vol}^{*} (A ∖ B) - u}{3}) \in ℝ$
374	373	ad3antrrr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to (\frac{{vol}^{} (A ∖ B) - u}{3}) + (\frac{{vol}^{} (A ∖ B) - u}{3}) \in ℝ$
375		eleq1w	$⊢ b = s \to (b \in dom vol \leftrightarrow s \in dom vol)$
376	375 34	vtoclga	$⊢ s \in Clsd (topGen (ran (.))) \to s \in dom vol$
377		mblvol	$⊢ s \in dom vol \to vol (s) = {vol}^{*} (s)$
378	376 377	syl	$⊢ s \in Clsd (topGen (ran (.))) \to vol (s) = {vol}^{*} (s)$
379	378	adantr	$⊢ (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.)))) \to vol (s) = {vol}^{*} (s)$
380		sseqin2	$⊢ s \subseteq A \leftrightarrow A \cap s = s$
381	380	biimpi	$⊢ s \subseteq A \to A \cap s = s$
382	381	eqcomd	$⊢ s \subseteq A \to s = A \cap s$
383	382	fveq2d	$⊢ s \subseteq A \to {vol}^{} (s) = {vol}^{} (A \cap s)$
384	383	ad2antrr	$⊢ ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w))) \to {vol}^{} (s) = {vol}^{} (A \cap s)$
385	379 384	sylan9eq	$⊢ ((s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.)))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to vol (s) = {vol}^{*} (A \cap s)$
386	385	oveq2d	$⊢ ((s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.)))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{} (A) - vol (s) = {vol}^{} (A) - {vol}^{*} (A \cap s)$
387	386	adantll	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{} (A) - vol (s) = {vol}^{} (A) - {vol}^{*} (A \cap s)$
388	376	adantr	$⊢ (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.)))) \to s \in dom vol$
389		simplll	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \to (A \subseteq ℝ \land {vol}^{*} (A) \in ℝ)$
390		mblsplit	$⊢ (s \in dom vol \land A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} (A) = {vol}^{} (A \cap s) + {vol}^{} (A ∖ s)$
391	390	eqcomd	$⊢ (s \in dom vol \land A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} (A \cap s) + {vol}^{} (A ∖ s) = {vol}^{} (A)$
392	391	3expb	$⊢ (s \in dom vol \land (A \subseteq ℝ \land {vol}^{} (A) \in ℝ)) \to {vol}^{} (A \cap s) + {vol}^{} (A ∖ s) = {vol}^{} (A)$
393	388 389 392	syl2anr	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \to {vol}^{} (A \cap s) + {vol}^{} (A ∖ s) = {vol}^{*} (A)$
394	393	adantr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{} (A \cap s) + {vol}^{} (A ∖ s) = {vol}^{*} (A)$
395		simp-6r	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{*} (A) \in ℝ$
396	395	recnd	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{*} (A) \in ℂ$
397		inss1	$⊢ A \cap s \subseteq A$
398		ovolsscl	$⊢ (A \cap s \subseteq A \land A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} (A \cap s) \in ℝ$
399	397 398	mp3an1	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} (A \cap s) \in ℝ$
400	399	recnd	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} (A \cap s) \in ℂ$
401	400	ad5antr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{*} (A \cap s) \in ℂ$
402	312	recnd	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} (A ∖ s) \in ℂ$
403	402	ad5antr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{*} (A ∖ s) \in ℂ$
404	396 401 403	subaddd	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to ({vol}^{} (A) - {vol}^{} (A \cap s) = {vol}^{} (A ∖ s) \leftrightarrow {vol}^{} (A \cap s) + {vol}^{} (A ∖ s) = {vol}^{} (A))$
405	394 404	mpbird	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{} (A) - {vol}^{} (A \cap s) = {vol}^{*} (A ∖ s)$
406	387 405	eqtrd	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{} (A) - vol (s) = {vol}^{} (A ∖ s)$
407	379	ad2antlr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to vol (s) = {vol}^{*} (s)$
408		simpll	$⊢ ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w))) \to s \subseteq A$
409		simp-4l	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \to (A \subseteq ℝ \land {vol}^{*} (A) \in ℝ)$
410		ovolsscl	$⊢ (s \subseteq A \land A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} (s) \in ℝ$
411	410	3expb	$⊢ (s \subseteq A \land (A \subseteq ℝ \land {vol}^{} (A) \in ℝ)) \to {vol}^{} (s) \in ℝ$
412	408 409 411	syl2anr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{*} (s) \in ℝ$
413	407 412	eqeltrd	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to vol (s) \in ℝ$
414		simprlr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)$
415	395 372 413 414	ltsub23d	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{} (A) - vol (s) < \frac{{vol}^{} (A ∖ B) - u}{3}$
416	406 415	eqbrtrrd	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{} (A ∖ s) < \frac{{vol}^{} (A ∖ B) - u}{3}$
417	321	recnd	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \to {vol}^{*} (⋃ ran ((.) \circ f)) \in ℂ$
418	417	ad2antrr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{*} (⋃ ran ((.) \circ f)) \in ℂ$
419	240	ad5antlr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{*} (B) \in ℝ$
420	419	recnd	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{*} (B) \in ℂ$
421		eleq1w	$⊢ b = w \to (b \in dom vol \leftrightarrow w \in dom vol)$
422	421 34	vtoclga	$⊢ w \in Clsd (topGen (ran (.))) \to w \in dom vol$
423		mblvol	$⊢ w \in dom vol \to vol (w) = {vol}^{*} (w)$
424	422 423	syl	$⊢ w \in Clsd (topGen (ran (.))) \to vol (w) = {vol}^{*} (w)$
425	424	adantl	$⊢ (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.)))) \to vol (w) = {vol}^{*} (w)$
426	425	ad2antlr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to vol (w) = {vol}^{*} (w)$
427		simprl	$⊢ ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w))) \to w \subseteq B$
428		simp-4r	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \to (B \subseteq ℝ \land {vol}^{*} (B) \in ℝ)$
429		ovolsscl	$⊢ (w \subseteq B \land B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \to {vol}^{} (w) \in ℝ$
430	429	3expb	$⊢ (w \subseteq B \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \to {vol}^{} (w) \in ℝ$
431	427 428 430	syl2anr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{*} (w) \in ℝ$
432	426 431	eqeltrd	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to vol (w) \in ℝ$
433	432	recnd	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to vol (w) \in ℂ$
434	418 420 433	npncand	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to ({vol}^{} (⋃ ran ((.) \circ f)) - {vol}^{} (B)) + {vol}^{} (B) - vol (w) = {vol}^{} (⋃ ran ((.) \circ f)) - vol (w)$
435		simplrl	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \to B \subseteq ⋃ ran ((.) \circ f)$
436	427 435	sylan9ssr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to w \subseteq ⋃ ran ((.) \circ f)$
437		sseqin2	$⊢ w \subseteq ⋃ ran ((.) \circ f) \leftrightarrow ⋃ ran ((.) \circ f) \cap w = w$
438	436 437	sylib	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to ⋃ ran ((.) \circ f) \cap w = w$
439	438	fveq2d	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{} (⋃ ran ((.) \circ f) \cap w) = {vol}^{} (w)$
440	426 439	eqtr4d	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to vol (w) = {vol}^{*} (⋃ ran ((.) \circ f) \cap w)$
441	440	oveq2d	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{} (⋃ ran ((.) \circ f)) - vol (w) = {vol}^{} (⋃ ran ((.) \circ f)) - {vol}^{*} (⋃ ran ((.) \circ f) \cap w)$
442	422	adantl	$⊢ (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.)))) \to w \in dom vol$
443	321 248	jctil	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \to (⋃ ran ((.) \circ f) \subseteq ℝ \land {vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ)$
444		mblsplit	$⊢ (w \in dom vol \land ⋃ ran ((.) \circ f) \subseteq ℝ \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{} (⋃ ran ((.) \circ f)) = {vol}^{} (⋃ ran ((.) \circ f) \cap w) + {vol}^{} (⋃ ran ((.) \circ f) ∖ w)$
445	444	eqcomd	$⊢ (w \in dom vol \land ⋃ ran ((.) \circ f) \subseteq ℝ \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{} (⋃ ran ((.) \circ f) \cap w) + {vol}^{} (⋃ ran ((.) \circ f) ∖ w) = {vol}^{} (⋃ ran ((.) \circ f))$
446	445	3expb	$⊢ (w \in dom vol \land (⋃ ran ((.) \circ f) \subseteq ℝ \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ)) \to {vol}^{} (⋃ ran ((.) \circ f) \cap w) + {vol}^{} (⋃ ran ((.) \circ f) ∖ w) = {vol}^{} (⋃ ran ((.) \circ f))$
447	442 443 446	syl2anr	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \to {vol}^{} (⋃ ran ((.) \circ f) \cap w) + {vol}^{} (⋃ ran ((.) \circ f) ∖ w) = {vol}^{*} (⋃ ran ((.) \circ f))$
448	447	adantr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{} (⋃ ran ((.) \circ f) \cap w) + {vol}^{} (⋃ ran ((.) \circ f) ∖ w) = {vol}^{*} (⋃ ran ((.) \circ f))$
449		inss1	$⊢ ⋃ ran ((.) \circ f) \cap w \subseteq ⋃ ran ((.) \circ f)$
450		ovolsscl	$⊢ (⋃ ran ((.) \circ f) \cap w \subseteq ⋃ ran ((.) \circ f) \land ⋃ ran ((.) \circ f) \subseteq ℝ \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{} (⋃ ran ((.) \circ f) \cap w) \in ℝ$
451	449 248 450	mp3an12	$⊢ {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \to {vol}^{} (⋃ ran ((.) \circ f) \cap w) \in ℝ$
452	321 451	syl	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \to {vol}^{*} (⋃ ran ((.) \circ f) \cap w) \in ℝ$
453	452	recnd	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \to {vol}^{*} (⋃ ran ((.) \circ f) \cap w) \in ℂ$
454	325	recnd	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \to {vol}^{*} (⋃ ran ((.) \circ f) ∖ w) \in ℂ$
455	417 453 454	subaddd	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \to ({vol}^{} (⋃ ran ((.) \circ f)) - {vol}^{} (⋃ ran ((.) \circ f) \cap w) = {vol}^{} (⋃ ran ((.) \circ f) ∖ w) \leftrightarrow {vol}^{} (⋃ ran ((.) \circ f) \cap w) + {vol}^{} (⋃ ran ((.) \circ f) ∖ w) = {vol}^{} (⋃ ran ((.) \circ f)))$
456	455	ad2antrr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to ({vol}^{} (⋃ ran ((.) \circ f)) - {vol}^{} (⋃ ran ((.) \circ f) \cap w) = {vol}^{} (⋃ ran ((.) \circ f) ∖ w) \leftrightarrow {vol}^{} (⋃ ran ((.) \circ f) \cap w) + {vol}^{} (⋃ ran ((.) \circ f) ∖ w) = {vol}^{} (⋃ ran ((.) \circ f)))$
457	448 456	mpbird	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{} (⋃ ran ((.) \circ f)) - {vol}^{} (⋃ ran ((.) \circ f) \cap w) = {vol}^{*} (⋃ ran ((.) \circ f) ∖ w)$
458	434 441 457	3eqtrd	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to ({vol}^{} (⋃ ran ((.) \circ f)) - {vol}^{} (B)) + {vol}^{} (B) - vol (w) = {vol}^{} (⋃ ran ((.) \circ f) ∖ w)$
459	240	ad3antlr	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \to {vol}^{*} (B) \in ℝ$
460	321 459	resubcld	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \to {vol}^{} (⋃ ran ((.) \circ f)) - {vol}^{} (B) \in ℝ$
461	460	ad2antrr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{} (⋃ ran ((.) \circ f)) - {vol}^{} (B) \in ℝ$
462	419 432	resubcld	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{*} (B) - vol (w) \in ℝ$
463		simprr	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \to {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{*} (A ∖ B) - u}{3})$
464	194	adantr	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \to \frac{{vol}^{*} (A ∖ B) - u}{3} \in ℝ$
465	321 459 464	lesubadd2d	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \to ({vol}^{} (⋃ ran ((.) \circ f)) - {vol}^{} (B) \leq \frac{{vol}^{} (A ∖ B) - u}{3} \leftrightarrow {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))$
466	463 465	mpbird	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \to {vol}^{} (⋃ ran ((.) \circ f)) - {vol}^{} (B) \leq \frac{{vol}^{*} (A ∖ B) - u}{3}$
467	466	ad2antrr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{} (⋃ ran ((.) \circ f)) - {vol}^{} (B) \leq \frac{{vol}^{*} (A ∖ B) - u}{3}$
468		simprrr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)$
469	419 372 432 468	ltsub23d	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{} (B) - vol (w) < \frac{{vol}^{} (A ∖ B) - u}{3}$
470	461 462 372 372 467 469	leltaddd	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to ({vol}^{} (⋃ ran ((.) \circ f)) - {vol}^{} (B)) + {vol}^{} (B) - vol (w) < (\frac{{vol}^{} (A ∖ B) - u}{3}) + (\frac{{vol}^{*} (A ∖ B) - u}{3})$
471	458 470	eqbrtrrd	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{} (⋃ ran ((.) \circ f) ∖ w) < (\frac{{vol}^{} (A ∖ B) - u}{3}) + (\frac{{vol}^{*} (A ∖ B) - u}{3})$
472	313 326 372 374 416 471	lt2addd	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{} (A ∖ s) + {vol}^{} (⋃ ran ((.) \circ f) ∖ w) < (\frac{{vol}^{} (A ∖ B) - u}{3}) + (\frac{{vol}^{} (A ∖ B) - u}{3}) + (\frac{{vol}^{*} (A ∖ B) - u}{3})$
473		df-3	$⊢ 3 = 2 + 1$
474		2cn	$⊢ 2 \in ℂ$
475		ax-1cn	$⊢ 1 \in ℂ$
476	474 475	addcomi	$⊢ 2 + 1 = 1 + 2$
477	473 476	eqtri	$⊢ 3 = 1 + 2$
478	477	oveq1i	$⊢ 3 (\frac{{vol}^{} (A ∖ B) - u}{3}) = (1 + 2) (\frac{{vol}^{} (A ∖ B) - u}{3})$
479	62	rpcnd	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to \frac{{vol}^{*} (A ∖ B) - u}{3} \in ℂ$
480		adddir	$⊢ (1 \in ℂ \land 2 \in ℂ \land \frac{{vol}^{} (A ∖ B) - u}{3} \in ℂ) \to (1 + 2) (\frac{{vol}^{} (A ∖ B) - u}{3}) = 1 (\frac{{vol}^{} (A ∖ B) - u}{3}) + 2 (\frac{{vol}^{} (A ∖ B) - u}{3})$
481	475 474 480	mp3an12	$⊢ \frac{{vol}^{} (A ∖ B) - u}{3} \in ℂ \to (1 + 2) (\frac{{vol}^{} (A ∖ B) - u}{3}) = 1 (\frac{{vol}^{} (A ∖ B) - u}{3}) + 2 (\frac{{vol}^{} (A ∖ B) - u}{3})$
482	479 481	syl	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to (1 + 2) (\frac{{vol}^{} (A ∖ B) - u}{3}) = 1 (\frac{{vol}^{} (A ∖ B) - u}{3}) + 2 (\frac{{vol}^{*} (A ∖ B) - u}{3})$
483	479	mulid2d	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to 1 (\frac{{vol}^{} (A ∖ B) - u}{3}) = \frac{{vol}^{} (A ∖ B) - u}{3}$
484	479	2timesd	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to 2 (\frac{{vol}^{} (A ∖ B) - u}{3}) = (\frac{{vol}^{} (A ∖ B) - u}{3}) + (\frac{{vol}^{*} (A ∖ B) - u}{3})$
485	483 484	oveq12d	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to 1 (\frac{{vol}^{} (A ∖ B) - u}{3}) + 2 (\frac{{vol}^{} (A ∖ B) - u}{3}) = (\frac{{vol}^{} (A ∖ B) - u}{3}) + (\frac{{vol}^{} (A ∖ B) - u}{3}) + (\frac{{vol}^{*} (A ∖ B) - u}{3})$
486	482 485	eqtrd	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to (1 + 2) (\frac{{vol}^{} (A ∖ B) - u}{3}) = (\frac{{vol}^{} (A ∖ B) - u}{3}) + (\frac{{vol}^{} (A ∖ B) - u}{3}) + (\frac{{vol}^{} (A ∖ B) - u}{3})$
487	478 486	syl5eq	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to 3 (\frac{{vol}^{} (A ∖ B) - u}{3}) = (\frac{{vol}^{} (A ∖ B) - u}{3}) + (\frac{{vol}^{} (A ∖ B) - u}{3}) + (\frac{{vol}^{} (A ∖ B) - u}{3})$
488	329	recnd	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to {vol}^{*} (A ∖ B) - u \in ℂ$
489		3cn	$⊢ 3 \in ℂ$
490		3ne0	$⊢ 3 \neq 0$
491		divcan2	$⊢ ({vol}^{} (A ∖ B) - u \in ℂ \land 3 \in ℂ \land 3 \neq 0) \to 3 (\frac{{vol}^{} (A ∖ B) - u}{3}) = {vol}^{*} (A ∖ B) - u$
492	489 490 491	mp3an23	$⊢ {vol}^{} (A ∖ B) - u \in ℂ \to 3 (\frac{{vol}^{} (A ∖ B) - u}{3}) = {vol}^{*} (A ∖ B) - u$
493	488 492	syl	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to 3 (\frac{{vol}^{} (A ∖ B) - u}{3}) = {vol}^{} (A ∖ B) - u$
494	487 493	eqtr3d	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to (\frac{{vol}^{} (A ∖ B) - u}{3}) + (\frac{{vol}^{} (A ∖ B) - u}{3}) + (\frac{{vol}^{} (A ∖ B) - u}{3}) = {vol}^{} (A ∖ B) - u$
495	494	adantlr	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to (\frac{{vol}^{} (A ∖ B) - u}{3}) + (\frac{{vol}^{} (A ∖ B) - u}{3}) + (\frac{{vol}^{} (A ∖ B) - u}{3}) = {vol}^{*} (A ∖ B) - u$
496	495	ad3antrrr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to (\frac{{vol}^{} (A ∖ B) - u}{3}) + (\frac{{vol}^{} (A ∖ B) - u}{3}) + (\frac{{vol}^{} (A ∖ B) - u}{3}) = {vol}^{} (A ∖ B) - u$
497	472 496	breqtrd	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{} (A ∖ s) + {vol}^{} (⋃ ran ((.) \circ f) ∖ w) < {vol}^{*} (A ∖ B) - u$
498	309 327 331 371 497	lelttrd	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{} (((A ∖ B) ∖ s) \cup ((A ∖ B) \cap ⋃ ran ((.) \circ f))) < {vol}^{} (A ∖ B) - u$
499	301 498	eqbrtrid	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{} ((A ∖ B) ∖ (s ∖ ⋃ ran ((.) \circ f))) < {vol}^{} (A ∖ B) - u$
500	296 297 299 499	ltsub13d	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to u < {vol}^{} (A ∖ B) - {vol}^{} ((A ∖ B) ∖ (s ∖ ⋃ ran ((.) \circ f)))$
501	283	adantlll	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to s ∖ ⋃ ran ((.) \circ f) \subseteq A ∖ B$
502		sseqin2	$⊢ s ∖ ⋃ ran ((.) \circ f) \subseteq A ∖ B \leftrightarrow (A ∖ B) \cap (s ∖ ⋃ ran ((.) \circ f)) = s ∖ ⋃ ran ((.) \circ f)$
503	501 502	sylib	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to (A ∖ B) \cap (s ∖ ⋃ ran ((.) \circ f)) = s ∖ ⋃ ran ((.) \circ f)$
504	503	fveq2d	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{} ((A ∖ B) \cap (s ∖ ⋃ ran ((.) \circ f))) = {vol}^{} (s ∖ ⋃ ran ((.) \circ f))$
505		opnmbl	$⊢ ⋃ ran ((.) \circ f) \in topGen (ran (.)) \to ⋃ ran ((.) \circ f) \in dom vol$
506	273 505	ax-mp	$⊢ ⋃ ran ((.) \circ f) \in dom vol$
507		difmbl	$⊢ (s \in dom vol \land ⋃ ran ((.) \circ f) \in dom vol) \to s ∖ ⋃ ran ((.) \circ f) \in dom vol$
508	376 506 507	sylancl	$⊢ s \in Clsd (topGen (ran (.))) \to s ∖ ⋃ ran ((.) \circ f) \in dom vol$
509	508	adantr	$⊢ (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.)))) \to s ∖ ⋃ ran ((.) \circ f) \in dom vol$
510	509	ad2antlr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to s ∖ ⋃ ran ((.) \circ f) \in dom vol$
511	13	adantr	$⊢ (A \subseteq ℝ \land {vol}^{*} (A) \in ℝ) \to A ∖ B \subseteq ℝ$
512	511 5	jca	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to (A ∖ B \subseteq ℝ \land {vol}^{} (A ∖ B) \in ℝ)$
513	512	ad5antr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to (A ∖ B \subseteq ℝ \land {vol}^{*} (A ∖ B) \in ℝ)$
514		mblsplit	$⊢ (s ∖ ⋃ ran ((.) \circ f) \in dom vol \land A ∖ B \subseteq ℝ \land {vol}^{} (A ∖ B) \in ℝ) \to {vol}^{} (A ∖ B) = {vol}^{} ((A ∖ B) \cap (s ∖ ⋃ ran ((.) \circ f))) + {vol}^{} ((A ∖ B) ∖ (s ∖ ⋃ ran ((.) \circ f)))$
515	514	3expb	$⊢ (s ∖ ⋃ ran ((.) \circ f) \in dom vol \land (A ∖ B \subseteq ℝ \land {vol}^{} (A ∖ B) \in ℝ)) \to {vol}^{} (A ∖ B) = {vol}^{} ((A ∖ B) \cap (s ∖ ⋃ ran ((.) \circ f))) + {vol}^{} ((A ∖ B) ∖ (s ∖ ⋃ ran ((.) \circ f)))$
516	515	eqcomd	$⊢ (s ∖ ⋃ ran ((.) \circ f) \in dom vol \land (A ∖ B \subseteq ℝ \land {vol}^{} (A ∖ B) \in ℝ)) \to {vol}^{} ((A ∖ B) \cap (s ∖ ⋃ ran ((.) \circ f))) + {vol}^{} ((A ∖ B) ∖ (s ∖ ⋃ ran ((.) \circ f))) = {vol}^{} (A ∖ B)$
517	510 513 516	syl2anc	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{} ((A ∖ B) \cap (s ∖ ⋃ ran ((.) \circ f))) + {vol}^{} ((A ∖ B) ∖ (s ∖ ⋃ ran ((.) \circ f))) = {vol}^{*} (A ∖ B)$
518	297	recnd	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{*} (A ∖ B) \in ℂ$
519	296	recnd	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{*} ((A ∖ B) ∖ (s ∖ ⋃ ran ((.) \circ f))) \in ℂ$
520		inss1	$⊢ (A ∖ B) \cap (s ∖ ⋃ ran ((.) \circ f)) \subseteq A ∖ B$
521	520 3	sstri	$⊢ (A ∖ B) \cap (s ∖ ⋃ ran ((.) \circ f)) \subseteq A$
522		ovolsscl	$⊢ ((A ∖ B) \cap (s ∖ ⋃ ran ((.) \circ f)) \subseteq A \land A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} ((A ∖ B) \cap (s ∖ ⋃ ran ((.) \circ f))) \in ℝ$
523	521 522	mp3an1	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} ((A ∖ B) \cap (s ∖ ⋃ ran ((.) \circ f))) \in ℝ$
524	523	ad5antr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{*} ((A ∖ B) \cap (s ∖ ⋃ ran ((.) \circ f))) \in ℝ$
525	524	recnd	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{*} ((A ∖ B) \cap (s ∖ ⋃ ran ((.) \circ f))) \in ℂ$
526	518 519 525	subadd2d	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to ({vol}^{} (A ∖ B) - {vol}^{} ((A ∖ B) ∖ (s ∖ ⋃ ran ((.) \circ f))) = {vol}^{} ((A ∖ B) \cap (s ∖ ⋃ ran ((.) \circ f))) \leftrightarrow {vol}^{} ((A ∖ B) \cap (s ∖ ⋃ ran ((.) \circ f))) + {vol}^{} ((A ∖ B) ∖ (s ∖ ⋃ ran ((.) \circ f))) = {vol}^{} (A ∖ B))$
527	517 526	mpbird	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to {vol}^{} (A ∖ B) - {vol}^{} ((A ∖ B) ∖ (s ∖ ⋃ ran ((.) \circ f))) = {vol}^{*} ((A ∖ B) \cap (s ∖ ⋃ ran ((.) \circ f)))$
528		mblvol	$⊢ s ∖ ⋃ ran ((.) \circ f) \in dom vol \to vol (s ∖ ⋃ ran ((.) \circ f)) = {vol}^{*} (s ∖ ⋃ ran ((.) \circ f))$
529	507 528	syl	$⊢ (s \in dom vol \land ⋃ ran ((.) \circ f) \in dom vol) \to vol (s ∖ ⋃ ran ((.) \circ f)) = {vol}^{*} (s ∖ ⋃ ran ((.) \circ f))$
530	376 506 529	sylancl	$⊢ s \in Clsd (topGen (ran (.))) \to vol (s ∖ ⋃ ran ((.) \circ f)) = {vol}^{*} (s ∖ ⋃ ran ((.) \circ f))$
531	530	adantr	$⊢ (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.)))) \to vol (s ∖ ⋃ ran ((.) \circ f)) = {vol}^{*} (s ∖ ⋃ ran ((.) \circ f))$
532	531	ad2antlr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to vol (s ∖ ⋃ ran ((.) \circ f)) = {vol}^{*} (s ∖ ⋃ ran ((.) \circ f))$
533	504 527 532	3eqtr4rd	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to vol (s ∖ ⋃ ran ((.) \circ f)) = {vol}^{} (A ∖ B) - {vol}^{} ((A ∖ B) ∖ (s ∖ ⋃ ran ((.) \circ f)))$
534	500 533	breqtrrd	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to u < vol (s ∖ ⋃ ran ((.) \circ f))$
535		fvex	$⊢ vol (s ∖ ⋃ ran ((.) \circ f)) \in V$
536		eqeq1	$⊢ v = vol (s ∖ ⋃ ran ((.) \circ f)) \to (v = vol (b) \leftrightarrow vol (s ∖ ⋃ ran ((.) \circ f)) = vol (b))$
537	536	anbi2d	$⊢ v = vol (s ∖ ⋃ ran ((.) \circ f)) \to ((b \subseteq A ∖ B \land v = vol (b)) \leftrightarrow (b \subseteq A ∖ B \land vol (s ∖ ⋃ ran ((.) \circ f)) = vol (b)))$
538	537	rexbidv	$⊢ v = vol (s ∖ ⋃ ran ((.) \circ f)) \to (\exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land v = vol (b)) \leftrightarrow \exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land vol (s ∖ ⋃ ran ((.) \circ f)) = vol (b)))$
539		breq2	$⊢ v = vol (s ∖ ⋃ ran ((.) \circ f)) \to (u < v \leftrightarrow u < vol (s ∖ ⋃ ran ((.) \circ f)))$
540	538 539	anbi12d	$⊢ v = vol (s ∖ ⋃ ran ((.) \circ f)) \to ((\exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land v = vol (b)) \land u < v) \leftrightarrow (\exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land vol (s ∖ ⋃ ran ((.) \circ f)) = vol (b)) \land u < vol (s ∖ ⋃ ran ((.) \circ f))))$
541	535 540	spcev	$⊢ (\exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land vol (s ∖ ⋃ ran ((.) \circ f)) = vol (b)) \land u < vol (s ∖ ⋃ ran ((.) \circ f))) \to \exists v (\exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land v = vol (b)) \land u < v)$
542	291 534 541	syl2anc	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to \exists v (\exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land v = vol (b)) \land u < v)$
543	148	anbi2d	$⊢ y = v \to ((b \subseteq A ∖ B \land y = vol (b)) \leftrightarrow (b \subseteq A ∖ B \land v = vol (b)))$
544	543	rexbidv	$⊢ y = v \to (\exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land y = vol (b)) \leftrightarrow \exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land v = vol (b)))$
545	544	rexab	$⊢ \exists v \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land y = vol (b))\} u < v \leftrightarrow \exists v (\exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land v = vol (b)) \land u < v)$
546	542 545	sylibr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \land ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w)))) \to \exists v \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land y = vol (b))\} u < v$
547	546	ex	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \land (s \in Clsd (topGen (ran (.))) \land w \in Clsd (topGen (ran (.))))) \to (((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w))) \to \exists v \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land y = vol (b))\} u < v)$
548	547	rexlimdvva	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \land (B \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (B) + (\frac{{vol}^{} (A ∖ B) - u}{3}))) \to (\exists s \in Clsd (topGen (ran (.))) \exists w \in Clsd (topGen (ran (.))) ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (w))) \to \exists v \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land y = vol (b))\} u < v)$
549	260 548	exlimddv	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to (\exists s \in Clsd (topGen (ran (.))) \exists w \in Clsd (topGen (ran (.))) ((s \subseteq A \land {vol}^{} (A) - (\frac{{vol}^{} (A ∖ B) - u}{3}) < vol (s)) \land (w \subseteq B \land {vol}^{} (B) - (\frac{{vol}^{*} (A ∖ B) - u}{3}) < vol (w))) \to \exists v \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land y = vol (b))\} u < v)$
550	221 549	syld	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land (u \in ℝ \land u < {vol}^{} (A ∖ B))) \to (({vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <) \land {vol}^{*} (B) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} ℝ <)) \to \exists v \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land y = vol (b))\} u < v)$
551	550	exp31	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to ((B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \to ((u \in ℝ \land u < {vol}^{} (A ∖ B)) \to (({vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <) \land {vol}^{*} (B) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} ℝ <)) \to \exists v \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land y = vol (b))\} u < v)))$
552	551	com34	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to ((B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \to (({vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <) \land {vol}^{} (B) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} ℝ <)) \to ((u \in ℝ \land u < {vol}^{*} (A ∖ B)) \to \exists v \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land y = vol (b))\} u < v)))$
553	552	3imp1	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land ({vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <) \land {vol}^{} (B) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} ℝ <))) \land (u \in ℝ \land u < {vol}^{*} (A ∖ B))) \to \exists v \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land y = vol (b))\} u < v$
554	2 6 48 553	eqsupd	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land ({vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <) \land {vol}^{} (B) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq B \land y = vol (b))\} ℝ <))) \to sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A ∖ B \land y = vol (b))\} ℝ <) = {vol}^{*} (A ∖ B)$

Metamath Proof Explorer

Theorem mblfinlem3

Proof