Theorem 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	⊢ ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) → ( 𝐴 ∈ dom vol ↔ ( vol* ‘ 𝐴 ) = sup ( { 𝑦 ∣ ∃ 𝑏 ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) ( 𝑏 ⊆ 𝐴 ∧ 𝑦 = ( vol ‘ 𝑏 ) ) } , ℝ , < ) ) )

Proof

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