ismblfin

Description: Measurability in terms of inner and outer measure. Proposition 7 of Viaclovsky8 p. 3. (Contributed by Brendan Leahy, 4-Mar-2018) (Revised by Brendan Leahy, 28-Mar-2018)

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

Proof

Step	Hyp	Ref	Expression
1		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))\} ℝ <)$
2		elpwi	$⊢ w \in 𝒫 ℝ \to w \subseteq ℝ$
3		elmapi	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to f : ℕ ⟶ \leq \cap ℝ^{2}$
4		inss1	$⊢ w \cap A \subseteq w$
5		ovolsscl	$⊢ (w \cap A \subseteq w \land w \subseteq ℝ \land {vol}^{} (w) \in ℝ) \to {vol}^{} (w \cap A) \in ℝ$
6	4 5	mp3an1	$⊢ (w \subseteq ℝ \land {vol}^{} (w) \in ℝ) \to {vol}^{} (w \cap A) \in ℝ$
7		difss	$⊢ w ∖ A \subseteq w$
8		ovolsscl	$⊢ (w ∖ A \subseteq w \land w \subseteq ℝ \land {vol}^{} (w) \in ℝ) \to {vol}^{} (w ∖ A) \in ℝ$
9	7 8	mp3an1	$⊢ (w \subseteq ℝ \land {vol}^{} (w) \in ℝ) \to {vol}^{} (w ∖ A) \in ℝ$
10	6 9	readdcld	$⊢ (w \subseteq ℝ \land {vol}^{} (w) \in ℝ) \to {vol}^{} (w \cap A) + {vol}^{*} (w ∖ A) \in ℝ$
11	10	rexrd	$⊢ (w \subseteq ℝ \land {vol}^{} (w) \in ℝ) \to {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \in ℝ^{}$
12	11	ad3antlr	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land (w \subseteq ℝ \land {vol}^{} (w) \in ℝ)) \land f : ℕ ⟶ \leq \cap ℝ^{2}) \land w \subseteq ⋃ ran ((.) \circ f)) \to {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \in ℝ^{}$
13		rncoss	$⊢ ran ((.) \circ f) \subseteq ran (.)$
14	13	unissi	$⊢ ⋃ ran ((.) \circ f) \subseteq ⋃ ran (.)$
15		unirnioo	$⊢ ℝ = ⋃ ran (.)$
16	14 15	sseqtrri	$⊢ ⋃ ran ((.) \circ f) \subseteq ℝ$
17		ovolcl	$⊢ ⋃ ran ((.) \circ f) \subseteq ℝ \to {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ^{}$
18	16 17	mp1i	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land (w \subseteq ℝ \land {vol}^{} (w) \in ℝ)) \land f : ℕ ⟶ \leq \cap ℝ^{2}) \land w \subseteq ⋃ ran ((.) \circ f)) \to {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ^{*}$
19		eqid	$⊢ (abs \circ -) \circ f = (abs \circ -) \circ f$
20		eqid	$⊢ seq 1 (+ ((abs \circ -) \circ f)) = seq 1 (+ ((abs \circ -) \circ f))$
21	19 20	ovolsf	$⊢ f : ℕ ⟶ \leq \cap ℝ^{2} \to seq 1 (+ ((abs \circ -) \circ f)) : ℕ ⟶ [0, +∞)$
22		frn	$⊢ seq 1 (+ ((abs \circ -) \circ f)) : ℕ ⟶ [0, +∞) \to ran seq 1 (+ ((abs \circ -) \circ f)) \subseteq [0, +∞)$
23		icossxr	$⊢ [0, +∞) \subseteq ℝ^{*}$
24	22 23	sstrdi	$⊢ seq 1 (+ ((abs \circ -) \circ f)) : ℕ ⟶ [0, +∞) \to ran seq 1 (+ ((abs \circ -) \circ f)) \subseteq ℝ^{*}$
25		supxrcl	$⊢ ran seq 1 (+ ((abs \circ -) \circ f)) \subseteq ℝ^{} \to sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \in ℝ^{*}$
26	21 24 25	3syl	$⊢ f : ℕ ⟶ \leq \cap ℝ^{2} \to sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \in ℝ^{}$
27	26	ad2antlr	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land (w \subseteq ℝ \land {vol}^{} (w) \in ℝ)) \land f : ℕ ⟶ \leq \cap ℝ^{2}) \land w \subseteq ⋃ ran ((.) \circ f)) \to sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \in ℝ^{*}$
28		pnfge	$⊢ {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \in ℝ^{} \to {vol}^{} (w \cap A) + {vol}^{*} (w ∖ A) \leq +∞$
29	11 28	syl	$⊢ (w \subseteq ℝ \land {vol}^{} (w) \in ℝ) \to {vol}^{} (w \cap A) + {vol}^{*} (w ∖ A) \leq +∞$
30	29	ad2antrr	$⊢ (((w \subseteq ℝ \land {vol}^{} (w) \in ℝ) \land w \subseteq ⋃ ran ((.) \circ f)) \land {vol}^{} (⋃ ran ((.) \circ f)) = +∞) \to {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \leq +∞$
31		simpr	$⊢ (((w \subseteq ℝ \land {vol}^{} (w) \in ℝ) \land w \subseteq ⋃ ran ((.) \circ f)) \land {vol}^{} (⋃ ran ((.) \circ f)) = +∞) \to {vol}^{*} (⋃ ran ((.) \circ f)) = +∞$
32	30 31	breqtrrd	$⊢ (((w \subseteq ℝ \land {vol}^{} (w) \in ℝ) \land w \subseteq ⋃ ran ((.) \circ f)) \land {vol}^{} (⋃ ran ((.) \circ f)) = +∞) \to {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \leq {vol}^{*} (⋃ ran ((.) \circ f))$
33	32	adantlll	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land (w \subseteq ℝ \land {vol}^{} (w) \in ℝ)) \land w \subseteq ⋃ ran ((.) \circ f)) \land {vol}^{} (⋃ ran ((.) \circ f)) = +∞) \to {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \leq {vol}^{*} (⋃ ran ((.) \circ f))$
34	16 17	ax-mp	$⊢ {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ^{}$
35		nltpnft	$⊢ {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ^{} \to ({vol}^{} (⋃ ran ((.) \circ f)) = +∞ \leftrightarrow \neg {vol}^{} (⋃ ran ((.) \circ f)) < +∞)$
36	34 35	ax-mp	$⊢ {vol}^{} (⋃ ran ((.) \circ f)) = +∞ \leftrightarrow \neg {vol}^{} (⋃ ran ((.) \circ f)) < +∞$
37	36	necon2abii	$⊢ {vol}^{} (⋃ ran ((.) \circ f)) < +∞ \leftrightarrow {vol}^{} (⋃ ran ((.) \circ f)) \neq +∞$
38		ovolge0	$⊢ ⋃ ran ((.) \circ f) \subseteq ℝ \to 0 \leq {vol}^{*} (⋃ ran ((.) \circ f))$
39	16 38	ax-mp	$⊢ 0 \leq {vol}^{*} (⋃ ran ((.) \circ f))$
40		0re	$⊢ 0 \in ℝ$
41		xrre3	$⊢ (({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ^{} \land 0 \in ℝ) \land (0 \leq {vol}^{} (⋃ ran ((.) \circ f)) \land {vol}^{} (⋃ ran ((.) \circ f)) < +∞)) \to {vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ$
42	34 40 41	mpanl12	$⊢ (0 \leq {vol}^{} (⋃ ran ((.) \circ f)) \land {vol}^{} (⋃ ran ((.) \circ f)) < +∞) \to {vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ$
43	39 42	mpan	$⊢ {vol}^{} (⋃ ran ((.) \circ f)) < +∞ \to {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ$
44	37 43	sylbir	$⊢ {vol}^{} (⋃ ran ((.) \circ f)) \neq +∞ \to {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ$
45	10	ad3antlr	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land (w \subseteq ℝ \land {vol}^{} (w) \in ℝ)) \land w \subseteq ⋃ ran ((.) \circ f)) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \in ℝ$
46		simpr	$⊢ (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a)) \to z = vol (a)$
47		eleq1w	$⊢ b = a \to (b \in dom vol \leftrightarrow a \in dom vol)$
48		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
49	48	cldss	$⊢ b \in Clsd (topGen (ran (.))) \to b \subseteq ℝ$
50		dfss4	$⊢ b \subseteq ℝ \leftrightarrow ℝ ∖ (ℝ ∖ b) = b$
51	49 50	sylib	$⊢ b \in Clsd (topGen (ran (.))) \to ℝ ∖ (ℝ ∖ b) = b$
52		rembl	$⊢ ℝ \in dom vol$
53	48	cldopn	$⊢ b \in Clsd (topGen (ran (.))) \to ℝ ∖ b \in topGen (ran (.))$
54		opnmbl	$⊢ ℝ ∖ b \in topGen (ran (.)) \to ℝ ∖ b \in dom vol$
55	53 54	syl	$⊢ b \in Clsd (topGen (ran (.))) \to ℝ ∖ b \in dom vol$
56		difmbl	$⊢ (ℝ \in dom vol \land ℝ ∖ b \in dom vol) \to ℝ ∖ (ℝ ∖ b) \in dom vol$
57	52 55 56	sylancr	$⊢ b \in Clsd (topGen (ran (.))) \to ℝ ∖ (ℝ ∖ b) \in dom vol$
58	51 57	eqeltrrd	$⊢ b \in Clsd (topGen (ran (.))) \to b \in dom vol$
59	47 58	vtoclga	$⊢ a \in Clsd (topGen (ran (.))) \to a \in dom vol$
60		mblvol	$⊢ a \in dom vol \to vol (a) = {vol}^{*} (a)$
61	59 60	syl	$⊢ a \in Clsd (topGen (ran (.))) \to vol (a) = {vol}^{*} (a)$
62	46 61	sylan9eqr	$⊢ (a \in Clsd (topGen (ran (.))) \land (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))) \to z = {vol}^{*} (a)$
63	62	adantl	$⊢ ({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \land (a \in Clsd (topGen (ran (.))) \land (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a)))) \to z = {vol}^{} (a)$
64		inss1	$⊢ ⋃ ran ((.) \circ f) \cap A \subseteq ⋃ ran ((.) \circ f)$
65		sstr	$⊢ (a \subseteq ⋃ ran ((.) \circ f) \cap A \land ⋃ ran ((.) \circ f) \cap A \subseteq ⋃ ran ((.) \circ f)) \to a \subseteq ⋃ ran ((.) \circ f)$
66	64 65	mpan2	$⊢ a \subseteq ⋃ ran ((.) \circ f) \cap A \to a \subseteq ⋃ ran ((.) \circ f)$
67	66	ad2antrl	$⊢ (a \in Clsd (topGen (ran (.))) \land (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))) \to a \subseteq ⋃ ran ((.) \circ f)$
68		ovolsscl	$⊢ (a \subseteq ⋃ ran ((.) \circ f) \land ⋃ ran ((.) \circ f) \subseteq ℝ \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{} (a) \in ℝ$
69	16 68	mp3an2	$⊢ (a \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{} (a) \in ℝ$
70	69	ancoms	$⊢ ({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \land a \subseteq ⋃ ran ((.) \circ f)) \to {vol}^{} (a) \in ℝ$
71	67 70	sylan2	$⊢ ({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \land (a \in Clsd (topGen (ran (.))) \land (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a)))) \to {vol}^{} (a) \in ℝ$
72	63 71	eqeltrd	$⊢ ({vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \land (a \in Clsd (topGen (ran (.))) \land (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a)))) \to z \in ℝ$
73	72	rexlimdvaa	$⊢ {vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \to (\exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a)) \to z \in ℝ)$
74	73	abssdv	$⊢ {vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \to \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \subseteq ℝ$
75		eqeq1	$⊢ z = y \to (z = vol (a) \leftrightarrow y = vol (a))$
76	75	anbi2d	$⊢ z = y \to ((a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a)) \leftrightarrow (a \subseteq ⋃ ran ((.) \circ f) \cap A \land y = vol (a)))$
77	76	rexbidv	$⊢ z = y \to (\exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a)) \leftrightarrow \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land y = vol (a)))$
78	77	ralab	$⊢ \forall y \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} y \leq {vol}^{} (⋃ ran ((.) \circ f)) \leftrightarrow \forall y (\exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land y = vol (a)) \to y \leq {vol}^{} (⋃ ran ((.) \circ f)))$
79		simpr	$⊢ (a \subseteq ⋃ ran ((.) \circ f) \cap A \land y = vol (a)) \to y = vol (a)$
80	79 61	sylan9eqr	$⊢ (a \in Clsd (topGen (ran (.))) \land (a \subseteq ⋃ ran ((.) \circ f) \cap A \land y = vol (a))) \to y = {vol}^{*} (a)$
81		ovolss	$⊢ (a \subseteq ⋃ ran ((.) \circ f) \land ⋃ ran ((.) \circ f) \subseteq ℝ) \to {vol}^{} (a) \leq {vol}^{} (⋃ ran ((.) \circ f))$
82	66 16 81	sylancl	$⊢ a \subseteq ⋃ ran ((.) \circ f) \cap A \to {vol}^{} (a) \leq {vol}^{} (⋃ ran ((.) \circ f))$
83	82	ad2antrl	$⊢ (a \in Clsd (topGen (ran (.))) \land (a \subseteq ⋃ ran ((.) \circ f) \cap A \land y = vol (a))) \to {vol}^{} (a) \leq {vol}^{} (⋃ ran ((.) \circ f))$
84	80 83	eqbrtrd	$⊢ (a \in Clsd (topGen (ran (.))) \land (a \subseteq ⋃ ran ((.) \circ f) \cap A \land y = vol (a))) \to y \leq {vol}^{*} (⋃ ran ((.) \circ f))$
85	84	rexlimiva	$⊢ \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land y = vol (a)) \to y \leq {vol}^{*} (⋃ ran ((.) \circ f))$
86	78 85	mpgbir	$⊢ \forall y \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} y \leq {vol}^{*} (⋃ ran ((.) \circ f))$
87		brralrspcev	$⊢ ({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \land \forall y \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} y \leq {vol}^{} (⋃ ran ((.) \circ f))) \to \exists x \in ℝ \forall y \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} y \leq x$
88	86 87	mpan2	$⊢ {vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \to \exists x \in ℝ \forall y \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} y \leq x$
89		retop	$⊢ topGen (ran (.)) \in Top$
90		0cld	$⊢ topGen (ran (.)) \in Top \to \emptyset \in Clsd (topGen (ran (.)))$
91	89 90	ax-mp	$⊢ \emptyset \in Clsd (topGen (ran (.)))$
92		0ss	$⊢ \emptyset \subseteq ⋃ ran ((.) \circ f) \cap A$
93		0mbl	$⊢ \emptyset \in dom vol$
94		mblvol	$⊢ \emptyset \in dom vol \to vol (\emptyset) = {vol}^{*} (\emptyset)$
95	93 94	ax-mp	$⊢ vol (\emptyset) = {vol}^{*} (\emptyset)$
96		ovol0	$⊢ {vol}^{*} (\emptyset) = 0$
97	95 96	eqtr2i	$⊢ 0 = vol (\emptyset)$
98	92 97	pm3.2i	$⊢ (\emptyset \subseteq ⋃ ran ((.) \circ f) \cap A \land 0 = vol (\emptyset))$
99		sseq1	$⊢ a = \emptyset \to (a \subseteq ⋃ ran ((.) \circ f) \cap A \leftrightarrow \emptyset \subseteq ⋃ ran ((.) \circ f) \cap A)$
100		fveq2	$⊢ a = \emptyset \to vol (a) = vol (\emptyset)$
101	100	eqeq2d	$⊢ a = \emptyset \to (0 = vol (a) \leftrightarrow 0 = vol (\emptyset))$
102	99 101	anbi12d	$⊢ a = \emptyset \to ((a \subseteq ⋃ ran ((.) \circ f) \cap A \land 0 = vol (a)) \leftrightarrow (\emptyset \subseteq ⋃ ran ((.) \circ f) \cap A \land 0 = vol (\emptyset)))$
103	102	rspcev	$⊢ (\emptyset \in Clsd (topGen (ran (.))) \land (\emptyset \subseteq ⋃ ran ((.) \circ f) \cap A \land 0 = vol (\emptyset))) \to \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land 0 = vol (a))$
104	91 98 103	mp2an	$⊢ \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land 0 = vol (a))$
105		c0ex	$⊢ 0 \in V$
106		eqeq1	$⊢ z = 0 \to (z = vol (a) \leftrightarrow 0 = vol (a))$
107	106	anbi2d	$⊢ z = 0 \to ((a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a)) \leftrightarrow (a \subseteq ⋃ ran ((.) \circ f) \cap A \land 0 = vol (a)))$
108	107	rexbidv	$⊢ z = 0 \to (\exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a)) \leftrightarrow \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land 0 = vol (a)))$
109	105 108	elab	$⊢ 0 \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \leftrightarrow \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land 0 = vol (a))$
110	104 109	mpbir	$⊢ 0 \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\}$
111	110	ne0ii	$⊢ \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \neq \emptyset$
112		suprcl	$⊢ (\{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \subseteq ℝ \land \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \neq \emptyset \land \exists x \in ℝ \forall y \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} y \leq x) \to sup (\{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} ℝ <) \in ℝ$
113	111 112	mp3an2	$⊢ (\{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \subseteq ℝ \land \exists x \in ℝ \forall y \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} y \leq x) \to sup (\{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} ℝ <) \in ℝ$
114	74 88 113	syl2anc	$⊢ {vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \to sup (\{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} ℝ <) \in ℝ$
115		simpr	$⊢ (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c)) \to z = vol (c)$
116		eleq1w	$⊢ b = c \to (b \in dom vol \leftrightarrow c \in dom vol)$
117	116 58	vtoclga	$⊢ c \in Clsd (topGen (ran (.))) \to c \in dom vol$
118		mblvol	$⊢ c \in dom vol \to vol (c) = {vol}^{*} (c)$
119	117 118	syl	$⊢ c \in Clsd (topGen (ran (.))) \to vol (c) = {vol}^{*} (c)$
120	115 119	sylan9eqr	$⊢ (c \in Clsd (topGen (ran (.))) \land (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))) \to z = {vol}^{*} (c)$
121	120	adantl	$⊢ ({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \land (c \in Clsd (topGen (ran (.))) \land (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c)))) \to z = {vol}^{} (c)$
122		difss2	$⊢ c \subseteq ⋃ ran ((.) \circ f) ∖ A \to c \subseteq ⋃ ran ((.) \circ f)$
123	122	ad2antrl	$⊢ (c \in Clsd (topGen (ran (.))) \land (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))) \to c \subseteq ⋃ ran ((.) \circ f)$
124		ovolsscl	$⊢ (c \subseteq ⋃ ran ((.) \circ f) \land ⋃ ran ((.) \circ f) \subseteq ℝ \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{} (c) \in ℝ$
125	16 124	mp3an2	$⊢ (c \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{} (c) \in ℝ$
126	125	ancoms	$⊢ ({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \land c \subseteq ⋃ ran ((.) \circ f)) \to {vol}^{} (c) \in ℝ$
127	123 126	sylan2	$⊢ ({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \land (c \in Clsd (topGen (ran (.))) \land (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c)))) \to {vol}^{} (c) \in ℝ$
128	121 127	eqeltrd	$⊢ ({vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \land (c \in Clsd (topGen (ran (.))) \land (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c)))) \to z \in ℝ$
129	128	rexlimdvaa	$⊢ {vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \to (\exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c)) \to z \in ℝ)$
130	129	abssdv	$⊢ {vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \to \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} \subseteq ℝ$
131		eqeq1	$⊢ z = y \to (z = vol (c) \leftrightarrow y = vol (c))$
132	131	anbi2d	$⊢ z = y \to ((c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c)) \leftrightarrow (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land y = vol (c)))$
133	132	rexbidv	$⊢ z = y \to (\exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c)) \leftrightarrow \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land y = vol (c)))$
134	133	ralab	$⊢ \forall y \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} y \leq {vol}^{} (⋃ ran ((.) \circ f)) \leftrightarrow \forall y (\exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land y = vol (c)) \to y \leq {vol}^{} (⋃ ran ((.) \circ f)))$
135		simpr	$⊢ (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land y = vol (c)) \to y = vol (c)$
136	135 119	sylan9eqr	$⊢ (c \in Clsd (topGen (ran (.))) \land (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land y = vol (c))) \to y = {vol}^{*} (c)$
137		ovolss	$⊢ (c \subseteq ⋃ ran ((.) \circ f) \land ⋃ ran ((.) \circ f) \subseteq ℝ) \to {vol}^{} (c) \leq {vol}^{} (⋃ ran ((.) \circ f))$
138	122 16 137	sylancl	$⊢ c \subseteq ⋃ ran ((.) \circ f) ∖ A \to {vol}^{} (c) \leq {vol}^{} (⋃ ran ((.) \circ f))$
139	138	ad2antrl	$⊢ (c \in Clsd (topGen (ran (.))) \land (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land y = vol (c))) \to {vol}^{} (c) \leq {vol}^{} (⋃ ran ((.) \circ f))$
140	136 139	eqbrtrd	$⊢ (c \in Clsd (topGen (ran (.))) \land (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land y = vol (c))) \to y \leq {vol}^{*} (⋃ ran ((.) \circ f))$
141	140	rexlimiva	$⊢ \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land y = vol (c)) \to y \leq {vol}^{*} (⋃ ran ((.) \circ f))$
142	134 141	mpgbir	$⊢ \forall y \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} y \leq {vol}^{*} (⋃ ran ((.) \circ f))$
143		brralrspcev	$⊢ ({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \land \forall y \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} y \leq {vol}^{} (⋃ ran ((.) \circ f))) \to \exists x \in ℝ \forall y \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} y \leq x$
144	142 143	mpan2	$⊢ {vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \to \exists x \in ℝ \forall y \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} y \leq x$
145		0ss	$⊢ \emptyset \subseteq ⋃ ran ((.) \circ f) ∖ A$
146	145 97	pm3.2i	$⊢ (\emptyset \subseteq ⋃ ran ((.) \circ f) ∖ A \land 0 = vol (\emptyset))$
147		sseq1	$⊢ c = \emptyset \to (c \subseteq ⋃ ran ((.) \circ f) ∖ A \leftrightarrow \emptyset \subseteq ⋃ ran ((.) \circ f) ∖ A)$
148		fveq2	$⊢ c = \emptyset \to vol (c) = vol (\emptyset)$
149	148	eqeq2d	$⊢ c = \emptyset \to (0 = vol (c) \leftrightarrow 0 = vol (\emptyset))$
150	147 149	anbi12d	$⊢ c = \emptyset \to ((c \subseteq ⋃ ran ((.) \circ f) ∖ A \land 0 = vol (c)) \leftrightarrow (\emptyset \subseteq ⋃ ran ((.) \circ f) ∖ A \land 0 = vol (\emptyset)))$
151	150	rspcev	$⊢ (\emptyset \in Clsd (topGen (ran (.))) \land (\emptyset \subseteq ⋃ ran ((.) \circ f) ∖ A \land 0 = vol (\emptyset))) \to \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land 0 = vol (c))$
152	91 146 151	mp2an	$⊢ \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land 0 = vol (c))$
153		eqeq1	$⊢ z = 0 \to (z = vol (c) \leftrightarrow 0 = vol (c))$
154	153	anbi2d	$⊢ z = 0 \to ((c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c)) \leftrightarrow (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land 0 = vol (c)))$
155	154	rexbidv	$⊢ z = 0 \to (\exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c)) \leftrightarrow \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land 0 = vol (c)))$
156	105 155	elab	$⊢ 0 \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} \leftrightarrow \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land 0 = vol (c))$
157	152 156	mpbir	$⊢ 0 \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\}$
158	157	ne0ii	$⊢ \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} \neq \emptyset$
159		suprcl	$⊢ (\{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} \subseteq ℝ \land \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} \neq \emptyset \land \exists x \in ℝ \forall y \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} y \leq x) \to sup (\{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} ℝ <) \in ℝ$
160	158 159	mp3an2	$⊢ (\{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} \subseteq ℝ \land \exists x \in ℝ \forall y \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} y \leq x) \to sup (\{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} ℝ <) \in ℝ$
161	130 144 160	syl2anc	$⊢ {vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \to sup (\{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} ℝ <) \in ℝ$
162	114 161	readdcld	$⊢ {vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \to sup (\{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} ℝ <) + sup (\{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} ℝ <) \in ℝ$
163	162	adantl	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land (w \subseteq ℝ \land {vol}^{} (w) \in ℝ)) \land w \subseteq ⋃ ran ((.) \circ f)) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to sup (\{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} ℝ <) + sup (\{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} ℝ <) \in ℝ$
164		simpr	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land (w \subseteq ℝ \land {vol}^{} (w) \in ℝ)) \land w \subseteq ⋃ ran ((.) \circ f)) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ$
165	6	ad2antrr	$⊢ (((w \subseteq ℝ \land {vol}^{} (w) \in ℝ) \land w \subseteq ⋃ ran ((.) \circ f)) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{*} (w \cap A) \in ℝ$
166	9	ad2antrr	$⊢ (((w \subseteq ℝ \land {vol}^{} (w) \in ℝ) \land w \subseteq ⋃ ran ((.) \circ f)) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{*} (w ∖ A) \in ℝ$
167		ovolsscl	$⊢ (⋃ ran ((.) \circ f) \cap A \subseteq ⋃ ran ((.) \circ f) \land ⋃ ran ((.) \circ f) \subseteq ℝ \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{} (⋃ ran ((.) \circ f) \cap A) \in ℝ$
168	64 16 167	mp3an12	$⊢ {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \to {vol}^{} (⋃ ran ((.) \circ f) \cap A) \in ℝ$
169	168	adantl	$⊢ (((w \subseteq ℝ \land {vol}^{} (w) \in ℝ) \land w \subseteq ⋃ ran ((.) \circ f)) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{*} (⋃ ran ((.) \circ f) \cap A) \in ℝ$
170		difss	$⊢ ⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ f)$
171		ovolsscl	$⊢ (⋃ ran ((.) \circ f) ∖ A \subseteq ⋃ ran ((.) \circ f) \land ⋃ ran ((.) \circ f) \subseteq ℝ \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{} (⋃ ran ((.) \circ f) ∖ A) \in ℝ$
172	170 16 171	mp3an12	$⊢ {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \to {vol}^{} (⋃ ran ((.) \circ f) ∖ A) \in ℝ$
173	172	adantl	$⊢ (((w \subseteq ℝ \land {vol}^{} (w) \in ℝ) \land w \subseteq ⋃ ran ((.) \circ f)) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{*} (⋃ ran ((.) \circ f) ∖ A) \in ℝ$
174		ssrin	$⊢ w \subseteq ⋃ ran ((.) \circ f) \to w \cap A \subseteq ⋃ ran ((.) \circ f) \cap A$
175	64 16	sstri	$⊢ ⋃ ran ((.) \circ f) \cap A \subseteq ℝ$
176		ovolss	$⊢ (w \cap A \subseteq ⋃ ran ((.) \circ f) \cap A \land ⋃ ran ((.) \circ f) \cap A \subseteq ℝ) \to {vol}^{} (w \cap A) \leq {vol}^{} (⋃ ran ((.) \circ f) \cap A)$
177	174 175 176	sylancl	$⊢ w \subseteq ⋃ ran ((.) \circ f) \to {vol}^{} (w \cap A) \leq {vol}^{} (⋃ ran ((.) \circ f) \cap A)$
178	177	ad2antlr	$⊢ (((w \subseteq ℝ \land {vol}^{} (w) \in ℝ) \land w \subseteq ⋃ ran ((.) \circ f)) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{} (w \cap A) \leq {vol}^{} (⋃ ran ((.) \circ f) \cap A)$
179		ssdif	$⊢ w \subseteq ⋃ ran ((.) \circ f) \to w ∖ A \subseteq ⋃ ran ((.) \circ f) ∖ A$
180	170 16	sstri	$⊢ ⋃ ran ((.) \circ f) ∖ A \subseteq ℝ$
181		ovolss	$⊢ (w ∖ A \subseteq ⋃ ran ((.) \circ f) ∖ A \land ⋃ ran ((.) \circ f) ∖ A \subseteq ℝ) \to {vol}^{} (w ∖ A) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A)$
182	179 180 181	sylancl	$⊢ w \subseteq ⋃ ran ((.) \circ f) \to {vol}^{} (w ∖ A) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A)$
183	182	ad2antlr	$⊢ (((w \subseteq ℝ \land {vol}^{} (w) \in ℝ) \land w \subseteq ⋃ ran ((.) \circ f)) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{} (w ∖ A) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ A)$
184	165 166 169 173 178 183	le2addd	$⊢ (((w \subseteq ℝ \land {vol}^{} (w) \in ℝ) \land w \subseteq ⋃ ran ((.) \circ f)) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \leq {vol}^{} (⋃ ran ((.) \circ f) \cap A) + {vol}^{} (⋃ ran ((.) \circ f) ∖ A)$
185		dfin4	$⊢ ⋃ ran ((.) \circ f) \cap A = ⋃ ran ((.) \circ f) ∖ (⋃ ran ((.) \circ f) ∖ A)$
186	185	fveq2i	$⊢ {vol}^{} (⋃ ran ((.) \circ f) \cap A) = {vol}^{} (⋃ ran ((.) \circ f) ∖ (⋃ ran ((.) \circ f) ∖ A))$
187	186	oveq1i	$⊢ {vol}^{} (⋃ ran ((.) \circ f) \cap A) + {vol}^{} (⋃ ran ((.) \circ f) ∖ A) = {vol}^{} (⋃ ran ((.) \circ f) ∖ (⋃ ran ((.) \circ f) ∖ A)) + {vol}^{} (⋃ ran ((.) \circ f) ∖ A)$
188	184 187	breqtrdi	$⊢ (((w \subseteq ℝ \land {vol}^{} (w) \in ℝ) \land w \subseteq ⋃ ran ((.) \circ f)) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ (⋃ ran ((.) \circ f) ∖ A)) + {vol}^{} (⋃ ran ((.) \circ f) ∖ A)$
189	188	adantlll	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land (w \subseteq ℝ \land {vol}^{} (w) \in ℝ)) \land w \subseteq ⋃ ran ((.) \circ f)) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \leq {vol}^{} (⋃ ran ((.) \circ f) ∖ (⋃ ran ((.) \circ f) ∖ A)) + {vol}^{} (⋃ ran ((.) \circ f) ∖ A)$
190		simpll	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land (w \subseteq ℝ \land {vol}^{} (w) \in ℝ)) \land w \subseteq ⋃ ran ((.) \circ f)) \to ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{*} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <))$
191	185	sseq2i	$⊢ a \subseteq ⋃ ran ((.) \circ f) \cap A \leftrightarrow a \subseteq ⋃ ran ((.) \circ f) ∖ (⋃ ran ((.) \circ f) ∖ A)$
192	191	anbi1i	$⊢ (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a)) \leftrightarrow (a \subseteq ⋃ ran ((.) \circ f) ∖ (⋃ ran ((.) \circ f) ∖ A) \land z = vol (a))$
193	192	rexbii	$⊢ \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a)) \leftrightarrow \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) ∖ (⋃ ran ((.) \circ f) ∖ A) \land z = vol (a))$
194	193	abbii	$⊢ \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} = \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) ∖ (⋃ ran ((.) \circ f) ∖ A) \land z = vol (a))\}$
195	194	supeq1i	$⊢ sup (\{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} ℝ <) = sup (\{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) ∖ (⋃ ran ((.) \circ f) ∖ A) \land z = vol (a))\} ℝ <)$
196	16	jctl	$⊢ {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \to (⋃ ran ((.) \circ f) \subseteq ℝ \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ)$
197	196	adantl	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to (⋃ ran ((.) \circ f) \subseteq ℝ \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ)$
198	172 180	jctil	$⊢ {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \to (⋃ ran ((.) \circ f) ∖ A \subseteq ℝ \land {vol}^{} (⋃ ran ((.) \circ f) ∖ A) \in ℝ)$
199	198	adantl	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to (⋃ ran ((.) \circ f) ∖ A \subseteq ℝ \land {vol}^{} (⋃ ran ((.) \circ f) ∖ A) \in ℝ)$
200		ltso	$⊢ < Or ℝ$
201	200	a1i	$⊢ {vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \to < Or ℝ$
202		id	$⊢ {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \to {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ$
203		vex	$⊢ x \in V$
204		eqeq1	$⊢ z = x \to (z = vol (c) \leftrightarrow x = vol (c))$
205	204	anbi2d	$⊢ z = x \to ((c \subseteq ⋃ ran ((.) \circ f) \land z = vol (c)) \leftrightarrow (c \subseteq ⋃ ran ((.) \circ f) \land x = vol (c)))$
206	205	rexbidv	$⊢ z = x \to (\exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) \land z = vol (c)) \leftrightarrow \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) \land x = vol (c)))$
207	203 206	elab	$⊢ x \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) \land z = vol (c))\} \leftrightarrow \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) \land x = vol (c))$
208	16 137	mpan2	$⊢ c \subseteq ⋃ ran ((.) \circ f) \to {vol}^{} (c) \leq {vol}^{} (⋃ ran ((.) \circ f))$
209	208	ad2antrl	$⊢ (c \in Clsd (topGen (ran (.))) \land (c \subseteq ⋃ ran ((.) \circ f) \land x = vol (c))) \to {vol}^{} (c) \leq {vol}^{} (⋃ ran ((.) \circ f))$
210	48	cldss	$⊢ c \in Clsd (topGen (ran (.))) \to c \subseteq ℝ$
211		ovolcl	$⊢ c \subseteq ℝ \to {vol}^{} (c) \in ℝ^{}$
212	210 211	syl	$⊢ c \in Clsd (topGen (ran (.))) \to {vol}^{} (c) \in ℝ^{}$
213		xrlenlt	$⊢ ({vol}^{} (c) \in ℝ^{} \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ^{}) \to ({vol}^{} (c) \leq {vol}^{} (⋃ ran ((.) \circ f)) \leftrightarrow \neg {vol}^{} (⋃ ran ((.) \circ f)) < {vol}^{} (c))$
214	212 34 213	sylancl	$⊢ c \in Clsd (topGen (ran (.))) \to ({vol}^{} (c) \leq {vol}^{} (⋃ ran ((.) \circ f)) \leftrightarrow \neg {vol}^{} (⋃ ran ((.) \circ f)) < {vol}^{} (c))$
215	214	adantr	$⊢ (c \in Clsd (topGen (ran (.))) \land (c \subseteq ⋃ ran ((.) \circ f) \land x = vol (c))) \to ({vol}^{} (c) \leq {vol}^{} (⋃ ran ((.) \circ f)) \leftrightarrow \neg {vol}^{} (⋃ ran ((.) \circ f)) < {vol}^{} (c))$
216		id	$⊢ x = vol (c) \to x = vol (c)$
217	216 119	sylan9eqr	$⊢ (c \in Clsd (topGen (ran (.))) \land x = vol (c)) \to x = {vol}^{*} (c)$
218		breq2	$⊢ x = {vol}^{} (c) \to ({vol}^{} (⋃ ran ((.) \circ f)) < x \leftrightarrow {vol}^{} (⋃ ran ((.) \circ f)) < {vol}^{} (c))$
219	218	notbid	$⊢ x = {vol}^{} (c) \to (\neg {vol}^{} (⋃ ran ((.) \circ f)) < x \leftrightarrow \neg {vol}^{} (⋃ ran ((.) \circ f)) < {vol}^{} (c))$
220	217 219	syl	$⊢ (c \in Clsd (topGen (ran (.))) \land x = vol (c)) \to (\neg {vol}^{} (⋃ ran ((.) \circ f)) < x \leftrightarrow \neg {vol}^{} (⋃ ran ((.) \circ f)) < {vol}^{*} (c))$
221	220	adantrl	$⊢ (c \in Clsd (topGen (ran (.))) \land (c \subseteq ⋃ ran ((.) \circ f) \land x = vol (c))) \to (\neg {vol}^{} (⋃ ran ((.) \circ f)) < x \leftrightarrow \neg {vol}^{} (⋃ ran ((.) \circ f)) < {vol}^{*} (c))$
222	215 221	bitr4d	$⊢ (c \in Clsd (topGen (ran (.))) \land (c \subseteq ⋃ ran ((.) \circ f) \land x = vol (c))) \to ({vol}^{} (c) \leq {vol}^{} (⋃ ran ((.) \circ f)) \leftrightarrow \neg {vol}^{*} (⋃ ran ((.) \circ f)) < x)$
223	209 222	mpbid	$⊢ (c \in Clsd (topGen (ran (.))) \land (c \subseteq ⋃ ran ((.) \circ f) \land x = vol (c))) \to \neg {vol}^{*} (⋃ ran ((.) \circ f)) < x$
224	223	rexlimiva	$⊢ \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) \land x = vol (c)) \to \neg {vol}^{*} (⋃ ran ((.) \circ f)) < x$
225	207 224	sylbi	$⊢ x \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) \land z = vol (c))\} \to \neg {vol}^{*} (⋃ ran ((.) \circ f)) < x$
226	225	adantl	$⊢ ({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \land x \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) \land z = vol (c))\}) \to \neg {vol}^{} (⋃ ran ((.) \circ f)) < x$
227		retopbas	$⊢ ran (.) \in TopBases$
228		bastg	$⊢ ran (.) \in TopBases \to ran (.) \subseteq topGen (ran (.))$
229	227 228	ax-mp	$⊢ ran (.) \subseteq topGen (ran (.))$
230	13 229	sstri	$⊢ ran ((.) \circ f) \subseteq topGen (ran (.))$
231		uniopn	$⊢ (topGen (ran (.)) \in Top \land ran ((.) \circ f) \subseteq topGen (ran (.))) \to ⋃ ran ((.) \circ f) \in topGen (ran (.))$
232	89 230 231	mp2an	$⊢ ⋃ ran ((.) \circ f) \in topGen (ran (.))$
233		mblfinlem2	$⊢ (⋃ ran ((.) \circ f) \in topGen (ran (.)) \land x \in ℝ \land x < {vol}^{} (⋃ ran ((.) \circ f))) \to \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) \land x < {vol}^{} (c))$
234	232 233	mp3an1	$⊢ (x \in ℝ \land x < {vol}^{} (⋃ ran ((.) \circ f))) \to \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) \land x < {vol}^{} (c))$
235	119	eqcomd	$⊢ c \in Clsd (topGen (ran (.))) \to {vol}^{*} (c) = vol (c)$
236	235	anim1i	$⊢ (c \in Clsd (topGen (ran (.))) \land x < {vol}^{} (c)) \to ({vol}^{} (c) = vol (c) \land x < {vol}^{*} (c))$
237	236	ex	$⊢ c \in Clsd (topGen (ran (.))) \to (x < {vol}^{} (c) \to ({vol}^{} (c) = vol (c) \land x < {vol}^{*} (c)))$
238	237	anim2d	$⊢ c \in Clsd (topGen (ran (.))) \to ((c \subseteq ⋃ ran ((.) \circ f) \land x < {vol}^{} (c)) \to (c \subseteq ⋃ ran ((.) \circ f) \land ({vol}^{} (c) = vol (c) \land x < {vol}^{*} (c))))$
239		fvex	$⊢ {vol}^{*} (c) \in V$
240		eqeq1	$⊢ y = {vol}^{} (c) \to (y = vol (c) \leftrightarrow {vol}^{} (c) = vol (c))$
241	240	anbi2d	$⊢ y = {vol}^{} (c) \to ((c \subseteq ⋃ ran ((.) \circ f) \land y = vol (c)) \leftrightarrow (c \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (c) = vol (c)))$
242		breq2	$⊢ y = {vol}^{} (c) \to (x < y \leftrightarrow x < {vol}^{} (c))$
243	241 242	anbi12d	$⊢ y = {vol}^{} (c) \to (((c \subseteq ⋃ ran ((.) \circ f) \land y = vol (c)) \land x < y) \leftrightarrow ((c \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (c) = vol (c)) \land x < {vol}^{*} (c)))$
244	239 243	spcev	$⊢ ((c \subseteq ⋃ ran ((.) \circ f) \land {vol}^{} (c) = vol (c)) \land x < {vol}^{} (c)) \to \exists y ((c \subseteq ⋃ ran ((.) \circ f) \land y = vol (c)) \land x < y)$
245	244	anasss	$⊢ (c \subseteq ⋃ ran ((.) \circ f) \land ({vol}^{} (c) = vol (c) \land x < {vol}^{} (c))) \to \exists y ((c \subseteq ⋃ ran ((.) \circ f) \land y = vol (c)) \land x < y)$
246	238 245	syl6	$⊢ c \in Clsd (topGen (ran (.))) \to ((c \subseteq ⋃ ran ((.) \circ f) \land x < {vol}^{*} (c)) \to \exists y ((c \subseteq ⋃ ran ((.) \circ f) \land y = vol (c)) \land x < y))$
247	246	reximia	$⊢ \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) \land x < {vol}^{*} (c)) \to \exists c \in Clsd (topGen (ran (.))) \exists y ((c \subseteq ⋃ ran ((.) \circ f) \land y = vol (c)) \land x < y)$
248	234 247	syl	$⊢ (x \in ℝ \land x < {vol}^{*} (⋃ ran ((.) \circ f))) \to \exists c \in Clsd (topGen (ran (.))) \exists y ((c \subseteq ⋃ ran ((.) \circ f) \land y = vol (c)) \land x < y)$
249		r19.41v	$⊢ \exists c \in Clsd (topGen (ran (.))) ((c \subseteq ⋃ ran ((.) \circ f) \land y = vol (c)) \land x < y) \leftrightarrow (\exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) \land y = vol (c)) \land x < y)$
250	249	exbii	$⊢ \exists y \exists c \in Clsd (topGen (ran (.))) ((c \subseteq ⋃ ran ((.) \circ f) \land y = vol (c)) \land x < y) \leftrightarrow \exists y (\exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) \land y = vol (c)) \land x < y)$
251		rexcom4	$⊢ \exists c \in Clsd (topGen (ran (.))) \exists y ((c \subseteq ⋃ ran ((.) \circ f) \land y = vol (c)) \land x < y) \leftrightarrow \exists y \exists c \in Clsd (topGen (ran (.))) ((c \subseteq ⋃ ran ((.) \circ f) \land y = vol (c)) \land x < y)$
252	131	anbi2d	$⊢ z = y \to ((c \subseteq ⋃ ran ((.) \circ f) \land z = vol (c)) \leftrightarrow (c \subseteq ⋃ ran ((.) \circ f) \land y = vol (c)))$
253	252	rexbidv	$⊢ z = y \to (\exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) \land z = vol (c)) \leftrightarrow \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) \land y = vol (c)))$
254	253	rexab	$⊢ \exists y \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) \land z = vol (c))\} x < y \leftrightarrow \exists y (\exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) \land y = vol (c)) \land x < y)$
255	250 251 254	3bitr4i	$⊢ \exists c \in Clsd (topGen (ran (.))) \exists y ((c \subseteq ⋃ ran ((.) \circ f) \land y = vol (c)) \land x < y) \leftrightarrow \exists y \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) \land z = vol (c))\} x < y$
256	248 255	sylib	$⊢ (x \in ℝ \land x < {vol}^{*} (⋃ ran ((.) \circ f))) \to \exists y \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) \land z = vol (c))\} x < y$
257	256	adantl	$⊢ ({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \land (x \in ℝ \land x < {vol}^{} (⋃ ran ((.) \circ f)))) \to \exists y \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) \land z = vol (c))\} x < y$
258	201 202 226 257	eqsupd	$⊢ {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \to sup (\{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) \land z = vol (c))\} ℝ <) = {vol}^{} (⋃ ran ((.) \circ f))$
259	258	eqcomd	$⊢ {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \to {vol}^{} (⋃ ran ((.) \circ f)) = sup (\{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) \land z = vol (c))\} ℝ <)$
260	259	adantl	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{} (⋃ ran ((.) \circ f)) = sup (\{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) \land z = vol (c))\} ℝ <)$
261		sseq1	$⊢ c = a \to (c \subseteq ⋃ ran ((.) \circ f) \leftrightarrow a \subseteq ⋃ ran ((.) \circ f))$
262		fveq2	$⊢ c = a \to vol (c) = vol (a)$
263	262	eqeq2d	$⊢ c = a \to (z = vol (c) \leftrightarrow z = vol (a))$
264	261 263	anbi12d	$⊢ c = a \to ((c \subseteq ⋃ ran ((.) \circ f) \land z = vol (c)) \leftrightarrow (a \subseteq ⋃ ran ((.) \circ f) \land z = vol (a)))$
265	264	cbvrexvw	$⊢ \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) \land z = vol (c)) \leftrightarrow \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \land z = vol (a))$
266	265	abbii	$⊢ \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) \land z = vol (c))\} = \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \land z = vol (a))\}$
267	266	supeq1i	$⊢ sup (\{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) \land z = vol (c))\} ℝ <) = sup (\{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \land z = vol (a))\} ℝ <)$
268	260 267	eqtrdi	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{} (⋃ ran ((.) \circ f)) = sup (\{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \land z = vol (a))\} ℝ <)$
269		simpll	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to (A \subseteq ℝ \land {vol}^{} (A) \in ℝ)$
270		eqeq1	$⊢ y = z \to (y = vol (b) \leftrightarrow z = vol (b))$
271	270	anbi2d	$⊢ y = z \to ((b \subseteq A \land y = vol (b)) \leftrightarrow (b \subseteq A \land z = vol (b)))$
272	271	rexbidv	$⊢ y = z \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 z = vol (b)))$
273		sseq1	$⊢ b = c \to (b \subseteq A \leftrightarrow c \subseteq A)$
274		fveq2	$⊢ b = c \to vol (b) = vol (c)$
275	274	eqeq2d	$⊢ b = c \to (z = vol (b) \leftrightarrow z = vol (c))$
276	273 275	anbi12d	$⊢ b = c \to ((b \subseteq A \land z = vol (b)) \leftrightarrow (c \subseteq A \land z = vol (c)))$
277	276	cbvrexvw	$⊢ \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land z = vol (b)) \leftrightarrow \exists c \in Clsd (topGen (ran (.))) (c \subseteq A \land z = vol (c))$
278	272 277	bitrdi	$⊢ y = z \to (\exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b)) \leftrightarrow \exists c \in Clsd (topGen (ran (.))) (c \subseteq A \land z = vol (c)))$
279	278	cbvabv	$⊢ \{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} = \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq A \land z = vol (c))\}$
280	279	supeq1i	$⊢ sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <) = sup (\{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq A \land z = vol (c))\} ℝ <)$
281	280	eqeq2i	$⊢ {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <) \leftrightarrow {vol}^{} (A) = sup (\{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq A \land z = vol (c))\} ℝ <)$
282	281	biimpi	$⊢ {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <) \to {vol}^{} (A) = sup (\{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq A \land z = vol (c))\} ℝ <)$
283	282	ad2antlr	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{} (A) = sup (\{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq A \land z = vol (c))\} ℝ <)$
284		mblfinlem3	$⊢ ((⋃ ran ((.) \circ f) \subseteq ℝ \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \land (A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land ({vol}^{} (⋃ ran ((.) \circ f)) = sup (\{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) \land z = vol (c))\} ℝ <) \land {vol}^{} (A) = sup (\{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq A \land z = vol (c))\} ℝ <))) \to sup (\{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} ℝ <) = {vol}^{*} (⋃ ran ((.) \circ f) ∖ A)$
285	197 269 260 283 284	syl112anc	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to sup (\{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} ℝ <) = {vol}^{} (⋃ ran ((.) \circ f) ∖ A)$
286		sseq1	$⊢ c = a \to (c \subseteq ⋃ ran ((.) \circ f) ∖ A \leftrightarrow a \subseteq ⋃ ran ((.) \circ f) ∖ A)$
287	286 263	anbi12d	$⊢ c = a \to ((c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c)) \leftrightarrow (a \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (a)))$
288	287	cbvrexvw	$⊢ \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c)) \leftrightarrow \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (a))$
289	288	abbii	$⊢ \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} = \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (a))\}$
290	289	supeq1i	$⊢ sup (\{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} ℝ <) = sup (\{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (a))\} ℝ <)$
291	285 290	eqtr3di	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{} (⋃ ran ((.) \circ f) ∖ A) = sup (\{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (a))\} ℝ <)$
292		mblfinlem3	$⊢ ((⋃ ran ((.) \circ f) \subseteq ℝ \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \land (⋃ ran ((.) \circ f) ∖ A \subseteq ℝ \land {vol}^{} (⋃ ran ((.) \circ f) ∖ A) \in ℝ) \land ({vol}^{} (⋃ ran ((.) \circ f)) = sup (\{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \land z = vol (a))\} ℝ <) \land {vol}^{} (⋃ ran ((.) \circ f) ∖ A) = sup (\{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (a))\} ℝ <))) \to sup (\{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) ∖ (⋃ ran ((.) \circ f) ∖ A) \land z = vol (a))\} ℝ <) = {vol}^{*} (⋃ ran ((.) \circ f) ∖ (⋃ ran ((.) \circ f) ∖ A))$
293	197 199 268 291 292	syl112anc	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to sup (\{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) ∖ (⋃ ran ((.) \circ f) ∖ A) \land z = vol (a))\} ℝ <) = {vol}^{} (⋃ ran ((.) \circ f) ∖ (⋃ ran ((.) \circ f) ∖ A))$
294	195 293	eqtrid	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to sup (\{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} ℝ <) = {vol}^{} (⋃ ran ((.) \circ f) ∖ (⋃ ran ((.) \circ f) ∖ A))$
295	294 285	oveq12d	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to sup (\{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} ℝ <) + sup (\{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} ℝ <) = {vol}^{} (⋃ ran ((.) \circ f) ∖ (⋃ ran ((.) \circ f) ∖ A)) + {vol}^{*} (⋃ ran ((.) \circ f) ∖ A)$
296	190 295	sylan	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land (w \subseteq ℝ \land {vol}^{} (w) \in ℝ)) \land w \subseteq ⋃ ran ((.) \circ f)) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to sup (\{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} ℝ <) + sup (\{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} ℝ <) = {vol}^{} (⋃ ran ((.) \circ f) ∖ (⋃ ran ((.) \circ f) ∖ A)) + {vol}^{} (⋃ ran ((.) \circ f) ∖ A)$
297	189 296	breqtrrd	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land (w \subseteq ℝ \land {vol}^{} (w) \in ℝ)) \land w \subseteq ⋃ ran ((.) \circ f)) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \leq sup (\{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} ℝ <) + sup (\{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} ℝ <)$
298		ne0i	$⊢ 0 \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \to \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \neq \emptyset$
299	110 298	mp1i	$⊢ {vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \to \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \neq \emptyset$
300		ne0i	$⊢ 0 \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} \to \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} \neq \emptyset$
301	157 300	mp1i	$⊢ {vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \to \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} \neq \emptyset$
302		eqid	$⊢ \{t \| \exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} t = u + v\} = \{t \| \exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} t = u + v\}$
303	74 299 88 130 301 144 302	supadd	$⊢ {vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \to sup (\{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} ℝ <) + sup (\{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} ℝ <) = sup (\{t \| \exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} t = u + v\} ℝ <)$
304		reeanv	$⊢ \exists a \in Clsd (topGen (ran (.))) \exists c \in Clsd (topGen (ran (.))) ((a \subseteq ⋃ ran ((.) \circ f) \cap A \land u = vol (a)) \land (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land v = vol (c))) \leftrightarrow (\exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land u = vol (a)) \land \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land v = vol (c)))$
305		vex	$⊢ u \in V$
306		eqeq1	$⊢ z = u \to (z = vol (a) \leftrightarrow u = vol (a))$
307	306	anbi2d	$⊢ z = u \to ((a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a)) \leftrightarrow (a \subseteq ⋃ ran ((.) \circ f) \cap A \land u = vol (a)))$
308	307	rexbidv	$⊢ z = u \to (\exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a)) \leftrightarrow \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land u = vol (a)))$
309	305 308	elab	$⊢ u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \leftrightarrow \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land u = vol (a))$
310		vex	$⊢ v \in V$
311		eqeq1	$⊢ z = v \to (z = vol (c) \leftrightarrow v = vol (c))$
312	311	anbi2d	$⊢ z = v \to ((c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c)) \leftrightarrow (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land v = vol (c)))$
313	312	rexbidv	$⊢ z = v \to (\exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c)) \leftrightarrow \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land v = vol (c)))$
314	310 313	elab	$⊢ v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} \leftrightarrow \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land v = vol (c))$
315	309 314	anbi12i	$⊢ (u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \land v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\}) \leftrightarrow (\exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land u = vol (a)) \land \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land v = vol (c)))$
316	304 315	bitr4i	$⊢ \exists a \in Clsd (topGen (ran (.))) \exists c \in Clsd (topGen (ran (.))) ((a \subseteq ⋃ ran ((.) \circ f) \cap A \land u = vol (a)) \land (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land v = vol (c))) \leftrightarrow (u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \land v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\})$
317		an4	$⊢ ((a \subseteq ⋃ ran ((.) \circ f) \cap A \land c \subseteq ⋃ ran ((.) \circ f) ∖ A) \land (u = vol (a) \land v = vol (c))) \leftrightarrow ((a \subseteq ⋃ ran ((.) \circ f) \cap A \land u = vol (a)) \land (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land v = vol (c)))$
318		oveq12	$⊢ (u = vol (a) \land v = vol (c)) \to u + v = vol (a) + vol (c)$
319	59	adantr	$⊢ (a \in Clsd (topGen (ran (.))) \land c \in Clsd (topGen (ran (.)))) \to a \in dom vol$
320	319	ad2antlr	$⊢ (({vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \land (a \in Clsd (topGen (ran (.))) \land c \in Clsd (topGen (ran (.))))) \land (a \subseteq ⋃ ran ((.) \circ f) \cap A \land c \subseteq ⋃ ran ((.) \circ f) ∖ A)) \to a \in dom vol$
321	117	adantl	$⊢ (a \in Clsd (topGen (ran (.))) \land c \in Clsd (topGen (ran (.)))) \to c \in dom vol$
322	321	ad2antlr	$⊢ (({vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \land (a \in Clsd (topGen (ran (.))) \land c \in Clsd (topGen (ran (.))))) \land (a \subseteq ⋃ ran ((.) \circ f) \cap A \land c \subseteq ⋃ ran ((.) \circ f) ∖ A)) \to c \in dom vol$
323		ss2in	$⊢ (a \subseteq ⋃ ran ((.) \circ f) \cap A \land c \subseteq ⋃ ran ((.) \circ f) ∖ A) \to a \cap c \subseteq (⋃ ran ((.) \circ f) \cap A) \cap (⋃ ran ((.) \circ f) ∖ A)$
324	185	ineq1i	$⊢ (⋃ ran ((.) \circ f) \cap A) \cap (⋃ ran ((.) \circ f) ∖ A) = (⋃ ran ((.) \circ f) ∖ (⋃ ran ((.) \circ f) ∖ A)) \cap (⋃ ran ((.) \circ f) ∖ A)$
325		incom	$⊢ (⋃ ran ((.) \circ f) ∖ (⋃ ran ((.) \circ f) ∖ A)) \cap (⋃ ran ((.) \circ f) ∖ A) = (⋃ ran ((.) \circ f) ∖ A) \cap (⋃ ran ((.) \circ f) ∖ (⋃ ran ((.) \circ f) ∖ A))$
326		disjdif	$⊢ (⋃ ran ((.) \circ f) ∖ A) \cap (⋃ ran ((.) \circ f) ∖ (⋃ ran ((.) \circ f) ∖ A)) = \emptyset$
327	324 325 326	3eqtri	$⊢ (⋃ ran ((.) \circ f) \cap A) \cap (⋃ ran ((.) \circ f) ∖ A) = \emptyset$
328	323 327	sseqtrdi	$⊢ (a \subseteq ⋃ ran ((.) \circ f) \cap A \land c \subseteq ⋃ ran ((.) \circ f) ∖ A) \to a \cap c \subseteq \emptyset$
329		ss0	$⊢ a \cap c \subseteq \emptyset \to a \cap c = \emptyset$
330	328 329	syl	$⊢ (a \subseteq ⋃ ran ((.) \circ f) \cap A \land c \subseteq ⋃ ran ((.) \circ f) ∖ A) \to a \cap c = \emptyset$
331	330	adantl	$⊢ (({vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \land (a \in Clsd (topGen (ran (.))) \land c \in Clsd (topGen (ran (.))))) \land (a \subseteq ⋃ ran ((.) \circ f) \cap A \land c \subseteq ⋃ ran ((.) \circ f) ∖ A)) \to a \cap c = \emptyset$
332	61	adantr	$⊢ (a \in Clsd (topGen (ran (.))) \land c \in Clsd (topGen (ran (.)))) \to vol (a) = {vol}^{*} (a)$
333	332	ad2antlr	$⊢ (({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \land (a \in Clsd (topGen (ran (.))) \land c \in Clsd (topGen (ran (.))))) \land (a \subseteq ⋃ ran ((.) \circ f) \cap A \land c \subseteq ⋃ ran ((.) \circ f) ∖ A)) \to vol (a) = {vol}^{} (a)$
334	66 16	jctir	$⊢ a \subseteq ⋃ ran ((.) \circ f) \cap A \to (a \subseteq ⋃ ran ((.) \circ f) \land ⋃ ran ((.) \circ f) \subseteq ℝ)$
335	68	3expa	$⊢ ((a \subseteq ⋃ ran ((.) \circ f) \land ⋃ ran ((.) \circ f) \subseteq ℝ) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{} (a) \in ℝ$
336	334 335	sylan	$⊢ (a \subseteq ⋃ ran ((.) \circ f) \cap A \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{} (a) \in ℝ$
337	336	ancoms	$⊢ ({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \land a \subseteq ⋃ ran ((.) \circ f) \cap A) \to {vol}^{} (a) \in ℝ$
338	337	ad2ant2r	$⊢ (({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \land (a \in Clsd (topGen (ran (.))) \land c \in Clsd (topGen (ran (.))))) \land (a \subseteq ⋃ ran ((.) \circ f) \cap A \land c \subseteq ⋃ ran ((.) \circ f) ∖ A)) \to {vol}^{} (a) \in ℝ$
339	333 338	eqeltrd	$⊢ (({vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \land (a \in Clsd (topGen (ran (.))) \land c \in Clsd (topGen (ran (.))))) \land (a \subseteq ⋃ ran ((.) \circ f) \cap A \land c \subseteq ⋃ ran ((.) \circ f) ∖ A)) \to vol (a) \in ℝ$
340	119	adantl	$⊢ (a \in Clsd (topGen (ran (.))) \land c \in Clsd (topGen (ran (.)))) \to vol (c) = {vol}^{*} (c)$
341	340	ad2antlr	$⊢ (({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \land (a \in Clsd (topGen (ran (.))) \land c \in Clsd (topGen (ran (.))))) \land (a \subseteq ⋃ ran ((.) \circ f) \cap A \land c \subseteq ⋃ ran ((.) \circ f) ∖ A)) \to vol (c) = {vol}^{} (c)$
342	122 16	jctir	$⊢ c \subseteq ⋃ ran ((.) \circ f) ∖ A \to (c \subseteq ⋃ ran ((.) \circ f) \land ⋃ ran ((.) \circ f) \subseteq ℝ)$
343	124	3expa	$⊢ ((c \subseteq ⋃ ran ((.) \circ f) \land ⋃ ran ((.) \circ f) \subseteq ℝ) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{} (c) \in ℝ$
344	342 343	sylan	$⊢ (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{} (c) \in ℝ$
345	344	ancoms	$⊢ ({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \land c \subseteq ⋃ ran ((.) \circ f) ∖ A) \to {vol}^{} (c) \in ℝ$
346	345	ad2ant2rl	$⊢ (({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \land (a \in Clsd (topGen (ran (.))) \land c \in Clsd (topGen (ran (.))))) \land (a \subseteq ⋃ ran ((.) \circ f) \cap A \land c \subseteq ⋃ ran ((.) \circ f) ∖ A)) \to {vol}^{} (c) \in ℝ$
347	341 346	eqeltrd	$⊢ (({vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \land (a \in Clsd (topGen (ran (.))) \land c \in Clsd (topGen (ran (.))))) \land (a \subseteq ⋃ ran ((.) \circ f) \cap A \land c \subseteq ⋃ ran ((.) \circ f) ∖ A)) \to vol (c) \in ℝ$
348		volun	$⊢ ((a \in dom vol \land c \in dom vol \land a \cap c = \emptyset) \land (vol (a) \in ℝ \land vol (c) \in ℝ)) \to vol (a \cup c) = vol (a) + vol (c)$
349	320 322 331 339 347 348	syl32anc	$⊢ (({vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \land (a \in Clsd (topGen (ran (.))) \land c \in Clsd (topGen (ran (.))))) \land (a \subseteq ⋃ ran ((.) \circ f) \cap A \land c \subseteq ⋃ ran ((.) \circ f) ∖ A)) \to vol (a \cup c) = vol (a) + vol (c)$
350		unmbl	$⊢ (a \in dom vol \land c \in dom vol) \to a \cup c \in dom vol$
351	59 117 350	syl2an	$⊢ (a \in Clsd (topGen (ran (.))) \land c \in Clsd (topGen (ran (.)))) \to a \cup c \in dom vol$
352		mblvol	$⊢ a \cup c \in dom vol \to vol (a \cup c) = {vol}^{*} (a \cup c)$
353	351 352	syl	$⊢ (a \in Clsd (topGen (ran (.))) \land c \in Clsd (topGen (ran (.)))) \to vol (a \cup c) = {vol}^{*} (a \cup c)$
354	353	ad2antlr	$⊢ (({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \land (a \in Clsd (topGen (ran (.))) \land c \in Clsd (topGen (ran (.))))) \land (a \subseteq ⋃ ran ((.) \circ f) \cap A \land c \subseteq ⋃ ran ((.) \circ f) ∖ A)) \to vol (a \cup c) = {vol}^{} (a \cup c)$
355	349 354	eqtr3d	$⊢ (({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \land (a \in Clsd (topGen (ran (.))) \land c \in Clsd (topGen (ran (.))))) \land (a \subseteq ⋃ ran ((.) \circ f) \cap A \land c \subseteq ⋃ ran ((.) \circ f) ∖ A)) \to vol (a) + vol (c) = {vol}^{} (a \cup c)$
356	318 355	sylan9eqr	$⊢ ((({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \land (a \in Clsd (topGen (ran (.))) \land c \in Clsd (topGen (ran (.))))) \land (a \subseteq ⋃ ran ((.) \circ f) \cap A \land c \subseteq ⋃ ran ((.) \circ f) ∖ A)) \land (u = vol (a) \land v = vol (c))) \to u + v = {vol}^{} (a \cup c)$
357		eqtr	$⊢ (y = u + v \land u + v = {vol}^{} (a \cup c)) \to y = {vol}^{} (a \cup c)$
358	357	ancoms	$⊢ (u + v = {vol}^{} (a \cup c) \land y = u + v) \to y = {vol}^{} (a \cup c)$
359	356 358	sylan	$⊢ (((({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \land (a \in Clsd (topGen (ran (.))) \land c \in Clsd (topGen (ran (.))))) \land (a \subseteq ⋃ ran ((.) \circ f) \cap A \land c \subseteq ⋃ ran ((.) \circ f) ∖ A)) \land (u = vol (a) \land v = vol (c))) \land y = u + v) \to y = {vol}^{} (a \cup c)$
360	66 122	anim12i	$⊢ (a \subseteq ⋃ ran ((.) \circ f) \cap A \land c \subseteq ⋃ ran ((.) \circ f) ∖ A) \to (a \subseteq ⋃ ran ((.) \circ f) \land c \subseteq ⋃ ran ((.) \circ f))$
361		unss	$⊢ (a \subseteq ⋃ ran ((.) \circ f) \land c \subseteq ⋃ ran ((.) \circ f)) \leftrightarrow a \cup c \subseteq ⋃ ran ((.) \circ f)$
362	360 361	sylib	$⊢ (a \subseteq ⋃ ran ((.) \circ f) \cap A \land c \subseteq ⋃ ran ((.) \circ f) ∖ A) \to a \cup c \subseteq ⋃ ran ((.) \circ f)$
363		ovolss	$⊢ (a \cup c \subseteq ⋃ ran ((.) \circ f) \land ⋃ ran ((.) \circ f) \subseteq ℝ) \to {vol}^{} (a \cup c) \leq {vol}^{} (⋃ ran ((.) \circ f))$
364	362 16 363	sylancl	$⊢ (a \subseteq ⋃ ran ((.) \circ f) \cap A \land c \subseteq ⋃ ran ((.) \circ f) ∖ A) \to {vol}^{} (a \cup c) \leq {vol}^{} (⋃ ran ((.) \circ f))$
365	364	ad3antlr	$⊢ (((({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \land (a \in Clsd (topGen (ran (.))) \land c \in Clsd (topGen (ran (.))))) \land (a \subseteq ⋃ ran ((.) \circ f) \cap A \land c \subseteq ⋃ ran ((.) \circ f) ∖ A)) \land (u = vol (a) \land v = vol (c))) \land y = u + v) \to {vol}^{} (a \cup c) \leq {vol}^{*} (⋃ ran ((.) \circ f))$
366	359 365	eqbrtrd	$⊢ (((({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \land (a \in Clsd (topGen (ran (.))) \land c \in Clsd (topGen (ran (.))))) \land (a \subseteq ⋃ ran ((.) \circ f) \cap A \land c \subseteq ⋃ ran ((.) \circ f) ∖ A)) \land (u = vol (a) \land v = vol (c))) \land y = u + v) \to y \leq {vol}^{} (⋃ ran ((.) \circ f))$
367	366	ex	$⊢ ((({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \land (a \in Clsd (topGen (ran (.))) \land c \in Clsd (topGen (ran (.))))) \land (a \subseteq ⋃ ran ((.) \circ f) \cap A \land c \subseteq ⋃ ran ((.) \circ f) ∖ A)) \land (u = vol (a) \land v = vol (c))) \to (y = u + v \to y \leq {vol}^{} (⋃ ran ((.) \circ f)))$
368	367	expl	$⊢ ({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \land (a \in Clsd (topGen (ran (.))) \land c \in Clsd (topGen (ran (.))))) \to (((a \subseteq ⋃ ran ((.) \circ f) \cap A \land c \subseteq ⋃ ran ((.) \circ f) ∖ A) \land (u = vol (a) \land v = vol (c))) \to (y = u + v \to y \leq {vol}^{} (⋃ ran ((.) \circ f))))$
369	317 368	syl5bir	$⊢ ({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \land (a \in Clsd (topGen (ran (.))) \land c \in Clsd (topGen (ran (.))))) \to (((a \subseteq ⋃ ran ((.) \circ f) \cap A \land u = vol (a)) \land (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land v = vol (c))) \to (y = u + v \to y \leq {vol}^{} (⋃ ran ((.) \circ f))))$
370	369	rexlimdvva	$⊢ {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \to (\exists a \in Clsd (topGen (ran (.))) \exists c \in Clsd (topGen (ran (.))) ((a \subseteq ⋃ ran ((.) \circ f) \cap A \land u = vol (a)) \land (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land v = vol (c))) \to (y = u + v \to y \leq {vol}^{} (⋃ ran ((.) \circ f))))$
371	316 370	syl5bir	$⊢ {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \to ((u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \land v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\}) \to (y = u + v \to y \leq {vol}^{} (⋃ ran ((.) \circ f))))$
372	371	rexlimdvv	$⊢ {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \to (\exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} y = u + v \to y \leq {vol}^{} (⋃ ran ((.) \circ f)))$
373	372	alrimiv	$⊢ {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \to \forall y (\exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} y = u + v \to y \leq {vol}^{} (⋃ ran ((.) \circ f)))$
374		eqeq1	$⊢ t = y \to (t = u + v \leftrightarrow y = u + v)$
375	374	2rexbidv	$⊢ t = y \to (\exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} t = u + v \leftrightarrow \exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} y = u + v)$
376	375	ralab	$⊢ \forall y \in \{t \| \exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} t = u + v\} y \leq {vol}^{} (⋃ ran ((.) \circ f)) \leftrightarrow \forall y (\exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} y = u + v \to y \leq {vol}^{} (⋃ ran ((.) \circ f)))$
377	373 376	sylibr	$⊢ {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \to \forall y \in \{t \| \exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} t = u + v\} y \leq {vol}^{} (⋃ ran ((.) \circ f))$
378		simpr	$⊢ (({vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \land (u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \land v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\})) \land t = u + v) \to t = u + v$
379	74	sselda	$⊢ ({vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \land u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\}) \to u \in ℝ$
380	130	sselda	$⊢ ({vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \land v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\}) \to v \in ℝ$
381		readdcl	$⊢ (u \in ℝ \land v \in ℝ) \to u + v \in ℝ$
382	379 380 381	syl2an	$⊢ (({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \land u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\}) \land ({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \land v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\})) \to u + v \in ℝ$
383	382	anandis	$⊢ ({vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \land (u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \land v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\})) \to u + v \in ℝ$
384	383	adantr	$⊢ (({vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \land (u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \land v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\})) \land t = u + v) \to u + v \in ℝ$
385	378 384	eqeltrd	$⊢ (({vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \land (u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \land v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\})) \land t = u + v) \to t \in ℝ$
386	385	ex	$⊢ ({vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \land (u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \land v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\})) \to (t = u + v \to t \in ℝ)$
387	386	rexlimdvva	$⊢ {vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \to (\exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} t = u + v \to t \in ℝ)$
388	387	abssdv	$⊢ {vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \to \{t \| \exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} t = u + v\} \subseteq ℝ$
389		00id	$⊢ 0 + 0 = 0$
390	389	eqcomi	$⊢ 0 = 0 + 0$
391		rspceov	$⊢ (0 \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \land 0 \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} \land 0 = 0 + 0) \to \exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} 0 = u + v$
392	110 157 390 391	mp3an	$⊢ \exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} 0 = u + v$
393		eqeq1	$⊢ t = 0 \to (t = u + v \leftrightarrow 0 = u + v)$
394	393	2rexbidv	$⊢ t = 0 \to (\exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} t = u + v \leftrightarrow \exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} 0 = u + v)$
395	105 394	spcev	$⊢ \exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} 0 = u + v \to \exists t \exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} t = u + v$
396	392 395	ax-mp	$⊢ \exists t \exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} t = u + v$
397		abn0	$⊢ \{t \| \exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} t = u + v\} \neq \emptyset \leftrightarrow \exists t \exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} t = u + v$
398	396 397	mpbir	$⊢ \{t \| \exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} t = u + v\} \neq \emptyset$
399	398	a1i	$⊢ {vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \to \{t \| \exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} t = u + v\} \neq \emptyset$
400		brralrspcev	$⊢ ({vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \land \forall y \in \{t \| \exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} t = u + v\} y \leq {vol}^{} (⋃ ran ((.) \circ f))) \to \exists x \in ℝ \forall y \in \{t \| \exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} t = u + v\} y \leq x$
401	377 400	mpdan	$⊢ {vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \to \exists x \in ℝ \forall y \in \{t \| \exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} t = u + v\} y \leq x$
402	388 399 401	3jca	$⊢ {vol}^{*} (⋃ ran ((.) \circ f)) \in ℝ \to (\{t \| \exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} t = u + v\} \subseteq ℝ \land \{t \| \exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} t = u + v\} \neq \emptyset \land \exists x \in ℝ \forall y \in \{t \| \exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} t = u + v\} y \leq x)$
403		suprleub	$⊢ ((\{t \| \exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} t = u + v\} \subseteq ℝ \land \{t \| \exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} t = u + v\} \neq \emptyset \land \exists x \in ℝ \forall y \in \{t \| \exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} t = u + v\} y \leq x) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to (sup (\{t \| \exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} t = u + v\} ℝ <) \leq {vol}^{} (⋃ ran ((.) \circ f)) \leftrightarrow \forall y \in \{t \| \exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} t = u + v\} y \leq {vol}^{*} (⋃ ran ((.) \circ f)))$
404	402 403	mpancom	$⊢ {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \to (sup (\{t \| \exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} t = u + v\} ℝ <) \leq {vol}^{} (⋃ ran ((.) \circ f)) \leftrightarrow \forall y \in \{t \| \exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} t = u + v\} y \leq {vol}^{*} (⋃ ran ((.) \circ f)))$
405	377 404	mpbird	$⊢ {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \to sup (\{t \| \exists u \in \{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} \exists v \in \{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} t = u + v\} ℝ <) \leq {vol}^{} (⋃ ran ((.) \circ f))$
406	303 405	eqbrtrd	$⊢ {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ \to sup (\{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} ℝ <) + sup (\{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} ℝ <) \leq {vol}^{} (⋃ ran ((.) \circ f))$
407	406	adantl	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land (w \subseteq ℝ \land {vol}^{} (w) \in ℝ)) \land w \subseteq ⋃ ran ((.) \circ f)) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to sup (\{z \| \exists a \in Clsd (topGen (ran (.))) (a \subseteq ⋃ ran ((.) \circ f) \cap A \land z = vol (a))\} ℝ <) + sup (\{z \| \exists c \in Clsd (topGen (ran (.))) (c \subseteq ⋃ ran ((.) \circ f) ∖ A \land z = vol (c))\} ℝ <) \leq {vol}^{*} (⋃ ran ((.) \circ f))$
408	45 163 164 297 407	letrd	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land (w \subseteq ℝ \land {vol}^{} (w) \in ℝ)) \land w \subseteq ⋃ ran ((.) \circ f)) \land {vol}^{} (⋃ ran ((.) \circ f)) \in ℝ) \to {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \leq {vol}^{*} (⋃ ran ((.) \circ f))$
409	44 408	sylan2	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land (w \subseteq ℝ \land {vol}^{} (w) \in ℝ)) \land w \subseteq ⋃ ran ((.) \circ f)) \land {vol}^{} (⋃ ran ((.) \circ f)) \neq +∞) \to {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \leq {vol}^{*} (⋃ ran ((.) \circ f))$
410	33 409	pm2.61dane	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land (w \subseteq ℝ \land {vol}^{} (w) \in ℝ)) \land w \subseteq ⋃ ran ((.) \circ f)) \to {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \leq {vol}^{} (⋃ ran ((.) \circ f))$
411	410	adantlr	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land (w \subseteq ℝ \land {vol}^{} (w) \in ℝ)) \land f : ℕ ⟶ \leq \cap ℝ^{2}) \land w \subseteq ⋃ ran ((.) \circ f)) \to {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \leq {vol}^{} (⋃ ran ((.) \circ f))$
412		ssid	$⊢ ⋃ ran ((.) \circ f) \subseteq ⋃ ran ((.) \circ f)$
413	20	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)) ℝ^{} <)$
414	412 413	mpan2	$⊢ f : ℕ ⟶ \leq \cap ℝ^{2} \to {vol}^{} (⋃ ran ((.) \circ f)) \leq sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <)$
415	414	ad2antlr	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land (w \subseteq ℝ \land {vol}^{} (w) \in ℝ)) \land f : ℕ ⟶ \leq \cap ℝ^{2}) \land w \subseteq ⋃ ran ((.) \circ f)) \to {vol}^{} (⋃ ran ((.) \circ f)) \leq sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <)$
416	12 18 27 411 415	xrletrd	$⊢ (((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land (w \subseteq ℝ \land {vol}^{} (w) \in ℝ)) \land f : ℕ ⟶ \leq \cap ℝ^{2}) \land w \subseteq ⋃ ran ((.) \circ f)) \to {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \leq sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <)$
417	416	adantr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land (w \subseteq ℝ \land {vol}^{} (w) \in ℝ)) \land f : ℕ ⟶ \leq \cap ℝ^{2}) \land w \subseteq ⋃ ran ((.) \circ f)) \land u = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <)) \to {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \leq sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <)$
418		simpr	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land (w \subseteq ℝ \land {vol}^{} (w) \in ℝ)) \land f : ℕ ⟶ \leq \cap ℝ^{2}) \land w \subseteq ⋃ ran ((.) \circ f)) \land u = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <)) \to u = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <)$
419	417 418	breqtrrd	$⊢ ((((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land (w \subseteq ℝ \land {vol}^{} (w) \in ℝ)) \land f : ℕ ⟶ \leq \cap ℝ^{2}) \land w \subseteq ⋃ ran ((.) \circ f)) \land u = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <)) \to {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \leq u$
420	419	expl	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land (w \subseteq ℝ \land {vol}^{} (w) \in ℝ)) \land f : ℕ ⟶ \leq \cap ℝ^{2}) \to ((w \subseteq ⋃ ran ((.) \circ f) \land u = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <)) \to {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \leq u)$
421	3 420	sylan2	$⊢ ((((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land (w \subseteq ℝ \land {vol}^{} (w) \in ℝ)) \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \to ((w \subseteq ⋃ ran ((.) \circ f) \land u = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <)) \to {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \leq u)$
422	421	rexlimdva	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land (w \subseteq ℝ \land {vol}^{} (w) \in ℝ)) \to (\exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (w \subseteq ⋃ ran ((.) \circ f) \land u = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <)) \to {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \leq u)$
423	422	ralrimivw	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land (w \subseteq ℝ \land {vol}^{} (w) \in ℝ)) \to \forall u \in ℝ^{} (\exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (w \subseteq ⋃ ran ((.) \circ f) \land u = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <)) \to {vol}^{} (w \cap A) + {vol}^{*} (w ∖ A) \leq u)$
424		eqeq1	$⊢ v = u \to (v = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leftrightarrow u = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))$
425	424	anbi2d	$⊢ v = u \to ((w \subseteq ⋃ ran ((.) \circ f) \land v = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <)) \leftrightarrow (w \subseteq ⋃ ran ((.) \circ f) \land u = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <)))$
426	425	rexbidv	$⊢ v = u \to (\exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (w \subseteq ⋃ ran ((.) \circ f) \land v = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <)) \leftrightarrow \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (w \subseteq ⋃ ran ((.) \circ f) \land u = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <)))$
427	426	ralrab	$⊢ \forall u \in \{v \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (w \subseteq ⋃ ran ((.) \circ f) \land v = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \leq u \leftrightarrow \forall u \in ℝ^{} (\exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (w \subseteq ⋃ ran ((.) \circ f) \land u = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <)) \to {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \leq u)$
428	423 427	sylibr	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land (w \subseteq ℝ \land {vol}^{} (w) \in ℝ)) \to \forall u \in \{v \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (w \subseteq ⋃ ran ((.) \circ f) \land v = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} {vol}^{} (w \cap A) + {vol}^{*} (w ∖ A) \leq u$
429		ssrab2	$⊢ \{v \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (w \subseteq ⋃ ran ((.) \circ f) \land v = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} \subseteq ℝ^{*}$
430	11	adantl	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land (w \subseteq ℝ \land {vol}^{} (w) \in ℝ)) \to {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \in ℝ^{}$
431		infxrgelb	$⊢ (\{v \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (w \subseteq ⋃ ran ((.) \circ f) \land v = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} \subseteq ℝ^{} \land {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \in ℝ^{}) \to ({vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \leq sup (\{v \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (w \subseteq ⋃ ran ((.) \circ f) \land v = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} ℝ^{} <) \leftrightarrow \forall u \in \{v \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (w \subseteq ⋃ ran ((.) \circ f) \land v = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} {vol}^{} (w \cap A) + {vol}^{*} (w ∖ A) \leq u)$
432	429 430 431	sylancr	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land (w \subseteq ℝ \land {vol}^{} (w) \in ℝ)) \to ({vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \leq sup (\{v \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (w \subseteq ⋃ ran ((.) \circ f) \land v = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} ℝ^{} <) \leftrightarrow \forall u \in \{v \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (w \subseteq ⋃ ran ((.) \circ f) \land v = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \leq u)$
433	428 432	mpbird	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land (w \subseteq ℝ \land {vol}^{} (w) \in ℝ)) \to {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \leq sup (\{v \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (w \subseteq ⋃ ran ((.) \circ f) \land v = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} ℝ^{} <)$
434		eqid	$⊢ \{v \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (w \subseteq ⋃ ran ((.) \circ f) \land v = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} = \{v \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (w \subseteq ⋃ ran ((.) \circ f) \land v = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\}$
435	434	ovolval	$⊢ w \subseteq ℝ \to {vol}^{} (w) = sup (\{v \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (w \subseteq ⋃ ran ((.) \circ f) \land v = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} ℝ^{} <)$
436	435	ad2antrl	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land (w \subseteq ℝ \land {vol}^{} (w) \in ℝ)) \to {vol}^{} (w) = sup (\{v \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (w \subseteq ⋃ ran ((.) \circ f) \land v = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} ℝ^{*} <)$
437	433 436	breqtrrd	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land (w \subseteq ℝ \land {vol}^{} (w) \in ℝ)) \to {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \leq {vol}^{} (w)$
438	437	expr	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land w \subseteq ℝ) \to ({vol}^{} (w) \in ℝ \to {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \leq {vol}^{} (w))$
439	2 438	sylan2	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \land w \in 𝒫 ℝ) \to ({vol}^{} (w) \in ℝ \to {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \leq {vol}^{} (w))$
440	439	ralrimiva	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \to \forall w \in 𝒫 ℝ ({vol}^{} (w) \in ℝ \to {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \leq {vol}^{} (w))$
441		ismbl2	$⊢ A \in dom vol \leftrightarrow (A \subseteq ℝ \land \forall w \in 𝒫 ℝ ({vol}^{} (w) \in ℝ \to {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \leq {vol}^{} (w)))$
442	441	baibr	$⊢ A \subseteq ℝ \to (\forall w \in 𝒫 ℝ ({vol}^{} (w) \in ℝ \to {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \leq {vol}^{} (w)) \leftrightarrow A \in dom vol)$
443	442	ad2antrr	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \to (\forall w \in 𝒫 ℝ ({vol}^{} (w) \in ℝ \to {vol}^{} (w \cap A) + {vol}^{} (w ∖ A) \leq {vol}^{} (w)) \leftrightarrow A \in dom vol)$
444	440 443	mpbid	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <)) \to A \in dom vol$
445	1 444	impbida	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \to (A \in dom vol \leftrightarrow {vol}^{} (A) = sup (\{y \| \exists b \in Clsd (topGen (ran (.))) (b \subseteq A \land y = vol (b))\} ℝ <))$

Metamath Proof Explorer

Theorem ismblfin

Proof