Metamath Proof Explorer

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 ⊢A⊆ℝ∧vol*⁡A∈ℝ∧A∈dom⁡vol→vol*⁡A=supy|∃b∈Clsd⁡topGen⁡ran⁡.b⊆A∧y=vol⁡bℝ<

Proof

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