Theorem mblfinlem4

Description: Backward direction of ismblfin . (Contributed by Brendan Leahy, 28-Mar-2018) (Revised by Brendan Leahy, 13-Jul-2018)

	Ref	Expression
Assertion	mblfinlem4	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) ∧ 𝐴 ∈ dom vol ) → ( vol* ‘ 𝐴 ) = sup ( { 𝑦 ∣ ∃ 𝑏 ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) ( 𝑏 ⊆ 𝐴 ∧ 𝑦 = ( vol ‘ 𝑏 ) ) } , ℝ , < ) )

Proof

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