mblfinlem4

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

Proof

Step	Hyp	Ref	Expression
1		ltso	$⊢ < Or ℝ$
2	1	a1i	$⊢ ((A \subseteq ℝ \land {vol}^{*} (A) \in ℝ) \land A \in dom vol) \to < Or ℝ$
3		simplr	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \to {vol}^{} (A) \in ℝ$
4		vex	$⊢ u \in V$
5		eqeq1	$⊢ y = u \to (y = vol (b) \leftrightarrow u = vol (b))$
6	5	anbi2d	$⊢ y = u \to ((b \subseteq A \land y = vol (b)) \leftrightarrow (b \subseteq A \land u = vol (b)))$
7	6	rexbidv	$⊢ y = u \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 u = vol (b)))$
8	4 7	elab	$⊢ u \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} \leftrightarrow \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land u = vol (b))$
9		simprl	$⊢ (b \in Clsd (topGen (ran (.))) \land (b \subseteq A \land u = vol (b))) \to b \subseteq A$
10		ovolss	$⊢ (b \subseteq A \land A \subseteq ℝ) \to {vol}^{} (b) \leq {vol}^{} (A)$
11		sstr	$⊢ (b \subseteq A \land A \subseteq ℝ) \to b \subseteq ℝ$
12		ovolcl	$⊢ b \subseteq ℝ \to {vol}^{} (b) \in ℝ^{}$
13	11 12	syl	$⊢ (b \subseteq A \land A \subseteq ℝ) \to {vol}^{} (b) \in ℝ^{}$
14		ovolcl	$⊢ A \subseteq ℝ \to {vol}^{} (A) \in ℝ^{}$
15	14	adantl	$⊢ (b \subseteq A \land A \subseteq ℝ) \to {vol}^{} (A) \in ℝ^{}$
16		xrlenlt	$⊢ ({vol}^{} (b) \in ℝ^{} \land {vol}^{} (A) \in ℝ^{}) \to ({vol}^{} (b) \leq {vol}^{} (A) \leftrightarrow \neg {vol}^{} (A) < {vol}^{} (b))$
17	13 15 16	syl2anc	$⊢ (b \subseteq A \land A \subseteq ℝ) \to ({vol}^{} (b) \leq {vol}^{} (A) \leftrightarrow \neg {vol}^{} (A) < {vol}^{} (b))$
18	10 17	mpbid	$⊢ (b \subseteq A \land A \subseteq ℝ) \to \neg {vol}^{} (A) < {vol}^{} (b)$
19	18	ancoms	$⊢ (A \subseteq ℝ \land b \subseteq A) \to \neg {vol}^{} (A) < {vol}^{} (b)$
20	9 19	sylan2	$⊢ (A \subseteq ℝ \land (b \in Clsd (topGen (ran (.))) \land (b \subseteq A \land u = vol (b)))) \to \neg {vol}^{} (A) < {vol}^{} (b)$
21		simprrr	$⊢ (A \subseteq ℝ \land (b \in Clsd (topGen (ran (.))) \land (b \subseteq A \land u = vol (b)))) \to u = vol (b)$
22		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
23	22	cldss	$⊢ b \in Clsd (topGen (ran (.))) \to b \subseteq ℝ$
24		dfss4	$⊢ b \subseteq ℝ \leftrightarrow ℝ ∖ (ℝ ∖ b) = b$
25	23 24	sylib	$⊢ b \in Clsd (topGen (ran (.))) \to ℝ ∖ (ℝ ∖ b) = b$
26		rembl	$⊢ ℝ \in dom vol$
27	22	cldopn	$⊢ b \in Clsd (topGen (ran (.))) \to ℝ ∖ b \in topGen (ran (.))$
28		opnmbl	$⊢ ℝ ∖ b \in topGen (ran (.)) \to ℝ ∖ b \in dom vol$
29	27 28	syl	$⊢ b \in Clsd (topGen (ran (.))) \to ℝ ∖ b \in dom vol$
30		difmbl	$⊢ (ℝ \in dom vol \land ℝ ∖ b \in dom vol) \to ℝ ∖ (ℝ ∖ b) \in dom vol$
31	26 29 30	sylancr	$⊢ b \in Clsd (topGen (ran (.))) \to ℝ ∖ (ℝ ∖ b) \in dom vol$
32	25 31	eqeltrrd	$⊢ b \in Clsd (topGen (ran (.))) \to b \in dom vol$
33		mblvol	$⊢ b \in dom vol \to vol (b) = {vol}^{*} (b)$
34	32 33	syl	$⊢ b \in Clsd (topGen (ran (.))) \to vol (b) = {vol}^{*} (b)$
35	34	ad2antrl	$⊢ (A \subseteq ℝ \land (b \in Clsd (topGen (ran (.))) \land (b \subseteq A \land u = vol (b)))) \to vol (b) = {vol}^{*} (b)$
36	21 35	eqtrd	$⊢ (A \subseteq ℝ \land (b \in Clsd (topGen (ran (.))) \land (b \subseteq A \land u = vol (b)))) \to u = {vol}^{*} (b)$
37	36	breq2d	$⊢ (A \subseteq ℝ \land (b \in Clsd (topGen (ran (.))) \land (b \subseteq A \land u = vol (b)))) \to ({vol}^{} (A) < u \leftrightarrow {vol}^{} (A) < {vol}^{*} (b))$
38	20 37	mtbird	$⊢ (A \subseteq ℝ \land (b \in Clsd (topGen (ran (.))) \land (b \subseteq A \land u = vol (b)))) \to \neg {vol}^{*} (A) < u$
39	38	rexlimdvaa	$⊢ A \subseteq ℝ \to (\exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land u = vol (b)) \to \neg {vol}^{*} (A) < u)$
40	8 39	biimtrid	$⊢ A \subseteq ℝ \to (u \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} \to \neg {vol}^{*} (A) < u)$
41	40	ad2antrr	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \to (u \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} \to \neg {vol}^{} (A) < u)$
42	41	imp	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land u \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\}) \to \neg {vol}^{} (A) < u$
43		1rp	$⊢ 1 \in ℝ^{+}$
44		eqid	$⊢ seq 1 (+ ((abs \circ -) \circ f)) = seq 1 (+ ((abs \circ -) \circ f))$
45	44	ovolgelb	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ \land 1 \in ℝ^{+}) \to \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{*} (A) + 1)$
46	43 45	mp3an3	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{*} (A) + 1)$
47		elmapi	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to f : ℕ ⟶ \leq \cap ℝ^{2}$
48		ssid	$⊢ ⋃ ran ((.) \circ f) \subseteq ⋃ ran ((.) \circ f)$
49	44	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)) ℝ^{} <)$
50	48 49	mpan2	$⊢ f : ℕ ⟶ \leq \cap ℝ^{2} \to {vol}^{} (⋃ ran ((.) \circ f)) \leq sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <)$
51	50	adantl	$⊢ ({vol}^{} (A) \in ℝ \land f : ℕ ⟶ \leq \cap ℝ^{2}) \to {vol}^{} (⋃ ran ((.) \circ f)) \leq sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <)$
52		eqid	$⊢ (abs \circ -) \circ f = (abs \circ -) \circ f$
53	52 44	ovolsf	$⊢ f : ℕ ⟶ \leq \cap ℝ^{2} \to seq 1 (+ ((abs \circ -) \circ f)) : ℕ ⟶ [0, +∞)$
54		frn	$⊢ seq 1 (+ ((abs \circ -) \circ f)) : ℕ ⟶ [0, +∞) \to ran seq 1 (+ ((abs \circ -) \circ f)) \subseteq [0, +∞)$
55		icossxr	$⊢ [0, +∞) \subseteq ℝ^{*}$
56	54 55	sstrdi	$⊢ seq 1 (+ ((abs \circ -) \circ f)) : ℕ ⟶ [0, +∞) \to ran seq 1 (+ ((abs \circ -) \circ f)) \subseteq ℝ^{*}$
57		supxrcl	$⊢ ran seq 1 (+ ((abs \circ -) \circ f)) \subseteq ℝ^{} \to sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \in ℝ^{*}$
58	53 56 57	3syl	$⊢ f : ℕ ⟶ \leq \cap ℝ^{2} \to sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \in ℝ^{}$
59		peano2re	$⊢ {vol}^{} (A) \in ℝ \to {vol}^{} (A) + 1 \in ℝ$
60	59	rexrd	$⊢ {vol}^{} (A) \in ℝ \to {vol}^{} (A) + 1 \in ℝ^{*}$
61		rncoss	$⊢ ran ((.) \circ f) \subseteq ran (.)$
62	61	unissi	$⊢ ⋃ ran ((.) \circ f) \subseteq ⋃ ran (.)$
63		unirnioo	$⊢ ℝ = ⋃ ran (.)$
64	62 63	sseqtrri	$⊢ ⋃ ran ((.) \circ f) \subseteq ℝ$
65		ovolcl	$⊢ ⋃ ran ((.) \circ f) \subseteq ℝ \to {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ^{}$
66	64 65	ax-mp	$⊢ {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ^{}$
67		xrletr	$⊢ ({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ^{} \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \in ℝ^{} \land {vol}^{} (A) + 1 \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}^{} (A) + 1) \to {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)$
68	66 67	mp3an1	$⊢ (sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \in ℝ^{} \land {vol}^{} (A) + 1 \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}^{} (A) + 1) \to {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)$
69	58 60 68	syl2anr	$⊢ ({vol}^{} (A) \in ℝ \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}^{} (A) + 1) \to {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{*} (A) + 1)$
70	51 69	mpand	$⊢ ({vol}^{} (A) \in ℝ \land f : ℕ ⟶ \leq \cap ℝ^{2}) \to (sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (A) + 1 \to {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{*} (A) + 1)$
71	70	adantll	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land f : ℕ ⟶ \leq \cap ℝ^{2}) \to (sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (A) + 1 \to {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{*} (A) + 1)$
72	47 71	sylan2	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \to (sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (A) + 1 \to {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{*} (A) + 1)$
73	72	anim2d	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \to ((A \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (A) + 1) \to (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{*} (A) + 1))$
74	73	reximdva	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to (\exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (A) + 1) \to \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{*} (A) + 1))$
75	46 74	mpd	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{*} (A) + 1)$
76		rexex	$⊢ \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1) \to \exists f (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)$
77	75 76	syl	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to \exists f (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{*} (A) + 1)$
78	77	ad2antrr	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \to \exists f (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)$
79		difss	$⊢ ⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ f)$
80	79 64	sstri	$⊢ ⋃ ran ((.) \circ f) ∖ A \subseteq ℝ$
81		ovolcl	$⊢ ⋃ ran ((.) \circ f) ∖ A \subseteq ℝ \to {vol}^{} (⋃ ran ((.) \circ f) ∖ A) \in ℝ^{}$
82	80 81	ax-mp	$⊢ {vol}^{} (⋃ ran ((.) \circ f) ∖ A) \in ℝ^{}$
83	59 82	jctil	$⊢ {vol}^{} (A) \in ℝ \to ({vol}^{} (⋃ ran ((.) \circ f) ∖ A) \in ℝ^{} \land {vol}^{} (A) + 1 \in ℝ)$
84	83	ad4antlr	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \to ({vol}^{} (⋃ ran ((.) \circ f) ∖ A) \in ℝ^{} \land {vol}^{*} (A) + 1 \in ℝ)$
85		ovolss	$⊢ (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ f) \land ⋃ ran ((.) \circ f) \subseteq ℝ) \to {vol}^{} (⋃ ran ((.) \circ f) ∖ A) \leq {vol}^{} (⋃ ran ((.) \circ f))$
86	79 64 85	mp2an	$⊢ {vol}^{} (⋃ ran ((.) \circ f) ∖ A) \leq {vol}^{} (⋃ ran ((.) \circ f))$
87		xrletr	$⊢ ({vol}^{} (⋃ ran ((.) \circ f) ∖ A) \in ℝ^{} \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ^{} \land {vol}^{} (A) + 1 \in ℝ^{}) \to (({vol}^{} (⋃ ran ((.) \circ f) ∖ A) \leq {vol}^{} (⋃ ran ((.) \circ f)) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1) \to {vol}^{} (⋃ ran ((.) \circ f) ∖ A) \leq {vol}^{} (A) + 1)$
88	82 66 87	mp3an12	$⊢ {vol}^{} (A) + 1 \in ℝ^{} \to (({vol}^{} (⋃ ran ((.) \circ f) ∖ A) \leq {vol}^{} (⋃ ran ((.) \circ f)) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1) \to {vol}^{} (⋃ ran ((.) \circ f) ∖ A) \leq {vol}^{} (A) + 1)$
89	60 88	syl	$⊢ {vol}^{} (A) \in ℝ \to (({vol}^{} (⋃ ran ((.) \circ f) ∖ A) \leq {vol}^{} (⋃ ran ((.) \circ f)) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1) \to {vol}^{} (⋃ ran ((.) \circ f) ∖ A) \leq {vol}^{*} (A) + 1)$
90	86 89	mpani	$⊢ {vol}^{} (A) \in ℝ \to ({vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1 \to {vol}^{} (⋃ ran ((.) \circ f) ∖ A) \leq {vol}^{*} (A) + 1)$
91	90	ad4antlr	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land A \subseteq ⋃ ran ((.) \circ f)) \to ({vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1 \to {vol}^{} (⋃ ran ((.) \circ f) ∖ A) \leq {vol}^{} (A) + 1)$
92	91	impr	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \to {vol}^{} (⋃ ran ((.) \circ f) ∖ A) \leq {vol}^{} (A) + 1$
93		ovolge0	$⊢ ⋃ ran ((.) \circ f) ∖ A \subseteq ℝ \to 0 \leq {vol}^{*} (⋃ ran ((.) \circ f) ∖ A)$
94	80 93	ax-mp	$⊢ 0 \leq {vol}^{*} (⋃ ran ((.) \circ f) ∖ A)$
95	92 94	jctil	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \to (0 \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) \land {vol}^{} (⋃ ran ((.) \circ f) ∖ A) \leq {vol}^{*} (A) + 1)$
96		xrrege0	$⊢ (({vol}^{} (⋃ ran ((.) \circ f) ∖ A) \in ℝ^{} \land {vol}^{} (A) + 1 \in ℝ) \land (0 \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) \land {vol}^{} (⋃ ran ((.) \circ f) ∖ A) \leq {vol}^{} (A) + 1)) \to {vol}^{*} (⋃ ran ((.) \circ f) ∖ A) \in ℝ$
97	84 95 96	syl2anc	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \to {vol}^{*} (⋃ ran ((.) \circ f) ∖ A) \in ℝ$
98		resubcl	$⊢ ({vol}^{} (A) \in ℝ \land u \in ℝ) \to {vol}^{} (A) - u \in ℝ$
99	98	adantrr	$⊢ ({vol}^{} (A) \in ℝ \land (u \in ℝ \land u < {vol}^{} (A))) \to {vol}^{*} (A) - u \in ℝ$
100		posdif	$⊢ (u \in ℝ \land {vol}^{} (A) \in ℝ) \to (u < {vol}^{} (A) \leftrightarrow 0 < {vol}^{*} (A) - u)$
101	100	ancoms	$⊢ ({vol}^{} (A) \in ℝ \land u \in ℝ) \to (u < {vol}^{} (A) \leftrightarrow 0 < {vol}^{*} (A) - u)$
102	101	biimpd	$⊢ ({vol}^{} (A) \in ℝ \land u \in ℝ) \to (u < {vol}^{} (A) \to 0 < {vol}^{*} (A) - u)$
103	102	impr	$⊢ ({vol}^{} (A) \in ℝ \land (u \in ℝ \land u < {vol}^{} (A))) \to 0 < {vol}^{*} (A) - u$
104	99 103	elrpd	$⊢ ({vol}^{} (A) \in ℝ \land (u \in ℝ \land u < {vol}^{} (A))) \to {vol}^{*} (A) - u \in ℝ^{+}$
105	104	rphalfcld	$⊢ ({vol}^{} (A) \in ℝ \land (u \in ℝ \land u < {vol}^{} (A))) \to \frac{{vol}^{*} (A) - u}{2} \in ℝ^{+}$
106	3 105	sylan	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \to \frac{{vol}^{*} (A) - u}{2} \in ℝ^{+}$
107	106	adantr	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \to \frac{{vol}^{*} (A) - u}{2} \in ℝ^{+}$
108		eqid	$⊢ seq 1 (+ ((abs \circ -) \circ g)) = seq 1 (+ ((abs \circ -) \circ g))$
109	108	ovolgelb	$⊢ (⋃ ran ((.) \circ f) ∖ A \subseteq ℝ \land {vol}^{} (⋃ ran ((.) \circ f) ∖ A) \in ℝ \land \frac{{vol}^{} (A) - u}{2} \in ℝ^{+}) \to \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{*} (A) - u}{2}))$
110	80 109	mp3an1	$⊢ ({vol}^{} (⋃ ran ((.) \circ f) ∖ A) \in ℝ \land \frac{{vol}^{} (A) - u}{2} \in ℝ^{+}) \to \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{*} (A) - u}{2}))$
111	97 107 110	syl2anc	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \to \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{*} (A) - u}{2}))$
112		elmapi	$⊢ g \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to g : ℕ ⟶ \leq \cap ℝ^{2}$
113		ssid	$⊢ ⋃ ran ((.) \circ g) \subseteq ⋃ ran ((.) \circ g)$
114	108	ovollb	$⊢ (g : ℕ ⟶ \leq \cap ℝ^{2} \land ⋃ ran ((.) \circ g) \subseteq ⋃ ran ((.) \circ g)) \to {vol}^{} (⋃ ran ((.) \circ g)) \leq sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <)$
115	113 114	mpan2	$⊢ g : ℕ ⟶ \leq \cap ℝ^{2} \to {vol}^{} (⋃ ran ((.) \circ g)) \leq sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <)$
116	115	adantl	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land g : ℕ ⟶ \leq \cap ℝ^{2}) \to {vol}^{} (⋃ ran ((.) \circ g)) \leq sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <)$
117		eqid	$⊢ (abs \circ -) \circ g = (abs \circ -) \circ g$
118	117 108	ovolsf	$⊢ g : ℕ ⟶ \leq \cap ℝ^{2} \to seq 1 (+ ((abs \circ -) \circ g)) : ℕ ⟶ [0, +∞)$
119		frn	$⊢ seq 1 (+ ((abs \circ -) \circ g)) : ℕ ⟶ [0, +∞) \to ran seq 1 (+ ((abs \circ -) \circ g)) \subseteq [0, +∞)$
120	119 55	sstrdi	$⊢ seq 1 (+ ((abs \circ -) \circ g)) : ℕ ⟶ [0, +∞) \to ran seq 1 (+ ((abs \circ -) \circ g)) \subseteq ℝ^{*}$
121		supxrcl	$⊢ ran seq 1 (+ ((abs \circ -) \circ g)) \subseteq ℝ^{} \to sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \in ℝ^{*}$
122	118 120 121	3syl	$⊢ g : ℕ ⟶ \leq \cap ℝ^{2} \to sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \in ℝ^{}$
123	99	rehalfcld	$⊢ ({vol}^{} (A) \in ℝ \land (u \in ℝ \land u < {vol}^{} (A))) \to \frac{{vol}^{*} (A) - u}{2} \in ℝ$
124	3 123	sylan	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \to \frac{{vol}^{*} (A) - u}{2} \in ℝ$
125	124	adantr	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \to \frac{{vol}^{*} (A) - u}{2} \in ℝ$
126	97 125	readdcld	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \to {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}) \in ℝ$
127	126	rexrd	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \to {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}) \in ℝ^{*}$
128		rncoss	$⊢ ran ((.) \circ g) \subseteq ran (.)$
129	128	unissi	$⊢ ⋃ ran ((.) \circ g) \subseteq ⋃ ran (.)$
130	129 63	sseqtrri	$⊢ ⋃ ran ((.) \circ g) \subseteq ℝ$
131		ovolcl	$⊢ ⋃ ran ((.) \circ g) \subseteq ℝ \to {vol}^{} (⋃ ran ((.) \circ g)) \in ℝ^{}$
132	130 131	ax-mp	$⊢ {vol}^{} (⋃ ran ((.) \circ g)) \in ℝ^{}$
133		xrletr	$⊢ ({vol}^{} (⋃ ran ((.) \circ g)) \in ℝ^{} \land sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \in ℝ^{} \land {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}) \in ℝ^{}) \to (({vol}^{} (⋃ ran ((.) \circ g)) \leq sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \land sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2})) \to {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{*} (A) - u}{2}))$
134	132 133	mp3an1	$⊢ (sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \in ℝ^{} \land {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}) \in ℝ^{}) \to (({vol}^{} (⋃ ran ((.) \circ g)) \leq sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \land sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2})) \to {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{*} (A) - u}{2}))$
135	122 127 134	syl2anr	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land g : ℕ ⟶ \leq \cap ℝ^{2}) \to (({vol}^{} (⋃ ran ((.) \circ g)) \leq sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \land sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2})) \to {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))$
136	116 135	mpand	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land g : ℕ ⟶ \leq \cap ℝ^{2}) \to (sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}) \to {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))$
137	112 136	sylan2	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land g \in ({(\leq \cap ℝ^{2})}^{ℕ})) \to (sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}) \to {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))$
138	137	anim2d	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land g \in ({(\leq \cap ℝ^{2})}^{ℕ})) \to ((⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2})) \to (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2})))$
139	138	reximdva	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \to (\exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2})) \to \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2})))$
140	111 139	mpd	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \to \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{*} (A) - u}{2}))$
141		rexex	$⊢ \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2})) \to \exists g (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))$
142	140 141	syl	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \to \exists g (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{*} (A) - u}{2}))$
143	59 66	jctil	$⊢ {vol}^{} (A) \in ℝ \to ({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ^{} \land {vol}^{} (A) + 1 \in ℝ)$
144	143	ad3antlr	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \to ({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ^{} \land {vol}^{*} (A) + 1 \in ℝ)$
145		ovolge0	$⊢ ⋃ ran ((.) \circ f) \subseteq ℝ \to 0 \leq {vol}^{*} (⋃ ran ((.) \circ f))$
146	64 145	ax-mp	$⊢ 0 \leq {vol}^{*} (⋃ ran ((.) \circ f))$
147	146	jctl	$⊢ {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1 \to (0 \leq {vol}^{} (⋃ ran ((.) \circ f)) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{*} (A) + 1)$
148	147	adantl	$⊢ (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1) \to (0 \leq {vol}^{} (⋃ ran ((.) \circ f)) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{*} (A) + 1)$
149		xrrege0	$⊢ (({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ^{} \land {vol}^{} (A) + 1 \in ℝ) \land (0 \leq {vol}^{} (⋃ ran ((.) \circ f)) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \to {vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ$
150	144 148 149	syl2an	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \to {vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ$
151	150 125	resubcld	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \to {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) \in ℝ$
152	150 107	ltsubrpd	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \to {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{*} (⋃ ran ((.) \circ f))$
153		retop	$⊢ topGen (ran (.)) \in Top$
154		retopbas	$⊢ ran (.) \in TopBases$
155		bastg	$⊢ ran (.) \in TopBases \to ran (.) \subseteq topGen (ran (.))$
156	154 155	ax-mp	$⊢ ran (.) \subseteq topGen (ran (.))$
157	61 156	sstri	$⊢ ran ((.) \circ f) \subseteq topGen (ran (.))$
158		uniopn	$⊢ (topGen (ran (.)) \in Top \land ran ((.) \circ f) \subseteq topGen (ran (.))) \to ⋃ ran ((.) \circ f) \in topGen (ran (.))$
159	153 157 158	mp2an	$⊢ ⋃ ran ((.) \circ f) \in topGen (ran (.))$
160		mblfinlem2	$⊢ (⋃ ran ((.) \circ f) \in topGen (ran (.)) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) \in ℝ \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (⋃ ran ((.) \circ f))) \to \exists s \in Clsd (topGen (ran (.))) (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s))$
161	159 160	mp3an1	$⊢ ({vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) \in ℝ \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (⋃ ran ((.) \circ f))) \to \exists s \in Clsd (topGen (ran (.))) (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s))$
162	151 152 161	syl2anc	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \to \exists s \in Clsd (topGen (ran (.))) (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{*} (s))$
163	162	adantr	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \to \exists s \in Clsd (topGen (ran (.))) (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s))$
164		indif2	$⊢ s \cap (ℝ ∖ ⋃ ran ((.) \circ g)) = (s \cap ℝ) ∖ ⋃ ran ((.) \circ g)$
165	22	cldss	$⊢ s \in Clsd (topGen (ran (.))) \to s \subseteq ℝ$
166		dfss2	$⊢ s \subseteq ℝ \leftrightarrow s \cap ℝ = s$
167	165 166	sylib	$⊢ s \in Clsd (topGen (ran (.))) \to s \cap ℝ = s$
168	167	difeq1d	$⊢ s \in Clsd (topGen (ran (.))) \to (s \cap ℝ) ∖ ⋃ ran ((.) \circ g) = s ∖ ⋃ ran ((.) \circ g)$
169	164 168	eqtrid	$⊢ s \in Clsd (topGen (ran (.))) \to s \cap (ℝ ∖ ⋃ ran ((.) \circ g)) = s ∖ ⋃ ran ((.) \circ g)$
170	128 156	sstri	$⊢ ran ((.) \circ g) \subseteq topGen (ran (.))$
171		uniopn	$⊢ (topGen (ran (.)) \in Top \land ran ((.) \circ g) \subseteq topGen (ran (.))) \to ⋃ ran ((.) \circ g) \in topGen (ran (.))$
172	153 170 171	mp2an	$⊢ ⋃ ran ((.) \circ g) \in topGen (ran (.))$
173	22	opncld	$⊢ (topGen (ran (.)) \in Top \land ⋃ ran ((.) \circ g) \in topGen (ran (.))) \to ℝ ∖ ⋃ ran ((.) \circ g) \in Clsd (topGen (ran (.)))$
174	153 172 173	mp2an	$⊢ ℝ ∖ ⋃ ran ((.) \circ g) \in Clsd (topGen (ran (.)))$
175		incld	$⊢ (s \in Clsd (topGen (ran (.))) \land ℝ ∖ ⋃ ran ((.) \circ g) \in Clsd (topGen (ran (.)))) \to s \cap (ℝ ∖ ⋃ ran ((.) \circ g)) \in Clsd (topGen (ran (.)))$
176	174 175	mpan2	$⊢ s \in Clsd (topGen (ran (.))) \to s \cap (ℝ ∖ ⋃ ran ((.) \circ g)) \in Clsd (topGen (ran (.)))$
177	169 176	eqeltrrd	$⊢ s \in Clsd (topGen (ran (.))) \to s ∖ ⋃ ran ((.) \circ g) \in Clsd (topGen (ran (.)))$
178		simpr	$⊢ (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land s \subseteq ⋃ ran ((.) \circ f)) \to s \subseteq ⋃ ran ((.) \circ f)$
179		simpl	$⊢ (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land s \subseteq ⋃ ran ((.) \circ f)) \to ⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g)$
180	178 179	ssdif2d	$⊢ (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land s \subseteq ⋃ ran ((.) \circ f)) \to s ∖ ⋃ ran ((.) \circ g) \subseteq ⋃ ran ((.) \circ f) ∖ (⋃ ran ((.) \circ f) ∖ A)$
181		dfin4	$⊢ ⋃ ran ((.) \circ f) \cap A = ⋃ ran ((.) \circ f) ∖ (⋃ ran ((.) \circ f) ∖ A)$
182		inss2	$⊢ ⋃ ran ((.) \circ f) \cap A \subseteq A$
183	181 182	eqsstrri	$⊢ ⋃ ran ((.) \circ f) ∖ (⋃ ran ((.) \circ f) ∖ A) \subseteq A$
184	180 183	sstrdi	$⊢ (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land s \subseteq ⋃ ran ((.) \circ f)) \to s ∖ ⋃ ran ((.) \circ g) \subseteq A$
185		sseq1	$⊢ b = s ∖ ⋃ ran ((.) \circ g) \to (b \subseteq A \leftrightarrow s ∖ ⋃ ran ((.) \circ g) \subseteq A)$
186	185	anbi1d	$⊢ b = s ∖ ⋃ ran ((.) \circ g) \to ((b \subseteq A \land vol (s ∖ ⋃ ran ((.) \circ g)) = vol (b)) \leftrightarrow (s ∖ ⋃ ran ((.) \circ g) \subseteq A \land vol (s ∖ ⋃ ran ((.) \circ g)) = vol (b)))$
187		fveq2	$⊢ s ∖ ⋃ ran ((.) \circ g) = b \to vol (s ∖ ⋃ ran ((.) \circ g)) = vol (b)$
188	187	eqcoms	$⊢ b = s ∖ ⋃ ran ((.) \circ g) \to vol (s ∖ ⋃ ran ((.) \circ g)) = vol (b)$
189	188	biantrud	$⊢ b = s ∖ ⋃ ran ((.) \circ g) \to (s ∖ ⋃ ran ((.) \circ g) \subseteq A \leftrightarrow (s ∖ ⋃ ran ((.) \circ g) \subseteq A \land vol (s ∖ ⋃ ran ((.) \circ g)) = vol (b)))$
190	186 189	bitr4d	$⊢ b = s ∖ ⋃ ran ((.) \circ g) \to ((b \subseteq A \land vol (s ∖ ⋃ ran ((.) \circ g)) = vol (b)) \leftrightarrow s ∖ ⋃ ran ((.) \circ g) \subseteq A)$
191	190	rspcev	$⊢ (s ∖ ⋃ ran ((.) \circ g) \in Clsd (topGen (ran (.))) \land s ∖ ⋃ ran ((.) \circ g) \subseteq A) \to \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land vol (s ∖ ⋃ ran ((.) \circ g)) = vol (b))$
192	177 184 191	syl2an	$⊢ (s \in Clsd (topGen (ran (.))) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land s \subseteq ⋃ ran ((.) \circ f))) \to \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land vol (s ∖ ⋃ ran ((.) \circ g)) = vol (b))$
193	192	an12s	$⊢ (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land (s \in Clsd (topGen (ran (.))) \land s \subseteq ⋃ ran ((.) \circ f))) \to \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land vol (s ∖ ⋃ ran ((.) \circ g)) = vol (b))$
194	193	adantrrr	$⊢ (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{*} (s)))) \to \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land vol (s ∖ ⋃ ran ((.) \circ g)) = vol (b))$
195	194	adantlr	$⊢ ((⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2})) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land vol (s ∖ ⋃ ran ((.) \circ g)) = vol (b))$
196	195	adantll	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land vol (s ∖ ⋃ ran ((.) \circ g)) = vol (b))$
197		difss	$⊢ A ∖ (s ∖ ⋃ ran ((.) \circ g)) \subseteq A$
198		ovolsscl	$⊢ (A ∖ (s ∖ ⋃ ran ((.) \circ g)) \subseteq A \land A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} (A ∖ (s ∖ ⋃ ran ((.) \circ g))) \in ℝ$
199	197 198	mp3an1	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} (A ∖ (s ∖ ⋃ ran ((.) \circ g))) \in ℝ$
200	199	ad5antr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{*} (A ∖ (s ∖ ⋃ ran ((.) \circ g))) \in ℝ$
201		simp-6r	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{*} (A) \in ℝ$
202		simpl	$⊢ (u \in ℝ \land u < {vol}^{*} (A)) \to u \in ℝ$
203	202	ad4antlr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to u \in ℝ$
204		difdif2	$⊢ A ∖ (s ∖ ⋃ ran ((.) \circ g)) = (A ∖ s) \cup (A \cap ⋃ ran ((.) \circ g))$
205	204	fveq2i	$⊢ {vol}^{} (A ∖ (s ∖ ⋃ ran ((.) \circ g))) = {vol}^{} ((A ∖ s) \cup (A \cap ⋃ ran ((.) \circ g)))$
206		difss	$⊢ A ∖ s \subseteq A$
207		inss1	$⊢ A \cap ⋃ ran ((.) \circ g) \subseteq A$
208	206 207	unssi	$⊢ (A ∖ s) \cup (A \cap ⋃ ran ((.) \circ g)) \subseteq A$
209		ovolsscl	$⊢ ((A ∖ s) \cup (A \cap ⋃ ran ((.) \circ g)) \subseteq A \land A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} ((A ∖ s) \cup (A \cap ⋃ ran ((.) \circ g))) \in ℝ$
210	208 209	mp3an1	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} ((A ∖ s) \cup (A \cap ⋃ ran ((.) \circ g))) \in ℝ$
211	210	ad5antr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{*} ((A ∖ s) \cup (A \cap ⋃ ran ((.) \circ g))) \in ℝ$
212		ovolsscl	$⊢ (A ∖ s \subseteq A \land A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} (A ∖ s) \in ℝ$
213	206 212	mp3an1	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} (A ∖ s) \in ℝ$
214	213	ad5antr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{*} (A ∖ s) \in ℝ$
215		ovolsscl	$⊢ (A \cap ⋃ ran ((.) \circ g) \subseteq A \land A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} (A \cap ⋃ ran ((.) \circ g)) \in ℝ$
216	207 215	mp3an1	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} (A \cap ⋃ ran ((.) \circ g)) \in ℝ$
217	216	ad5antr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{*} (A \cap ⋃ ran ((.) \circ g)) \in ℝ$
218	214 217	readdcld	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{} (A ∖ s) + {vol}^{} (A \cap ⋃ ran ((.) \circ g)) \in ℝ$
219	3 202 98	syl2an	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \to {vol}^{*} (A) - u \in ℝ$
220	219	ad3antrrr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{*} (A) - u \in ℝ$
221		ssdifss	$⊢ A \subseteq ℝ \to A ∖ s \subseteq ℝ$
222	221	adantr	$⊢ (A \subseteq ℝ \land {vol}^{*} (A) \in ℝ) \to A ∖ s \subseteq ℝ$
223		ssinss1	$⊢ A \subseteq ℝ \to A \cap ⋃ ran ((.) \circ g) \subseteq ℝ$
224	223	adantr	$⊢ (A \subseteq ℝ \land {vol}^{*} (A) \in ℝ) \to A \cap ⋃ ran ((.) \circ g) \subseteq ℝ$
225		ovolun	$⊢ ((A ∖ s \subseteq ℝ \land {vol}^{} (A ∖ s) \in ℝ) \land (A \cap ⋃ ran ((.) \circ g) \subseteq ℝ \land {vol}^{} (A \cap ⋃ ran ((.) \circ g)) \in ℝ)) \to {vol}^{} ((A ∖ s) \cup (A \cap ⋃ ran ((.) \circ g))) \leq {vol}^{} (A ∖ s) + {vol}^{*} (A \cap ⋃ ran ((.) \circ g))$
226	222 213 224 216 225	syl22anc	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} ((A ∖ s) \cup (A \cap ⋃ ran ((.) \circ g))) \leq {vol}^{} (A ∖ s) + {vol}^{} (A \cap ⋃ ran ((.) \circ g))$
227	226	ad5antr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{} ((A ∖ s) \cup (A \cap ⋃ ran ((.) \circ g))) \leq {vol}^{} (A ∖ s) + {vol}^{*} (A \cap ⋃ ran ((.) \circ g))$
228	124	ad2antrr	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \to \frac{{vol}^{} (A) - u}{2} \in ℝ$
229	228	adantr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to \frac{{vol}^{*} (A) - u}{2} \in ℝ$
230	150	ad2antrr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ$
231		simprl	$⊢ (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{*} (s))) \to s \subseteq ⋃ ran ((.) \circ f)$
232	150	adantr	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \to {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ$
233		ovolsscl	$⊢ (s \subseteq ⋃ ran ((.) \circ f) \land ⋃ ran ((.) \circ f) \subseteq ℝ \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{} (s) \in ℝ$
234	64 233	mp3an2	$⊢ (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{} (s) \in ℝ$
235	231 232 234	syl2anr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{*} (s) \in ℝ$
236	230 235	resubcld	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{} (⋃ ran ((.) \circ f)) - {vol}^{} (s) \in ℝ$
237		ssdif	$⊢ A \subseteq ⋃ ran ((.) \circ f) \to A ∖ s \subseteq ⋃ ran ((.) \circ f) ∖ s$
238		difss	$⊢ ⋃ ran ((.) \circ f) ∖ s \subseteq ⋃ ran ((.) \circ f)$
239	238 64	sstri	$⊢ ⋃ ran ((.) \circ f) ∖ s \subseteq ℝ$
240		ovolss	$⊢ (A ∖ s \subseteq ⋃ ran ((.) \circ f) ∖ s \land ⋃ ran ((.) \circ f) ∖ s \subseteq ℝ) \to {vol}^{} (A ∖ s) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ s)$
241	237 239 240	sylancl	$⊢ A \subseteq ⋃ ran ((.) \circ f) \to {vol}^{} (A ∖ s) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ s)$
242	241	adantr	$⊢ (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1) \to {vol}^{} (A ∖ s) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ s)$
243	242	ad3antlr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{} (A ∖ s) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ s)$
244		eleq1w	$⊢ b = s \to (b \in dom vol \leftrightarrow s \in dom vol)$
245	244 32	vtoclga	$⊢ s \in Clsd (topGen (ran (.))) \to s \in dom vol$
246	245	adantr	$⊢ (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{*} (s))) \to s \in dom vol$
247		mblsplit	$⊢ (s \in dom vol \land ⋃ ran ((.) \circ f) \subseteq ℝ \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{} (⋃ ran ((.) \circ f)) = {vol}^{} (⋃ ran ((.) \circ f) \cap s) + {vol}^{} (⋃ ran ((.) \circ f) ∖ s)$
248	64 247	mp3an2	$⊢ (s \in dom vol \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{} (⋃ ran ((.) \circ f)) = {vol}^{} (⋃ ran ((.) \circ f) \cap s) + {vol}^{} (⋃ ran ((.) \circ f) ∖ s)$
249	246 232 248	syl2anr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{} (⋃ ran ((.) \circ f)) = {vol}^{} (⋃ ran ((.) \circ f) \cap s) + {vol}^{*} (⋃ ran ((.) \circ f) ∖ s)$
250	249	eqcomd	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{} (⋃ ran ((.) \circ f) \cap s) + {vol}^{} (⋃ ran ((.) \circ f) ∖ s) = {vol}^{*} (⋃ ran ((.) \circ f))$
251	230	recnd	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{*} (⋃ ran ((.) \circ f)) \in ℂ$
252		inss1	$⊢ ⋃ ran ((.) \circ f) \cap s \subseteq ⋃ ran ((.) \circ f)$
253		ovolsscl	$⊢ (⋃ ran ((.) \circ f) \cap s \subseteq ⋃ ran ((.) \circ f) \land ⋃ ran ((.) \circ f) \subseteq ℝ \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{} (⋃ ran ((.) \circ f) \cap s) \in ℝ$
254	252 64 253	mp3an12	$⊢ {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \to {vol}^{} (⋃ ran ((.) \circ f) \cap s) \in ℝ$
255	150 254	syl	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \to {vol}^{*} (⋃ ran ((.) \circ f) \cap s) \in ℝ$
256	255	ad2antrr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{*} (⋃ ran ((.) \circ f) \cap s) \in ℝ$
257	256	recnd	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{*} (⋃ ran ((.) \circ f) \cap s) \in ℂ$
258		ovolsscl	$⊢ (⋃ ran ((.) \circ f) ∖ s \subseteq ⋃ ran ((.) \circ f) \land ⋃ ran ((.) \circ f) \subseteq ℝ \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{} (⋃ ran ((.) \circ f) ∖ s) \in ℝ$
259	238 64 258	mp3an12	$⊢ {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \to {vol}^{} (⋃ ran ((.) \circ f) ∖ s) \in ℝ$
260	150 259	syl	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \to {vol}^{*} (⋃ ran ((.) \circ f) ∖ s) \in ℝ$
261	260	recnd	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \to {vol}^{*} (⋃ ran ((.) \circ f) ∖ s) \in ℂ$
262	261	ad2antrr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{*} (⋃ ran ((.) \circ f) ∖ s) \in ℂ$
263	251 257 262	subaddd	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to ({vol}^{} (⋃ ran ((.) \circ f)) - {vol}^{} (⋃ ran ((.) \circ f) \cap s) = {vol}^{} (⋃ ran ((.) \circ f) ∖ s) \leftrightarrow {vol}^{} (⋃ ran ((.) \circ f) \cap s) + {vol}^{} (⋃ ran ((.) \circ f) ∖ s) = {vol}^{} (⋃ ran ((.) \circ f)))$
264	250 263	mpbird	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{} (⋃ ran ((.) \circ f)) - {vol}^{} (⋃ ran ((.) \circ f) \cap s) = {vol}^{*} (⋃ ran ((.) \circ f) ∖ s)$
265		sseqin2	$⊢ s \subseteq ⋃ ran ((.) \circ f) \leftrightarrow ⋃ ran ((.) \circ f) \cap s = s$
266	265	biimpi	$⊢ s \subseteq ⋃ ran ((.) \circ f) \to ⋃ ran ((.) \circ f) \cap s = s$
267	266	fveq2d	$⊢ s \subseteq ⋃ ran ((.) \circ f) \to {vol}^{} (⋃ ran ((.) \circ f) \cap s) = {vol}^{} (s)$
268	267	oveq2d	$⊢ s \subseteq ⋃ ran ((.) \circ f) \to {vol}^{} (⋃ ran ((.) \circ f)) - {vol}^{} (⋃ ran ((.) \circ f) \cap s) = {vol}^{} (⋃ ran ((.) \circ f)) - {vol}^{} (s)$
269	268	adantr	$⊢ (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)) \to {vol}^{} (⋃ ran ((.) \circ f)) - {vol}^{} (⋃ ran ((.) \circ f) \cap s) = {vol}^{} (⋃ ran ((.) \circ f)) - {vol}^{*} (s)$
270	269	ad2antll	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{} (⋃ ran ((.) \circ f)) - {vol}^{} (⋃ ran ((.) \circ f) \cap s) = {vol}^{} (⋃ ran ((.) \circ f)) - {vol}^{} (s)$
271	264 270	eqtr3d	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{} (⋃ ran ((.) \circ f) ∖ s) = {vol}^{} (⋃ ran ((.) \circ f)) - {vol}^{*} (s)$
272	243 271	breqtrd	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{} (A ∖ s) \leq {vol}^{} (⋃ ran ((.) \circ f)) - {vol}^{*} (s)$
273		simprrr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{*} (s)$
274	230 229 235 273	ltsub23d	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{} (⋃ ran ((.) \circ f)) - {vol}^{} (s) < \frac{{vol}^{*} (A) - u}{2}$
275	214 236 229 272 274	lelttrd	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{} (A ∖ s) < \frac{{vol}^{} (A) - u}{2}$
276	216	ad4antr	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \to {vol}^{} (A \cap ⋃ ran ((.) \circ g)) \in ℝ$
277	126 132	jctil	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \to ({vol}^{} (⋃ ran ((.) \circ g)) \in ℝ^{} \land {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}) \in ℝ)$
278		simpr	$⊢ (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2})) \to {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2})$
279		ovolge0	$⊢ ⋃ ran ((.) \circ g) \subseteq ℝ \to 0 \leq {vol}^{*} (⋃ ran ((.) \circ g))$
280	130 279	ax-mp	$⊢ 0 \leq {vol}^{*} (⋃ ran ((.) \circ g))$
281	278 280	jctil	$⊢ (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2})) \to (0 \leq {vol}^{} (⋃ ran ((.) \circ g)) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{*} (A) - u}{2}))$
282		xrrege0	$⊢ (({vol}^{} (⋃ ran ((.) \circ g)) \in ℝ^{} \land {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}) \in ℝ) \land (0 \leq {vol}^{} (⋃ ran ((.) \circ g)) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \to {vol}^{*} (⋃ ran ((.) \circ g)) \in ℝ$
283	277 281 282	syl2an	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \to {vol}^{} (⋃ ran ((.) \circ g)) \in ℝ$
284		difss	$⊢ ⋃ ran ((.) \circ g) ∖ (⋃ ran ((.) \circ f) ∖ A) \subseteq ⋃ ran ((.) \circ g)$
285		ovolsscl	$⊢ (⋃ ran ((.) \circ g) ∖ (⋃ ran ((.) \circ f) ∖ A) \subseteq ⋃ ran ((.) \circ g) \land ⋃ ran ((.) \circ g) \subseteq ℝ \land {vol}^{} (⋃ ran ((.) \circ g)) \in ℝ) \to {vol}^{} (⋃ ran ((.) \circ g) ∖ (⋃ ran ((.) \circ f) ∖ A)) \in ℝ$
286	284 130 285	mp3an12	$⊢ {vol}^{} (⋃ ran ((.) \circ g)) \in ℝ \to {vol}^{} (⋃ ran ((.) \circ g) ∖ (⋃ ran ((.) \circ f) ∖ A)) \in ℝ$
287	283 286	syl	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \to {vol}^{} (⋃ ran ((.) \circ g) ∖ (⋃ ran ((.) \circ f) ∖ A)) \in ℝ$
288		ssun2	$⊢ ⋃ ran ((.) \circ g) \cap A \subseteq (⋃ ran ((.) \circ g) ∖ ⋃ ran ((.) \circ f)) \cup (⋃ ran ((.) \circ g) \cap A)$
289		incom	$⊢ A \cap ⋃ ran ((.) \circ g) = ⋃ ran ((.) \circ g) \cap A$
290		difdif2	$⊢ ⋃ ran ((.) \circ g) ∖ (⋃ ran ((.) \circ f) ∖ A) = (⋃ ran ((.) \circ g) ∖ ⋃ ran ((.) \circ f)) \cup (⋃ ran ((.) \circ g) \cap A)$
291	288 289 290	3sstr4i	$⊢ A \cap ⋃ ran ((.) \circ g) \subseteq ⋃ ran ((.) \circ g) ∖ (⋃ ran ((.) \circ f) ∖ A)$
292	284 130	sstri	$⊢ ⋃ ran ((.) \circ g) ∖ (⋃ ran ((.) \circ f) ∖ A) \subseteq ℝ$
293	291 292	pm3.2i	$⊢ (A \cap ⋃ ran ((.) \circ g) \subseteq ⋃ ran ((.) \circ g) ∖ (⋃ ran ((.) \circ f) ∖ A) \land ⋃ ran ((.) \circ g) ∖ (⋃ ran ((.) \circ f) ∖ A) \subseteq ℝ)$
294		ovolss	$⊢ (A \cap ⋃ ran ((.) \circ g) \subseteq ⋃ ran ((.) \circ g) ∖ (⋃ ran ((.) \circ f) ∖ A) \land ⋃ ran ((.) \circ g) ∖ (⋃ ran ((.) \circ f) ∖ A) \subseteq ℝ) \to {vol}^{} (A \cap ⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ g) ∖ (⋃ ran ((.) \circ f) ∖ A))$
295	293 294	mp1i	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \to {vol}^{} (A \cap ⋃ ran ((.) \circ g)) \leq {vol}^{*} (⋃ ran ((.) \circ g) ∖ (⋃ ran ((.) \circ f) ∖ A))$
296		opnmbl	$⊢ ⋃ ran ((.) \circ f) \in topGen (ran (.)) \to ⋃ ran ((.) \circ f) \in dom vol$
297	159 296	ax-mp	$⊢ ⋃ ran ((.) \circ f) \in dom vol$
298		difmbl	$⊢ (⋃ ran ((.) \circ f) \in dom vol \land A \in dom vol) \to ⋃ ran ((.) \circ f) ∖ A \in dom vol$
299	297 298	mpan	$⊢ A \in dom vol \to ⋃ ran ((.) \circ f) ∖ A \in dom vol$
300	299	ad4antlr	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{*} (A) - u}{2}))) \to ⋃ ran ((.) \circ f) ∖ A \in dom vol$
301		mblsplit	$⊢ (⋃ ran ((.) \circ f) ∖ A \in dom vol \land ⋃ ran ((.) \circ g) \subseteq ℝ \land {vol}^{} (⋃ ran ((.) \circ g)) \in ℝ) \to {vol}^{} (⋃ ran ((.) \circ g)) = {vol}^{} (⋃ ran ((.) \circ g) \cap (⋃ ran ((.) \circ f) ∖ A)) + {vol}^{} (⋃ ran ((.) \circ g) ∖ (⋃ ran ((.) \circ f) ∖ A))$
302	130 301	mp3an2	$⊢ (⋃ ran ((.) \circ f) ∖ A \in dom vol \land {vol}^{} (⋃ ran ((.) \circ g)) \in ℝ) \to {vol}^{} (⋃ ran ((.) \circ g)) = {vol}^{} (⋃ ran ((.) \circ g) \cap (⋃ ran ((.) \circ f) ∖ A)) + {vol}^{} (⋃ ran ((.) \circ g) ∖ (⋃ ran ((.) \circ f) ∖ A))$
303	300 283 302	syl2anc	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \to {vol}^{} (⋃ ran ((.) \circ g)) = {vol}^{} (⋃ ran ((.) \circ g) \cap (⋃ ran ((.) \circ f) ∖ A)) + {vol}^{} (⋃ ran ((.) \circ g) ∖ (⋃ ran ((.) \circ f) ∖ A))$
304		sseqin2	$⊢ ⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \leftrightarrow ⋃ ran ((.) \circ g) \cap (⋃ ran ((.) \circ f) ∖ A) = ⋃ ran ((.) \circ f) ∖ A$
305	304	biimpi	$⊢ ⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \to ⋃ ran ((.) \circ g) \cap (⋃ ran ((.) \circ f) ∖ A) = ⋃ ran ((.) \circ f) ∖ A$
306	305	fveq2d	$⊢ ⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \to {vol}^{} (⋃ ran ((.) \circ g) \cap (⋃ ran ((.) \circ f) ∖ A)) = {vol}^{} (⋃ ran ((.) \circ f) ∖ A)$
307	306	oveq1d	$⊢ ⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \to {vol}^{} (⋃ ran ((.) \circ g) \cap (⋃ ran ((.) \circ f) ∖ A)) + {vol}^{} (⋃ ran ((.) \circ g) ∖ (⋃ ran ((.) \circ f) ∖ A)) = {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + {vol}^{} (⋃ ran ((.) \circ g) ∖ (⋃ ran ((.) \circ f) ∖ A))$
308	307	ad2antrl	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \to {vol}^{} (⋃ ran ((.) \circ g) \cap (⋃ ran ((.) \circ f) ∖ A)) + {vol}^{} (⋃ ran ((.) \circ g) ∖ (⋃ ran ((.) \circ f) ∖ A)) = {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + {vol}^{*} (⋃ ran ((.) \circ g) ∖ (⋃ ran ((.) \circ f) ∖ A))$
309	303 308	eqtr2d	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \to {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + {vol}^{} (⋃ ran ((.) \circ g) ∖ (⋃ ran ((.) \circ f) ∖ A)) = {vol}^{} (⋃ ran ((.) \circ g))$
310	283	recnd	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \to {vol}^{} (⋃ ran ((.) \circ g)) \in ℂ$
311	97	adantr	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \to {vol}^{} (⋃ ran ((.) \circ f) ∖ A) \in ℝ$
312	311	recnd	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \to {vol}^{} (⋃ ran ((.) \circ f) ∖ A) \in ℂ$
313	287	recnd	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \to {vol}^{} (⋃ ran ((.) \circ g) ∖ (⋃ ran ((.) \circ f) ∖ A)) \in ℂ$
314	310 312 313	subaddd	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \to ({vol}^{} (⋃ ran ((.) \circ g)) - {vol}^{} (⋃ ran ((.) \circ f) ∖ A) = {vol}^{} (⋃ ran ((.) \circ g) ∖ (⋃ ran ((.) \circ f) ∖ A)) \leftrightarrow {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + {vol}^{} (⋃ ran ((.) \circ g) ∖ (⋃ ran ((.) \circ f) ∖ A)) = {vol}^{*} (⋃ ran ((.) \circ g)))$
315	309 314	mpbird	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \to {vol}^{} (⋃ ran ((.) \circ g)) - {vol}^{} (⋃ ran ((.) \circ f) ∖ A) = {vol}^{} (⋃ ran ((.) \circ g) ∖ (⋃ ran ((.) \circ f) ∖ A))$
316		simprr	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \to {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2})$
317	283 311 228	lesubadd2d	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \to ({vol}^{} (⋃ ran ((.) \circ g)) - {vol}^{} (⋃ ran ((.) \circ f) ∖ A) \leq \frac{{vol}^{} (A) - u}{2} \leftrightarrow {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{*} (A) - u}{2}))$
318	316 317	mpbird	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \to {vol}^{} (⋃ ran ((.) \circ g)) - {vol}^{} (⋃ ran ((.) \circ f) ∖ A) \leq \frac{{vol}^{} (A) - u}{2}$
319	315 318	eqbrtrrd	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \to {vol}^{} (⋃ ran ((.) \circ g) ∖ (⋃ ran ((.) \circ f) ∖ A)) \leq \frac{{vol}^{*} (A) - u}{2}$
320	276 287 228 295 319	letrd	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \to {vol}^{} (A \cap ⋃ ran ((.) \circ g)) \leq \frac{{vol}^{*} (A) - u}{2}$
321	320	adantr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{} (A \cap ⋃ ran ((.) \circ g)) \leq \frac{{vol}^{} (A) - u}{2}$
322	214 217 229 229 275 321	ltleaddd	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{} (A ∖ s) + {vol}^{} (A \cap ⋃ ran ((.) \circ g)) < (\frac{{vol}^{} (A) - u}{2}) + (\frac{{vol}^{} (A) - u}{2})$
323	98	recnd	$⊢ ({vol}^{} (A) \in ℝ \land u \in ℝ) \to {vol}^{} (A) - u \in ℂ$
324	323	2halvesd	$⊢ ({vol}^{} (A) \in ℝ \land u \in ℝ) \to (\frac{{vol}^{} (A) - u}{2}) + (\frac{{vol}^{} (A) - u}{2}) = {vol}^{} (A) - u$
325	324	adantll	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land u \in ℝ) \to (\frac{{vol}^{} (A) - u}{2}) + (\frac{{vol}^{} (A) - u}{2}) = {vol}^{} (A) - u$
326	325	ad2ant2r	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \to (\frac{{vol}^{} (A) - u}{2}) + (\frac{{vol}^{} (A) - u}{2}) = {vol}^{*} (A) - u$
327	326	ad3antrrr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to (\frac{{vol}^{} (A) - u}{2}) + (\frac{{vol}^{} (A) - u}{2}) = {vol}^{*} (A) - u$
328	322 327	breqtrd	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{} (A ∖ s) + {vol}^{} (A \cap ⋃ ran ((.) \circ g)) < {vol}^{*} (A) - u$
329	211 218 220 227 328	lelttrd	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{} ((A ∖ s) \cup (A \cap ⋃ ran ((.) \circ g))) < {vol}^{} (A) - u$
330	205 329	eqbrtrid	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{} (A ∖ (s ∖ ⋃ ran ((.) \circ g))) < {vol}^{} (A) - u$
331	200 201 203 330	ltsub13d	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to u < {vol}^{} (A) - {vol}^{} (A ∖ (s ∖ ⋃ ran ((.) \circ g)))$
332		opnmbl	$⊢ ⋃ ran ((.) \circ g) \in topGen (ran (.)) \to ⋃ ran ((.) \circ g) \in dom vol$
333	172 332	ax-mp	$⊢ ⋃ ran ((.) \circ g) \in dom vol$
334		difmbl	$⊢ (s \in dom vol \land ⋃ ran ((.) \circ g) \in dom vol) \to s ∖ ⋃ ran ((.) \circ g) \in dom vol$
335	245 333 334	sylancl	$⊢ s \in Clsd (topGen (ran (.))) \to s ∖ ⋃ ran ((.) \circ g) \in dom vol$
336		mblvol	$⊢ s ∖ ⋃ ran ((.) \circ g) \in dom vol \to vol (s ∖ ⋃ ran ((.) \circ g)) = {vol}^{*} (s ∖ ⋃ ran ((.) \circ g))$
337	335 336	syl	$⊢ s \in Clsd (topGen (ran (.))) \to vol (s ∖ ⋃ ran ((.) \circ g)) = {vol}^{*} (s ∖ ⋃ ran ((.) \circ g))$
338	337	ad2antrl	$⊢ ((⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2})) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to vol (s ∖ ⋃ ran ((.) \circ g)) = {vol}^{*} (s ∖ ⋃ ran ((.) \circ g))$
339		sseqin2	$⊢ s ∖ ⋃ ran ((.) \circ g) \subseteq A \leftrightarrow A \cap (s ∖ ⋃ ran ((.) \circ g)) = s ∖ ⋃ ran ((.) \circ g)$
340	184 339	sylib	$⊢ (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land s \subseteq ⋃ ran ((.) \circ f)) \to A \cap (s ∖ ⋃ ran ((.) \circ g)) = s ∖ ⋃ ran ((.) \circ g)$
341	340	fveq2d	$⊢ (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land s \subseteq ⋃ ran ((.) \circ f)) \to {vol}^{} (A \cap (s ∖ ⋃ ran ((.) \circ g))) = {vol}^{} (s ∖ ⋃ ran ((.) \circ g))$
342	341	adantrr	$⊢ (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s))) \to {vol}^{} (A \cap (s ∖ ⋃ ran ((.) \circ g))) = {vol}^{*} (s ∖ ⋃ ran ((.) \circ g))$
343	342	ad2ant2rl	$⊢ ((⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2})) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{} (A \cap (s ∖ ⋃ ran ((.) \circ g))) = {vol}^{} (s ∖ ⋃ ran ((.) \circ g))$
344	338 343	eqtr4d	$⊢ ((⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2})) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to vol (s ∖ ⋃ ran ((.) \circ g)) = {vol}^{*} (A \cap (s ∖ ⋃ ran ((.) \circ g)))$
345	344	adantll	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to vol (s ∖ ⋃ ran ((.) \circ g)) = {vol}^{*} (A \cap (s ∖ ⋃ ran ((.) \circ g)))$
346	335	adantr	$⊢ (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{*} (s))) \to s ∖ ⋃ ran ((.) \circ g) \in dom vol$
347		simp-4l	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \to (A \subseteq ℝ \land {vol}^{} (A) \in ℝ)$
348		mblsplit	$⊢ (s ∖ ⋃ ran ((.) \circ g) \in dom vol \land A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} (A) = {vol}^{} (A \cap (s ∖ ⋃ ran ((.) \circ g))) + {vol}^{} (A ∖ (s ∖ ⋃ ran ((.) \circ g)))$
349	348	3expb	$⊢ (s ∖ ⋃ ran ((.) \circ g) \in dom vol \land (A \subseteq ℝ \land {vol}^{} (A) \in ℝ)) \to {vol}^{} (A) = {vol}^{} (A \cap (s ∖ ⋃ ran ((.) \circ g))) + {vol}^{} (A ∖ (s ∖ ⋃ ran ((.) \circ g)))$
350	349	eqcomd	$⊢ (s ∖ ⋃ ran ((.) \circ g) \in dom vol \land (A \subseteq ℝ \land {vol}^{} (A) \in ℝ)) \to {vol}^{} (A \cap (s ∖ ⋃ ran ((.) \circ g))) + {vol}^{} (A ∖ (s ∖ ⋃ ran ((.) \circ g))) = {vol}^{} (A)$
351	346 347 350	syl2anr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{} (A \cap (s ∖ ⋃ ran ((.) \circ g))) + {vol}^{} (A ∖ (s ∖ ⋃ ran ((.) \circ g))) = {vol}^{*} (A)$
352		recn	$⊢ {vol}^{} (A) \in ℝ \to {vol}^{} (A) \in ℂ$
353	352	adantl	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} (A) \in ℂ$
354	199	recnd	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} (A ∖ (s ∖ ⋃ ran ((.) \circ g))) \in ℂ$
355		inss1	$⊢ A \cap (s ∖ ⋃ ran ((.) \circ g)) \subseteq A$
356		ovolsscl	$⊢ (A \cap (s ∖ ⋃ ran ((.) \circ g)) \subseteq A \land A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} (A \cap (s ∖ ⋃ ran ((.) \circ g))) \in ℝ$
357	355 356	mp3an1	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} (A \cap (s ∖ ⋃ ran ((.) \circ g))) \in ℝ$
358	357	recnd	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to {vol}^{} (A \cap (s ∖ ⋃ ran ((.) \circ g))) \in ℂ$
359	353 354 358	subadd2d	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to ({vol}^{} (A) - {vol}^{} (A ∖ (s ∖ ⋃ ran ((.) \circ g))) = {vol}^{} (A \cap (s ∖ ⋃ ran ((.) \circ g))) \leftrightarrow {vol}^{} (A \cap (s ∖ ⋃ ran ((.) \circ g))) + {vol}^{} (A ∖ (s ∖ ⋃ ran ((.) \circ g))) = {vol}^{*} (A))$
360	359	ad5antr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to ({vol}^{} (A) - {vol}^{} (A ∖ (s ∖ ⋃ ran ((.) \circ g))) = {vol}^{} (A \cap (s ∖ ⋃ ran ((.) \circ g))) \leftrightarrow {vol}^{} (A \cap (s ∖ ⋃ ran ((.) \circ g))) + {vol}^{} (A ∖ (s ∖ ⋃ ran ((.) \circ g))) = {vol}^{} (A))$
361	351 360	mpbird	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to {vol}^{} (A) - {vol}^{} (A ∖ (s ∖ ⋃ ran ((.) \circ g))) = {vol}^{*} (A \cap (s ∖ ⋃ ran ((.) \circ g)))$
362	345 361	eqtr4d	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to vol (s ∖ ⋃ ran ((.) \circ g)) = {vol}^{} (A) - {vol}^{} (A ∖ (s ∖ ⋃ ran ((.) \circ g)))$
363	331 362	breqtrrd	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to u < vol (s ∖ ⋃ ran ((.) \circ g))$
364		fvex	$⊢ vol (s ∖ ⋃ ran ((.) \circ g)) \in V$
365		eqeq1	$⊢ v = vol (s ∖ ⋃ ran ((.) \circ g)) \to (v = vol (b) \leftrightarrow vol (s ∖ ⋃ ran ((.) \circ g)) = vol (b))$
366	365	anbi2d	$⊢ v = vol (s ∖ ⋃ ran ((.) \circ g)) \to ((b \subseteq A \land v = vol (b)) \leftrightarrow (b \subseteq A \land vol (s ∖ ⋃ ran ((.) \circ g)) = vol (b)))$
367	366	rexbidv	$⊢ v = vol (s ∖ ⋃ ran ((.) \circ g)) \to (\exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land v = vol (b)) \leftrightarrow \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land vol (s ∖ ⋃ ran ((.) \circ g)) = vol (b)))$
368		breq2	$⊢ v = vol (s ∖ ⋃ ran ((.) \circ g)) \to (u < v \leftrightarrow u < vol (s ∖ ⋃ ran ((.) \circ g)))$
369	367 368	anbi12d	$⊢ v = vol (s ∖ ⋃ ran ((.) \circ g)) \to ((\exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land v = vol (b)) \land u < v) \leftrightarrow (\exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land vol (s ∖ ⋃ ran ((.) \circ g)) = vol (b)) \land u < vol (s ∖ ⋃ ran ((.) \circ g))))$
370	364 369	spcev	$⊢ (\exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land vol (s ∖ ⋃ ran ((.) \circ g)) = vol (b)) \land u < vol (s ∖ ⋃ ran ((.) \circ g))) \to \exists v (\exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land v = vol (b)) \land u < v)$
371	196 363 370	syl2anc	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{} (A) - u}{2}))) \land (s \in Clsd (topGen (ran (.))) \land (s \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) - (\frac{{vol}^{} (A) - u}{2}) < {vol}^{} (s)))) \to \exists v (\exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land v = vol (b)) \land u < v)$
372	163 371	rexlimddv	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ g) \land {vol}^{} (⋃ ran ((.) \circ g)) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A) + (\frac{{vol}^{*} (A) - u}{2}))) \to \exists v (\exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land v = vol (b)) \land u < v)$
373	142 372	exlimddv	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \land (A \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \leq {vol}^{} (A) + 1)) \to \exists v (\exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land v = vol (b)) \land u < v)$
374	78 373	exlimddv	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \to \exists v (\exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land v = vol (b)) \land u < v)$
375		eqeq1	$⊢ y = v \to (y = vol (b) \leftrightarrow v = vol (b))$
376	375	anbi2d	$⊢ y = v \to ((b \subseteq A \land y = vol (b)) \leftrightarrow (b \subseteq A \land v = vol (b)))$
377	376	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)))$
378	377	rexab	$⊢ \exists v \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} u < v \leftrightarrow \exists v (\exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land v = vol (b)) \land u < v)$
379	374 378	sylibr	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \land (u \in ℝ \land u < {vol}^{} (A))) \to \exists v \in \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} u < v$
380	2 3 42 379	eqsupd	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \to sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <) = {vol}^{} (A)$
381	380	eqcomd	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land A \in dom vol) \to {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)$

Metamath Proof Explorer

Theorem mblfinlem4

Proof