Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ismblfin Structured version   Visualization version   GIF version
Theorem ismblfin 38559
Description: Measurability in terms of inner and outer measure. Proposition 7 of [Viaclovsky8] p. 3. (Contributed by Brendan Leahy, 4-Mar-2018.) (Revised by Brendan Leahy, 28-Mar-2018.)
Assertion
Ref Expression
ismblfin ((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) → (𝐴 ∈ dom vol ↔ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )))
Distinct variable group:   𝑦,𝑏,𝐴
Proof of Theorem ismblfin
Dummy variables 𝑎 𝑐 𝑓 𝑡 𝑢 𝑣 𝑤 𝑥 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mblfinlem4 38558 . 2 (((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ 𝐴 ∈ dom vol) → (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < ))
2 elpwi 4564 . . . . 5 (𝑤 ∈ 𝒫 ℝ → 𝑤 ⊆ ℝ)
3 elmapi 8862 . . . . . . . . . . . 12 (𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ) → 𝑓:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
4 inss1 4182 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∩ 𝐴) ⊆ 𝑤
5 ovolsscl 25800 . . . . . . . . . . . . . . . . . . . 20 (((𝑤 ∩ 𝐴) ⊆ 𝑤 ∧ 𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) → (vol*‘(𝑤 ∩ 𝐴)) ∈ ℝ)
64, 5mp3an1 1477 . . . . . . . . . . . . . . . . . . 19 ((𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) → (vol*‘(𝑤 ∩ 𝐴)) ∈ ℝ)
7 difss 4083 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∖ 𝐴) ⊆ 𝑤
8 ovolsscl 25800 . . . . . . . . . . . . . . . . . . . 20 (((𝑤 ∖ 𝐴) ⊆ 𝑤 ∧ 𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) → (vol*‘(𝑤 ∖ 𝐴)) ∈ ℝ)
97, 8mp3an1 1477 . . . . . . . . . . . . . . . . . . 19 ((𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) → (vol*‘(𝑤 ∖ 𝐴)) ∈ ℝ)
106, 9readdcld 11331 . . . . . . . . . . . . . . . . . 18 ((𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ∈ ℝ)
1110rexrd 11352 . . . . . . . . . . . . . . . . 17 ((𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ∈ ℝ*)
1211ad3antlr 744 . . . . . . . . . . . . . . . 16 ((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑓:ℕ⟶( ≤ ∩ (ℝ × ℝ))) ∧ 𝑤 ⊆ ∪ ran ((,) ∘ 𝑓)) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ∈ ℝ*)
13 rncoss 5959 . . . . . . . . . . . . . . . . . . 19 ran ((,) ∘ 𝑓) ⊆ ran (,)
1413unissi 4876 . . . . . . . . . . . . . . . . . 18 ∪ ran ((,) ∘ 𝑓) ⊆ ∪ ran (,)
15 unirnioo 13573 . . . . . . . . . . . . . . . . . 18 ℝ = ∪ ran (,)
1614, 15sseqtrri 3980 . . . . . . . . . . . . . . . . 17 ∪ ran ((,) ∘ 𝑓) ⊆ ℝ
17 ovolcl 25792 . . . . . . . . . . . . . . . . 17 (∪ ran ((,) ∘ 𝑓) ⊆ ℝ → (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ*)
1816, 17mp1i 14 . . . . . . . . . . . . . . . 16 ((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑓:ℕ⟶( ≤ ∩ (ℝ × ℝ))) ∧ 𝑤 ⊆ ∪ ran ((,) ∘ 𝑓)) → (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ*)
19 eqid 2761 . . . . . . . . . . . . . . . . . . 19 ((abs ∘ − ) ∘ 𝑓) = ((abs ∘ − ) ∘ 𝑓)
20 eqid 2761 . . . . . . . . . . . . . . . . . . 19 seq1( + , ((abs ∘ − ) ∘ 𝑓)) = seq1( + , ((abs ∘ − ) ∘ 𝑓))
2119, 20ovolsf 25786 . . . . . . . . . . . . . . . . . 18 (𝑓:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → seq1( + , ((abs ∘ − ) ∘ 𝑓)):ℕ⟶(0[,)+∞))
22 frn 6715 . . . . . . . . . . . . . . . . . . 19 (seq1( + , ((abs ∘ − ) ∘ 𝑓)):ℕ⟶(0[,)+∞) → ran seq1( + , ((abs ∘ − ) ∘ 𝑓)) ⊆ (0[,)+∞))
23 icossxr 13556 . . . . . . . . . . . . . . . . . . 19 (0[,)+∞) ⊆ ℝ*
2422, 23sstrdi 3943 . . . . . . . . . . . . . . . . . 18 (seq1( + , ((abs ∘ − ) ∘ 𝑓)):ℕ⟶(0[,)+∞) → ran seq1( + , ((abs ∘ − ) ∘ 𝑓)) ⊆ ℝ*)
25 supxrcl 13438 . . . . . . . . . . . . . . . . . 18 (ran seq1( + , ((abs ∘ − ) ∘ 𝑓)) ⊆ ℝ* → sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ∈ ℝ*)
2621, 24, 253syl 19 . . . . . . . . . . . . . . . . 17 (𝑓:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ∈ ℝ*)
2726ad2antlr 740 . . . . . . . . . . . . . . . 16 ((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑓:ℕ⟶( ≤ ∩ (ℝ × ℝ))) ∧ 𝑤 ⊆ ∪ ran ((,) ∘ 𝑓)) → sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ∈ ℝ*)
28 pnfge 13252 . . . . . . . . . . . . . . . . . . . . . 22 (((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ∈ ℝ* → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ +∞)
2911, 28syl 18 . . . . . . . . . . . . . . . . . . . . 21 ((𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ +∞)
3029ad2antrr 739 . . . . . . . . . . . . . . . . . . . 20 ((((𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) ∧ 𝑤 ⊆ ∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) = +∞) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ +∞)
31 simpr 490 . . . . . . . . . . . . . . . . . . . 20 ((((𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) ∧ 𝑤 ⊆ ∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) = +∞) → (vol*‘∪ ran ((,) ∘ 𝑓)) = +∞)
3230, 31breqtrrd 5133 . . . . . . . . . . . . . . . . . . 19 ((((𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) ∧ 𝑤 ⊆ ∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) = +∞) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))
3332adantlll 731 . . . . . . . . . . . . . . . . . 18 ((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑤 ⊆ ∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) = +∞) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))
3416, 17ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ*
35 nltpnft 13287 . . . . . . . . . . . . . . . . . . . . . 22 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ* → ((vol*‘∪ ran ((,) ∘ 𝑓)) = +∞ ↔ ¬ (vol*‘∪ ran ((,) ∘ 𝑓)) < +∞))
3634, 35ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 ((vol*‘∪ ran ((,) ∘ 𝑓)) = +∞ ↔ ¬ (vol*‘∪ ran ((,) ∘ 𝑓)) < +∞)
3736necon2abii 3006 . . . . . . . . . . . . . . . . . . . 20 ((vol*‘∪ ran ((,) ∘ 𝑓)) < +∞ ↔ (vol*‘∪ ran ((,) ∘ 𝑓)) ≠ +∞)
38 ovolge0 25795 . . . . . . . . . . . . . . . . . . . . . 22 (∪ ran ((,) ∘ 𝑓) ⊆ ℝ → 0 ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))
3916, 38ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 0 ≤ (vol*‘∪ ran ((,) ∘ 𝑓))
40 0re 11303 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ ℝ
41 xrre3 13294 . . . . . . . . . . . . . . . . . . . . . 22 ((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ* ∧ 0 ∈ ℝ) ∧ (0 ≤ (vol*‘∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) < +∞)) → (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ)
4234, 40, 41mpanl12 715 . . . . . . . . . . . . . . . . . . . . 21 ((0 ≤ (vol*‘∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) < +∞) → (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ)
4339, 42mpan 703 . . . . . . . . . . . . . . . . . . . 20 ((vol*‘∪ ran ((,) ∘ 𝑓)) < +∞ → (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ)
4437, 43sylbir 238 . . . . . . . . . . . . . . . . . . 19 ((vol*‘∪ ran ((,) ∘ 𝑓)) ≠ +∞ → (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ)
4510ad3antlr 744 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑤 ⊆ ∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ∈ ℝ)
46 simpr 490 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)) → 𝑧 = (vol‘𝑎))
47 eleq1w 2844 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑏 = 𝑎 → (𝑏 ∈ dom vol ↔ 𝑎 ∈ dom vol))
48 uniretop 25074 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ℝ = ∪ (topGen‘ran (,))
4948cldss 23340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑏 ∈ (Clsd‘(topGen‘ran (,))) → 𝑏 ⊆ ℝ)
50 dfss4 4215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑏 ⊆ ℝ ↔ (ℝ ∖ (ℝ ∖ 𝑏)) = 𝑏)
5149, 50sylib 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑏 ∈ (Clsd‘(topGen‘ran (,))) → (ℝ ∖ (ℝ ∖ 𝑏)) = 𝑏)
52 rembl 25854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ℝ ∈ dom vol
5348cldopn 23342 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑏 ∈ (Clsd‘(topGen‘ran (,))) → (ℝ ∖ 𝑏) ∈ (topGen‘ran (,)))
54 opnmbl 25916 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((ℝ ∖ 𝑏) ∈ (topGen‘ran (,)) → (ℝ ∖ 𝑏) ∈ dom vol)
5553, 54syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑏 ∈ (Clsd‘(topGen‘ran (,))) → (ℝ ∖ 𝑏) ∈ dom vol)
56 difmbl 25857 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((ℝ ∈ dom vol ∧ (ℝ ∖ 𝑏) ∈ dom vol) → (ℝ ∖ (ℝ ∖ 𝑏)) ∈ dom vol)
5752, 55, 56sylancr 599 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑏 ∈ (Clsd‘(topGen‘ran (,))) → (ℝ ∖ (ℝ ∖ 𝑏)) ∈ dom vol)
5851, 57eqeltrrd 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑏 ∈ (Clsd‘(topGen‘ran (,))) → 𝑏 ∈ dom vol)
5947, 58vtoclga 3537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎 ∈ (Clsd‘(topGen‘ran (,))) → 𝑎 ∈ dom vol)
60 mblvol 25844 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎 ∈ dom vol → (vol‘𝑎) = (vol*‘𝑎))
6159, 60syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 ∈ (Clsd‘(topGen‘ran (,))) → (vol‘𝑎) = (vol*‘𝑎))
6246, 61sylan9eqr 2818 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))) → 𝑧 = (vol*‘𝑎))
6362adantl 487 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)))) → 𝑧 = (vol*‘𝑎))
64 inss1 4182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ⊆ ∪ ran ((,) ∘ 𝑓)
65 sstr 3939 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ⊆ ∪ ran ((,) ∘ 𝑓)) → 𝑎 ⊆ ∪ ran ((,) ∘ 𝑓))
6664, 65mpan2 704 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) → 𝑎 ⊆ ∪ ran ((,) ∘ 𝑓))
6766ad2antrl 741 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))) → 𝑎 ⊆ ∪ ran ((,) ∘ 𝑓))
68 ovolsscl 25800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑎 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ ∪ ran ((,) ∘ 𝑓) ⊆ ℝ ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘𝑎) ∈ ℝ)
6916, 68mp3an2 1478 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑎 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘𝑎) ∈ ℝ)
7069ancoms 464 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ 𝑎 ⊆ ∪ ran ((,) ∘ 𝑓)) → (vol*‘𝑎) ∈ ℝ)
7167, 70sylan2 605 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)))) → (vol*‘𝑎) ∈ ℝ)
7263, 71eqeltrd 2861 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)))) → 𝑧 ∈ ℝ)
7372rexlimdvaa 3165 . . . . . . . . . . . . . . . . . . . . . . . 24 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → (∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)) → 𝑧 ∈ ℝ))
7473abssdv 4015 . . . . . . . . . . . . . . . . . . . . . . 23 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ⊆ ℝ)
75 eqeq1 2765 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 = 𝑦 → (𝑧 = (vol‘𝑎) ↔ 𝑦 = (vol‘𝑎)))
7675anbi2d 642 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = 𝑦 → ((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)) ↔ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑦 = (vol‘𝑎))))
7776rexbidv 3187 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 = 𝑦 → (∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)) ↔ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑦 = (vol‘𝑎))))
7877ralab 3651 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑦 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓)) ↔ ∀𝑦(∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑦 = (vol‘𝑎)) → 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓))))
79 simpr 490 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑦 = (vol‘𝑎)) → 𝑦 = (vol‘𝑎))
8079, 61sylan9eqr 2818 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑦 = (vol‘𝑎))) → 𝑦 = (vol*‘𝑎))
81 ovolss 25799 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑎 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ ∪ ran ((,) ∘ 𝑓) ⊆ ℝ) → (vol*‘𝑎) ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))
8266, 16, 81sylancl 598 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) → (vol*‘𝑎) ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))
8382ad2antrl 741 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑦 = (vol‘𝑎))) → (vol*‘𝑎) ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))
8480, 83eqbrtrd 5127 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑦 = (vol‘𝑎))) → 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))
8584rexlimiva 3156 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑦 = (vol‘𝑎)) → 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))
8678, 85mpgbir 1832 . . . . . . . . . . . . . . . . . . . . . . . 24 ∀𝑦 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓))
87 brralrspcev 5165 . . . . . . . . . . . . . . . . . . . . . . . 24 (((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ ∀𝑦 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓))) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}𝑦 ≤ 𝑥)
8886, 87mpan2 704 . . . . . . . . . . . . . . . . . . . . . . 23 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}𝑦 ≤ 𝑥)
89 retop 25073 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (topGen‘ran (,)) ∈ Top
90 0cld 23349 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((topGen‘ran (,)) ∈ Top → ∅ ∈ (Clsd‘(topGen‘ran (,))))
9189, 90ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ∅ ∈ (Clsd‘(topGen‘ran (,)))
92 0ss 4350 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ∅ ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴)
93 0mbl 25853 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ∅ ∈ dom vol
94 mblvol 25844 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
9593, 94ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (vol‘∅) = (vol*‘∅)
96 ovol0 25807 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (vol*‘∅) = 0
9795, 96eqtr2i 2785 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 0 = (vol‘∅)
9892, 97pm3.2i 476 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∅ ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 0 = (vol‘∅))
99 sseq1 3956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎 = ∅ → (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ↔ ∅ ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴)))
100 fveq2 6883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 = ∅ → (vol‘𝑎) = (vol‘∅))
101100eqeq2d 2772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎 = ∅ → (0 = (vol‘𝑎) ↔ 0 = (vol‘∅)))
10299, 101anbi12d 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 = ∅ → ((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 0 = (vol‘𝑎)) ↔ (∅ ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 0 = (vol‘∅))))
103102rspcev 3577 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((∅ ∈ (Clsd‘(topGen‘ran (,))) ∧ (∅ ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 0 = (vol‘∅))) → ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 0 = (vol‘𝑎)))
10491, 98, 103mp2an 705 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 0 = (vol‘𝑎))
105 c0ex 11293 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 0 ∈ V
106 eqeq1 2765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 = 0 → (𝑧 = (vol‘𝑎) ↔ 0 = (vol‘𝑎)))
107106anbi2d 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 = 0 → ((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)) ↔ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 0 = (vol‘𝑎))))
108107rexbidv 3187 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = 0 → (∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)) ↔ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 0 = (vol‘𝑎))))
109105, 108elab 3633 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ↔ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 0 = (vol‘𝑎)))
110104, 109mpbir 234 . . . . . . . . . . . . . . . . . . . . . . . . 25 0 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}
111110ne0ii 4290 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ≠ ∅
112 suprcl 12270 . . . . . . . . . . . . . . . . . . . . . . . 24 (({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ⊆ ℝ ∧ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}𝑦 ≤ 𝑥) → sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) ∈ ℝ)
113111, 112mp3an2 1478 . . . . . . . . . . . . . . . . . . . . . . 23 (({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}𝑦 ≤ 𝑥) → sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) ∈ ℝ)
11474, 88, 113syl2anc 596 . . . . . . . . . . . . . . . . . . . . . 22 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) ∈ ℝ)
115 simpr 490 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐)) → 𝑧 = (vol‘𝑐))
116 eleq1w 2844 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑏 = 𝑐 → (𝑏 ∈ dom vol ↔ 𝑐 ∈ dom vol))
117116, 58vtoclga 3537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ (Clsd‘(topGen‘ran (,))) → 𝑐 ∈ dom vol)
118 mblvol 25844 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ dom vol → (vol‘𝑐) = (vol*‘𝑐))
119117, 118syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 ∈ (Clsd‘(topGen‘ran (,))) → (vol‘𝑐) = (vol*‘𝑐))
120115, 119sylan9eqr 2818 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑐 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))) → 𝑧 = (vol*‘𝑐))
121120adantl 487 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑐 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐)))) → 𝑧 = (vol*‘𝑐))
122 difss2 4085 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) → 𝑐 ⊆ ∪ ran ((,) ∘ 𝑓))
123122ad2antrl 741 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑐 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))) → 𝑐 ⊆ ∪ ran ((,) ∘ 𝑓))
124 ovolsscl 25800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ ∪ ran ((,) ∘ 𝑓) ⊆ ℝ ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘𝑐) ∈ ℝ)
12516, 124mp3an2 1478 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘𝑐) ∈ ℝ)
126125ancoms 464 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ 𝑐 ⊆ ∪ ran ((,) ∘ 𝑓)) → (vol*‘𝑐) ∈ ℝ)
127123, 126sylan2 605 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑐 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐)))) → (vol*‘𝑐) ∈ ℝ)
128121, 127eqeltrd 2861 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑐 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐)))) → 𝑧 ∈ ℝ)
129128rexlimdvaa 3165 . . . . . . . . . . . . . . . . . . . . . . . 24 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → (∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐)) → 𝑧 ∈ ℝ))
130129abssdv 4015 . . . . . . . . . . . . . . . . . . . . . . 23 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))} ⊆ ℝ)
131 eqeq1 2765 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 = 𝑦 → (𝑧 = (vol‘𝑐) ↔ 𝑦 = (vol‘𝑐)))
132131anbi2d 642 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = 𝑦 → ((𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐)) ↔ (𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑦 = (vol‘𝑐))))
133132rexbidv 3187 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 = 𝑦 → (∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐)) ↔ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑦 = (vol‘𝑐))))
134133ralab 3651 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓)) ↔ ∀𝑦(∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑦 = (vol‘𝑐)) → 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓))))
135 simpr 490 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑦 = (vol‘𝑐)) → 𝑦 = (vol‘𝑐))
136135, 119sylan9eqr 2818 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑐 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑦 = (vol‘𝑐))) → 𝑦 = (vol*‘𝑐))
137 ovolss 25799 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ ∪ ran ((,) ∘ 𝑓) ⊆ ℝ) → (vol*‘𝑐) ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))
138122, 16, 137sylancl 598 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) → (vol*‘𝑐) ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))
139138ad2antrl 741 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑐 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑦 = (vol‘𝑐))) → (vol*‘𝑐) ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))
140136, 139eqbrtrd 5127 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑐 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑦 = (vol‘𝑐))) → 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))
141140rexlimiva 3156 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑦 = (vol‘𝑐)) → 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))
142134, 141mpgbir 1832 . . . . . . . . . . . . . . . . . . . . . . . 24 ∀𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓))
143 brralrspcev 5165 . . . . . . . . . . . . . . . . . . . . . . . 24 (((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ ∀𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓))) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦 ≤ 𝑥)
144142, 143mpan2 704 . . . . . . . . . . . . . . . . . . . . . . 23 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦 ≤ 𝑥)
145 0ss 4350 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ∅ ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴)
146145, 97pm3.2i 476 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∅ ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 0 = (vol‘∅))
147 sseq1 3956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = ∅ → (𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ↔ ∅ ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴)))
148 fveq2 6883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 = ∅ → (vol‘𝑐) = (vol‘∅))
149148eqeq2d 2772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = ∅ → (0 = (vol‘𝑐) ↔ 0 = (vol‘∅)))
150147, 149anbi12d 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 = ∅ → ((𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 0 = (vol‘𝑐)) ↔ (∅ ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 0 = (vol‘∅))))
151150rspcev 3577 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((∅ ∈ (Clsd‘(topGen‘ran (,))) ∧ (∅ ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 0 = (vol‘∅))) → ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 0 = (vol‘𝑐)))
15291, 146, 151mp2an 705 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 0 = (vol‘𝑐))
153 eqeq1 2765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 = 0 → (𝑧 = (vol‘𝑐) ↔ 0 = (vol‘𝑐)))
154153anbi2d 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 = 0 → ((𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐)) ↔ (𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 0 = (vol‘𝑐))))
155154rexbidv 3187 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = 0 → (∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐)) ↔ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 0 = (vol‘𝑐))))
156105, 155elab 3633 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))} ↔ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 0 = (vol‘𝑐)))
157152, 156mpbir 234 . . . . . . . . . . . . . . . . . . . . . . . . 25 0 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}
158157ne0ii 4290 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))} ≠ ∅
159 suprcl 12270 . . . . . . . . . . . . . . . . . . . . . . . 24 (({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))} ⊆ ℝ ∧ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦 ≤ 𝑥) → sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < ) ∈ ℝ)
160158, 159mp3an2 1478 . . . . . . . . . . . . . . . . . . . . . . 23 (({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))} ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦 ≤ 𝑥) → sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < ) ∈ ℝ)
161130, 144, 160syl2anc 596 . . . . . . . . . . . . . . . . . . . . . 22 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < ) ∈ ℝ)
162114, 161readdcld 11331 . . . . . . . . . . . . . . . . . . . . 21 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → (sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) + sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < )) ∈ ℝ)
163162adantl 487 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑤 ⊆ ∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) + sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < )) ∈ ℝ)
164 simpr 490 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑤 ⊆ ∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ)
1656ad2antrr 739 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) ∧ 𝑤 ⊆ ∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘(𝑤 ∩ 𝐴)) ∈ ℝ)
1669ad2antrr 739 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) ∧ 𝑤 ⊆ ∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘(𝑤 ∖ 𝐴)) ∈ ℝ)
167 ovolsscl 25800 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ⊆ ∪ ran ((,) ∘ 𝑓) ∧ ∪ ran ((,) ∘ 𝑓) ⊆ ℝ ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘(∪ ran ((,) ∘ 𝑓) ∩ 𝐴)) ∈ ℝ)
16864, 16, 167mp3an12 1480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → (vol*‘(∪ ran ((,) ∘ 𝑓) ∩ 𝐴)) ∈ ℝ)
169168adantl 487 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) ∧ 𝑤 ⊆ ∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘(∪ ran ((,) ∘ 𝑓) ∩ 𝐴)) ∈ ℝ)
170 difss 4083 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ⊆ ∪ ran ((,) ∘ 𝑓)
171 ovolsscl 25800 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ⊆ ∪ ran ((,) ∘ 𝑓) ∧ ∪ ran ((,) ∘ 𝑓) ⊆ ℝ ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) ∈ ℝ)
172170, 16, 171mp3an12 1480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) ∈ ℝ)
173172adantl 487 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) ∧ 𝑤 ⊆ ∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) ∈ ℝ)
174 ssrin 4187 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) → (𝑤 ∩ 𝐴) ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴))
17564, 16sstri 3940 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ⊆ ℝ
176 ovolss 25799 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑤 ∩ 𝐴) ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ⊆ ℝ) → (vol*‘(𝑤 ∩ 𝐴)) ≤ (vol*‘(∪ ran ((,) ∘ 𝑓) ∩ 𝐴)))
177174, 175, 176sylancl 598 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) → (vol*‘(𝑤 ∩ 𝐴)) ≤ (vol*‘(∪ ran ((,) ∘ 𝑓) ∩ 𝐴)))
178177ad2antlr 740 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) ∧ 𝑤 ⊆ ∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘(𝑤 ∩ 𝐴)) ≤ (vol*‘(∪ ran ((,) ∘ 𝑓) ∩ 𝐴)))
179 ssdif 4091 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) → (𝑤 ∖ 𝐴) ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴))
180170, 16sstri 3940 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ⊆ ℝ
181 ovolss 25799 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑤 ∖ 𝐴) ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ⊆ ℝ) → (vol*‘(𝑤 ∖ 𝐴)) ≤ (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴)))
182179, 180, 181sylancl 598 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) → (vol*‘(𝑤 ∖ 𝐴)) ≤ (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴)))
183182ad2antlr 740 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) ∧ 𝑤 ⊆ ∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘(𝑤 ∖ 𝐴)) ≤ (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴)))
184165, 166, 169, 173, 178, 183le2addd 11928 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) ∧ 𝑤 ⊆ ∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ ((vol*‘(∪ ran ((,) ∘ 𝑓) ∩ 𝐴)) + (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴))))
185 dfin4 4224 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) = (∪ ran ((,) ∘ 𝑓) ∖ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴))
186185fveq2i 6886 . . . . . . . . . . . . . . . . . . . . . . . 24 (vol*‘(∪ ran ((,) ∘ 𝑓) ∩ 𝐴)) = (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴)))
187186oveq1i 7428 . . . . . . . . . . . . . . . . . . . . . . 23 ((vol*‘(∪ ran ((,) ∘ 𝑓) ∩ 𝐴)) + (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) = ((vol*‘(∪ ran ((,) ∘ 𝑓) ∖ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) + (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴)))
188184, 187breqtrdi 5146 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) ∧ 𝑤 ⊆ ∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ ((vol*‘(∪ ran ((,) ∘ 𝑓) ∖ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) + (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴))))
189188adantlll 731 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑤 ⊆ ∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ ((vol*‘(∪ ran ((,) ∘ 𝑓) ∖ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) + (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴))))
190 simpll 779 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑤 ⊆ ∪ ran ((,) ∘ 𝑓)) → ((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )))
191185sseq2i 3960 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ↔ 𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴)))
192191anbi1i 636 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)) ↔ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) ∧ 𝑧 = (vol‘𝑎)))
193192rexbii 3110 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)) ↔ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) ∧ 𝑧 = (vol‘𝑎)))
194193abbii 2828 . . . . . . . . . . . . . . . . . . . . . . . . 25 {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} = {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) ∧ 𝑧 = (vol‘𝑎))}
195194supeq1i 9432 . . . . . . . . . . . . . . . . . . . . . . . 24 sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) = sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < )
19616jctl 533 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → (∪ ran ((,) ∘ 𝑓) ⊆ ℝ ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ))
197196adantl 487 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (∪ ran ((,) ∘ 𝑓) ⊆ ℝ ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ))
198172, 180jctil 529 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → ((∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ⊆ ℝ ∧ (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) ∈ ℝ))
199198adantl 487 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → ((∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ⊆ ℝ ∧ (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) ∈ ℝ))
200 ltso 11383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 < Or ℝ
201200a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → < Or ℝ)
202 id 23 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ)
203 vex 3455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑥 ∈ V
204 eqeq1 2765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 = 𝑥 → (𝑧 = (vol‘𝑐) ↔ 𝑥 = (vol‘𝑐)))
205204anbi2d 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 = 𝑥 → ((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐)) ↔ (𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑥 = (vol‘𝑐))))
206205rexbidv 3187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧 = 𝑥 → (∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐)) ↔ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑥 = (vol‘𝑐))))
207203, 206elab 3633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))} ↔ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑥 = (vol‘𝑐)))
20816, 137mpan2 704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) → (vol*‘𝑐) ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))
209208ad2antrl 741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑐 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑥 = (vol‘𝑐))) → (vol*‘𝑐) ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))
21048cldss 23340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑐 ∈ (Clsd‘(topGen‘ran (,))) → 𝑐 ⊆ ℝ)
211 ovolcl 25792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑐 ⊆ ℝ → (vol*‘𝑐) ∈ ℝ*)
212210, 211syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑐 ∈ (Clsd‘(topGen‘ran (,))) → (vol*‘𝑐) ∈ ℝ*)
213 xrlenlt 11367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((vol*‘𝑐) ∈ ℝ* ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ*) → ((vol*‘𝑐) ≤ (vol*‘∪ ran ((,) ∘ 𝑓)) ↔ ¬ (vol*‘∪ ran ((,) ∘ 𝑓)) < (vol*‘𝑐)))
214212, 34, 213sylancl 598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 ∈ (Clsd‘(topGen‘ran (,))) → ((vol*‘𝑐) ≤ (vol*‘∪ ran ((,) ∘ 𝑓)) ↔ ¬ (vol*‘∪ ran ((,) ∘ 𝑓)) < (vol*‘𝑐)))
215214adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑥 = (vol‘𝑐))) → ((vol*‘𝑐) ≤ (vol*‘∪ ran ((,) ∘ 𝑓)) ↔ ¬ (vol*‘∪ ran ((,) ∘ 𝑓)) < (vol*‘𝑐)))
216 id 23 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑥 = (vol‘𝑐) → 𝑥 = (vol‘𝑐))
217216, 119sylan9eqr 2818 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑐 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑥 = (vol‘𝑐)) → 𝑥 = (vol*‘𝑐))
218 breq2 5107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑥 = (vol*‘𝑐) → ((vol*‘∪ ran ((,) ∘ 𝑓)) < 𝑥 ↔ (vol*‘∪ ran ((,) ∘ 𝑓)) < (vol*‘𝑐)))
219218notbid 321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑥 = (vol*‘𝑐) → (¬ (vol*‘∪ ran ((,) ∘ 𝑓)) < 𝑥 ↔ ¬ (vol*‘∪ ran ((,) ∘ 𝑓)) < (vol*‘𝑐)))
220217, 219syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑐 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑥 = (vol‘𝑐)) → (¬ (vol*‘∪ ran ((,) ∘ 𝑓)) < 𝑥 ↔ ¬ (vol*‘∪ ran ((,) ∘ 𝑓)) < (vol*‘𝑐)))
221220adantrl 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑥 = (vol‘𝑐))) → (¬ (vol*‘∪ ran ((,) ∘ 𝑓)) < 𝑥 ↔ ¬ (vol*‘∪ ran ((,) ∘ 𝑓)) < (vol*‘𝑐)))
222215, 221bitr4d 285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑐 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑥 = (vol‘𝑐))) → ((vol*‘𝑐) ≤ (vol*‘∪ ran ((,) ∘ 𝑓)) ↔ ¬ (vol*‘∪ ran ((,) ∘ 𝑓)) < 𝑥))
223209, 222mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑐 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑥 = (vol‘𝑐))) → ¬ (vol*‘∪ ran ((,) ∘ 𝑓)) < 𝑥)
224223rexlimiva 3156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑥 = (vol‘𝑐)) → ¬ (vol*‘∪ ran ((,) ∘ 𝑓)) < 𝑥)
225207, 224sylbi 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))} → ¬ (vol*‘∪ ran ((,) ∘ 𝑓)) < 𝑥)
226225adantl 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ 𝑥 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))}) → ¬ (vol*‘∪ ran ((,) ∘ 𝑓)) < 𝑥)
227 retopbas 25072 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ran (,) ∈ TopBases
228 bastg 23277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (ran (,) ∈ TopBases → ran (,) ⊆ (topGen‘ran (,)))
229227, 228ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ran (,) ⊆ (topGen‘ran (,))
23013, 229sstri 3940 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ran ((,) ∘ 𝑓) ⊆ (topGen‘ran (,))
231 uniopn 23208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((topGen‘ran (,)) ∈ Top ∧ ran ((,) ∘ 𝑓) ⊆ (topGen‘ran (,))) → ∪ ran ((,) ∘ 𝑓) ∈ (topGen‘ran (,)))
23289, 230, 231mp2an 705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ∪ ran ((,) ∘ 𝑓) ∈ (topGen‘ran (,))
233 mblfinlem2 38556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((∪ ran ((,) ∘ 𝑓) ∈ (topGen‘ran (,)) ∧ 𝑥 ∈ ℝ ∧ 𝑥 < (vol*‘∪ ran ((,) ∘ 𝑓))) → ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑥 < (vol*‘𝑐)))
234232, 233mp3an1 1477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑥 ∈ ℝ ∧ 𝑥 < (vol*‘∪ ran ((,) ∘ 𝑓))) → ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑥 < (vol*‘𝑐)))
235119eqcomd 2767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑐 ∈ (Clsd‘(topGen‘ran (,))) → (vol*‘𝑐) = (vol‘𝑐))
236235anim1i 627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑐 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑥 < (vol*‘𝑐)) → ((vol*‘𝑐) = (vol‘𝑐) ∧ 𝑥 < (vol*‘𝑐)))
237236ex 418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 ∈ (Clsd‘(topGen‘ran (,))) → (𝑥 < (vol*‘𝑐) → ((vol*‘𝑐) = (vol‘𝑐) ∧ 𝑥 < (vol*‘𝑐))))
238237anim2d 624 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 ∈ (Clsd‘(topGen‘ran (,))) → ((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑥 < (vol*‘𝑐)) → (𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ ((vol*‘𝑐) = (vol‘𝑐) ∧ 𝑥 < (vol*‘𝑐)))))
239 fvex 6896 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (vol*‘𝑐) ∈ V
240 eqeq1 2765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑦 = (vol*‘𝑐) → (𝑦 = (vol‘𝑐) ↔ (vol*‘𝑐) = (vol‘𝑐)))
241240anbi2d 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 = (vol*‘𝑐) → ((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ↔ (𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ (vol*‘𝑐) = (vol‘𝑐))))
242 breq2 5107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 = (vol*‘𝑐) → (𝑥 < 𝑦 ↔ 𝑥 < (vol*‘𝑐)))
243241, 242anbi12d 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 = (vol*‘𝑐) → (((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦) ↔ ((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ (vol*‘𝑐) = (vol‘𝑐)) ∧ 𝑥 < (vol*‘𝑐))))
244239, 243spcev 3561 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ (vol*‘𝑐) = (vol‘𝑐)) ∧ 𝑥 < (vol*‘𝑐)) → ∃𝑦((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦))
245244anasss 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ ((vol*‘𝑐) = (vol‘𝑐) ∧ 𝑥 < (vol*‘𝑐))) → ∃𝑦((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦))
246238, 245syl6 36 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 ∈ (Clsd‘(topGen‘ran (,))) → ((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑥 < (vol*‘𝑐)) → ∃𝑦((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦)))
247246reximia 3098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑥 < (vol*‘𝑐)) → ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))∃𝑦((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦))
248234, 247syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑥 ∈ ℝ ∧ 𝑥 < (vol*‘∪ ran ((,) ∘ 𝑓))) → ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))∃𝑦((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦))
249 r19.41v 3193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦) ↔ (∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦))
250249exbii 1881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∃𝑦∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦) ↔ ∃𝑦(∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦))
251 rexcom4 3290 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))∃𝑦((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦) ↔ ∃𝑦∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦))
252131anbi2d 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 = 𝑦 → ((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐)) ↔ (𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐))))
253252rexbidv 3187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 = 𝑦 → (∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐)) ↔ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐))))
254253rexab 3653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∃𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))}𝑥 < 𝑦 ↔ ∃𝑦(∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦))
255250, 251, 2543bitr4i 306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))∃𝑦((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦) ↔ ∃𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))}𝑥 < 𝑦)
256248, 255sylib 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑥 ∈ ℝ ∧ 𝑥 < (vol*‘∪ ran ((,) ∘ 𝑓))) → ∃𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))}𝑥 < 𝑦)
257256adantl 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (vol*‘∪ ran ((,) ∘ 𝑓)))) → ∃𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))}𝑥 < 𝑦)
258201, 202, 226, 257eqsupd 9442 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < ) = (vol*‘∪ ran ((,) ∘ 𝑓)))
259258eqcomd 2767 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → (vol*‘∪ ran ((,) ∘ 𝑓)) = sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < ))
260259adantl 487 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘∪ ran ((,) ∘ 𝑓)) = sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < ))
261 sseq1 3956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 = 𝑎 → (𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ↔ 𝑎 ⊆ ∪ ran ((,) ∘ 𝑓)))
262 fveq2 6883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑐 = 𝑎 → (vol‘𝑐) = (vol‘𝑎))
263262eqeq2d 2772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 = 𝑎 → (𝑧 = (vol‘𝑐) ↔ 𝑧 = (vol‘𝑎)))
264261, 263anbi12d 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = 𝑎 → ((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐)) ↔ (𝑎 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑎))))
265264cbvrexvw 3242 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐)) ↔ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑎)))
266265abbii 2828 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))} = {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑎))}
267266supeq1i 9432 . . . . . . . . . . . . . . . . . . . . . . . . . 26 sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < ) = sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < )
268260, 267eqtrdi 2812 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘∪ ran ((,) ∘ 𝑓)) = sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ))
269 simpll 779 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ))
270 eqeq1 2765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = 𝑧 → (𝑦 = (vol‘𝑏) ↔ 𝑧 = (vol‘𝑏)))
271270anbi2d 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = 𝑧 → ((𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏)) ↔ (𝑏 ⊆ 𝐴 ∧ 𝑧 = (vol‘𝑏))))
272271rexbidv 3187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = 𝑧 → (∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏)) ↔ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑧 = (vol‘𝑏))))
273 sseq1 3956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑏 = 𝑐 → (𝑏 ⊆ 𝐴 ↔ 𝑐 ⊆ 𝐴))
274 fveq2 6883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑏 = 𝑐 → (vol‘𝑏) = (vol‘𝑐))
275274eqeq2d 2772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑏 = 𝑐 → (𝑧 = (vol‘𝑏) ↔ 𝑧 = (vol‘𝑐)))
276273, 275anbi12d 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑏 = 𝑐 → ((𝑏 ⊆ 𝐴 ∧ 𝑧 = (vol‘𝑏)) ↔ (𝑐 ⊆ 𝐴 ∧ 𝑧 = (vol‘𝑐))))
277276cbvrexvw 3242 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑧 = (vol‘𝑏)) ↔ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ 𝐴 ∧ 𝑧 = (vol‘𝑐)))
278272, 277bitrdi 290 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = 𝑧 → (∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏)) ↔ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ 𝐴 ∧ 𝑧 = (vol‘𝑐))))
279278cbvabv 2831 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 {𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))} = {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ 𝐴 ∧ 𝑧 = (vol‘𝑐))}
280279supeq1i 9432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < ) = sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ 𝐴 ∧ 𝑧 = (vol‘𝑐))}, ℝ, < )
281280eqeq2i 2774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < ) ↔ (vol*‘𝐴) = sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ 𝐴 ∧ 𝑧 = (vol‘𝑐))}, ℝ, < ))
282281biimpi 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < ) → (vol*‘𝐴) = sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ 𝐴 ∧ 𝑧 = (vol‘𝑐))}, ℝ, < ))
283282ad2antlr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘𝐴) = sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ 𝐴 ∧ 𝑧 = (vol‘𝑐))}, ℝ, < ))
284 mblfinlem3 38557 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((∪ ran ((,) ∘ 𝑓) ⊆ ℝ ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) ∧ (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ ((vol*‘∪ ran ((,) ∘ 𝑓)) = sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < ) ∧ (vol*‘𝐴) = sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ 𝐴 ∧ 𝑧 = (vol‘𝑐))}, ℝ, < ))) → sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < ) = (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴)))
285197, 269, 260, 283, 284syl112anc 1401 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < ) = (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴)))
286 sseq1 3956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 = 𝑎 → (𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ↔ 𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴)))
287286, 263anbi12d 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = 𝑎 → ((𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐)) ↔ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑎))))
288287cbvrexvw 3242 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐)) ↔ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑎)))
289288abbii 2828 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))} = {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑎))}
290289supeq1i 9432 . . . . . . . . . . . . . . . . . . . . . . . . . 26 sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < ) = sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < )
291285, 290eqtr3di 2811 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) = sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ))
292 mblfinlem3 38557 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((∪ ran ((,) ∘ 𝑓) ⊆ ℝ ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) ∧ ((∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ⊆ ℝ ∧ (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) ∈ ℝ) ∧ ((vol*‘∪ ran ((,) ∘ 𝑓)) = sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) ∧ (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) = sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ))) → sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) = (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴))))
293197, 199, 268, 291, 292syl112anc 1401 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) = (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴))))
294195, 293eqtrid 2808 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) = (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴))))
295294, 285oveq12d 7436 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) + sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < )) = ((vol*‘(∪ ran ((,) ∘ 𝑓) ∖ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) + (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴))))
296190, 295sylan 592 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑤 ⊆ ∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) + sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < )) = ((vol*‘(∪ ran ((,) ∘ 𝑓) ∖ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) + (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴))))
297189, 296breqtrrd 5133 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑤 ⊆ ∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ (sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) + sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < )))
298 ne0i 4287 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} → {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ≠ ∅)
299110, 298mp1i 14 . . . . . . . . . . . . . . . . . . . . . . 23 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ≠ ∅)
300 ne0i 4287 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))} → {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))} ≠ ∅)
301157, 300mp1i 14 . . . . . . . . . . . . . . . . . . . . . . 23 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))} ≠ ∅)
302 eqid 2761 . . . . . . . . . . . . . . . . . . . . . . 23 {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)} = {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)}
30374, 299, 88, 130, 301, 144, 302supadd 12278 . . . . . . . . . . . . . . . . . . . . . 22 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → (sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) + sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < )) = sup({𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)}, ℝ, < ))
304 reeanv 3235 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑢 = (vol‘𝑎)) ∧ (𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑣 = (vol‘𝑐))) ↔ (∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑢 = (vol‘𝑎)) ∧ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑣 = (vol‘𝑐))))
305 vex 3455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑢 ∈ V
306 eqeq1 2765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧 = 𝑢 → (𝑧 = (vol‘𝑎) ↔ 𝑢 = (vol‘𝑎)))
307306anbi2d 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 = 𝑢 → ((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)) ↔ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑢 = (vol‘𝑎))))
308307rexbidv 3187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 = 𝑢 → (∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)) ↔ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑢 = (vol‘𝑎))))
309305, 308elab 3633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ↔ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑢 = (vol‘𝑎)))
310 vex 3455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑣 ∈ V
311 eqeq1 2765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧 = 𝑣 → (𝑧 = (vol‘𝑐) ↔ 𝑣 = (vol‘𝑐)))
312311anbi2d 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 = 𝑣 → ((𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐)) ↔ (𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑣 = (vol‘𝑐))))
313312rexbidv 3187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 = 𝑣 → (∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐)) ↔ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑣 = (vol‘𝑐))))
314310, 313elab 3633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))} ↔ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑣 = (vol‘𝑐)))
315309, 314anbi12i 640 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}) ↔ (∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑢 = (vol‘𝑎)) ∧ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑣 = (vol‘𝑐))))
316304, 315bitr4i 281 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑢 = (vol‘𝑎)) ∧ (𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑣 = (vol‘𝑐))) ↔ (𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}))
317 an4 669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) ∧ (𝑢 = (vol‘𝑎) ∧ 𝑣 = (vol‘𝑐))) ↔ ((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑢 = (vol‘𝑎)) ∧ (𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑣 = (vol‘𝑐))))
318 oveq12 7427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑢 = (vol‘𝑎) ∧ 𝑣 = (vol‘𝑐)) → (𝑢 + 𝑣) = ((vol‘𝑎) + (vol‘𝑐)))
31959adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,)))) → 𝑎 ∈ dom vol)
320319ad2antlr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) → 𝑎 ∈ dom vol)
321117adantl 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,)))) → 𝑐 ∈ dom vol)
322321ad2antlr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) → 𝑐 ∈ dom vol)
323 ss2in 4190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) → (𝑎 ∩ 𝑐) ⊆ ((∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∩ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴)))
324185ineq1i 4162 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∩ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) = ((∪ ran ((,) ∘ 𝑓) ∖ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) ∩ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴))
325 incom 4155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((∪ ran ((,) ∘ 𝑓) ∖ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) ∩ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) = ((∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∩ (∪ ran ((,) ∘ 𝑓) ∖ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴)))
326 disjdif 4426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∩ (∪ ran ((,) ∘ 𝑓) ∖ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) = ∅
327324, 325, 3263eqtri 2788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∩ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) = ∅
328323, 327sseqtrdi 3971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) → (𝑎 ∩ 𝑐) ⊆ ∅)
329 ss0 4352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑎 ∩ 𝑐) ⊆ ∅ → (𝑎 ∩ 𝑐) = ∅)
330328, 329syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) → (𝑎 ∩ 𝑐) = ∅)
331330adantl 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) → (𝑎 ∩ 𝑐) = ∅)
33261adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,)))) → (vol‘𝑎) = (vol*‘𝑎))
333332ad2antlr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) → (vol‘𝑎) = (vol*‘𝑎))
33466, 16jctir 530 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) → (𝑎 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ ∪ ran ((,) ∘ 𝑓) ⊆ ℝ))
335683expa 1136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑎 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ ∪ ran ((,) ∘ 𝑓) ⊆ ℝ) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘𝑎) ∈ ℝ)
336334, 335sylan 592 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘𝑎) ∈ ℝ)
337336ancoms 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ 𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴)) → (vol*‘𝑎) ∈ ℝ)
338337ad2ant2r 760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) → (vol*‘𝑎) ∈ ℝ)
339333, 338eqeltrd 2861 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) → (vol‘𝑎) ∈ ℝ)
340119adantl 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,)))) → (vol‘𝑐) = (vol*‘𝑐))
341340ad2antlr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) → (vol‘𝑐) = (vol*‘𝑐))
342122, 16jctir 530 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) → (𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ ∪ ran ((,) ∘ 𝑓) ⊆ ℝ))
3431243expa 1136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ ∪ ran ((,) ∘ 𝑓) ⊆ ℝ) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘𝑐) ∈ ℝ)
344342, 343sylan 592 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘𝑐) ∈ ℝ)
345344ancoms 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ 𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) → (vol*‘𝑐) ∈ ℝ)
346345ad2ant2rl 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) → (vol*‘𝑐) ∈ ℝ)
347341, 346eqeltrd 2861 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) → (vol‘𝑐) ∈ ℝ)
348 volun 25859 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝑎 ∈ dom vol ∧ 𝑐 ∈ dom vol ∧ (𝑎 ∩ 𝑐) = ∅) ∧ ((vol‘𝑎) ∈ ℝ ∧ (vol‘𝑐) ∈ ℝ)) → (vol‘(𝑎 ∪ 𝑐)) = ((vol‘𝑎) + (vol‘𝑐)))
349320, 322, 331, 339, 347, 348syl32anc 1405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) → (vol‘(𝑎 ∪ 𝑐)) = ((vol‘𝑎) + (vol‘𝑐)))
350 unmbl 25851 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑎 ∈ dom vol ∧ 𝑐 ∈ dom vol) → (𝑎 ∪ 𝑐) ∈ dom vol)
35159, 117, 350syl2an 608 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,)))) → (𝑎 ∪ 𝑐) ∈ dom vol)
352 mblvol 25844 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑎 ∪ 𝑐) ∈ dom vol → (vol‘(𝑎 ∪ 𝑐)) = (vol*‘(𝑎 ∪ 𝑐)))
353351, 352syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,)))) → (vol‘(𝑎 ∪ 𝑐)) = (vol*‘(𝑎 ∪ 𝑐)))
354353ad2antlr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) → (vol‘(𝑎 ∪ 𝑐)) = (vol*‘(𝑎 ∪ 𝑐)))
355349, 354eqtr3d 2798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) → ((vol‘𝑎) + (vol‘𝑐)) = (vol*‘(𝑎 ∪ 𝑐)))
356318, 355sylan9eqr 2818 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) ∧ (𝑢 = (vol‘𝑎) ∧ 𝑣 = (vol‘𝑐))) → (𝑢 + 𝑣) = (vol*‘(𝑎 ∪ 𝑐)))
357 eqtr 2781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑦 = (𝑢 + 𝑣) ∧ (𝑢 + 𝑣) = (vol*‘(𝑎 ∪ 𝑐))) → 𝑦 = (vol*‘(𝑎 ∪ 𝑐)))
358357ancoms 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑢 + 𝑣) = (vol*‘(𝑎 ∪ 𝑐)) ∧ 𝑦 = (𝑢 + 𝑣)) → 𝑦 = (vol*‘(𝑎 ∪ 𝑐)))
359356, 358sylan 592 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) ∧ (𝑢 = (vol‘𝑎) ∧ 𝑣 = (vol‘𝑐))) ∧ 𝑦 = (𝑢 + 𝑣)) → 𝑦 = (vol*‘(𝑎 ∪ 𝑐)))
36066, 122anim12i 625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) → (𝑎 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑐 ⊆ ∪ ran ((,) ∘ 𝑓)))
361 unss 4136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑎 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑐 ⊆ ∪ ran ((,) ∘ 𝑓)) ↔ (𝑎 ∪ 𝑐) ⊆ ∪ ran ((,) ∘ 𝑓))
362360, 361sylib 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) → (𝑎 ∪ 𝑐) ⊆ ∪ ran ((,) ∘ 𝑓))
363 ovolss 25799 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑎 ∪ 𝑐) ⊆ ∪ ran ((,) ∘ 𝑓) ∧ ∪ ran ((,) ∘ 𝑓) ⊆ ℝ) → (vol*‘(𝑎 ∪ 𝑐)) ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))
364362, 16, 363sylancl 598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) → (vol*‘(𝑎 ∪ 𝑐)) ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))
365364ad3antlr 744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) ∧ (𝑢 = (vol‘𝑎) ∧ 𝑣 = (vol‘𝑐))) ∧ 𝑦 = (𝑢 + 𝑣)) → (vol*‘(𝑎 ∪ 𝑐)) ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))
366359, 365eqbrtrd 5127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) ∧ (𝑢 = (vol‘𝑎) ∧ 𝑣 = (vol‘𝑐))) ∧ 𝑦 = (𝑢 + 𝑣)) → 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))
367366ex 418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) ∧ (𝑢 = (vol‘𝑎) ∧ 𝑣 = (vol‘𝑐))) → (𝑦 = (𝑢 + 𝑣) → 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓))))
368367expl 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) → (((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) ∧ (𝑢 = (vol‘𝑎) ∧ 𝑣 = (vol‘𝑐))) → (𝑦 = (𝑢 + 𝑣) → 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))))
369317, 368biimtrrid 246 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) → (((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑢 = (vol‘𝑎)) ∧ (𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑣 = (vol‘𝑐))) → (𝑦 = (𝑢 + 𝑣) → 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))))
370369rexlimdvva 3220 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → (∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑢 = (vol‘𝑎)) ∧ (𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑣 = (vol‘𝑐))) → (𝑦 = (𝑢 + 𝑣) → 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))))
371316, 370biimtrrid 246 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → ((𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}) → (𝑦 = (𝑢 + 𝑣) → 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))))
372371rexlimdvv 3219 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → (∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦 = (𝑢 + 𝑣) → 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓))))
373372alrimiv 1960 . . . . . . . . . . . . . . . . . . . . . . . 24 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → ∀𝑦(∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦 = (𝑢 + 𝑣) → 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓))))
374 eqeq1 2765 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = 𝑦 → (𝑡 = (𝑢 + 𝑣) ↔ 𝑦 = (𝑢 + 𝑣)))
3753742rexbidv 3228 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑦 → (∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣) ↔ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦 = (𝑢 + 𝑣)))
376375ralab 3651 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑦 ∈ {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)}𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓)) ↔ ∀𝑦(∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦 = (𝑢 + 𝑣) → 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓))))
377373, 376sylibr 237 . . . . . . . . . . . . . . . . . . . . . . 23 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → ∀𝑦 ∈ {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)}𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))
378 simpr 490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))})) ∧ 𝑡 = (𝑢 + 𝑣)) → 𝑡 = (𝑢 + 𝑣))
37974sselda 3931 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ 𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}) → 𝑢 ∈ ℝ)
380130sselda 3931 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}) → 𝑣 ∈ ℝ)
381 readdcl 11276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → (𝑢 + 𝑣) ∈ ℝ)
382379, 380, 381syl2an 608 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ 𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}) ∧ ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))})) → (𝑢 + 𝑣) ∈ ℝ)
383382anandis 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))})) → (𝑢 + 𝑣) ∈ ℝ)
384383adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))})) ∧ 𝑡 = (𝑢 + 𝑣)) → (𝑢 + 𝑣) ∈ ℝ)
385378, 384eqeltrd 2861 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))})) ∧ 𝑡 = (𝑢 + 𝑣)) → 𝑡 ∈ ℝ)
386385ex 418 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))})) → (𝑡 = (𝑢 + 𝑣) → 𝑡 ∈ ℝ))
387386rexlimdvva 3220 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → (∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣) → 𝑡 ∈ ℝ))
388387abssdv 4015 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)} ⊆ ℝ)
389 00id 11478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (0 + 0) = 0
390389eqcomi 2770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 0 = (0 + 0)
391 rspceov 7467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((0 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ∧ 0 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))} ∧ 0 = (0 + 0)) → ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}0 = (𝑢 + 𝑣))
392110, 157, 390, 391mp3an 1490 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}0 = (𝑢 + 𝑣)
393 eqeq1 2765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑡 = 0 → (𝑡 = (𝑢 + 𝑣) ↔ 0 = (𝑢 + 𝑣)))
3943932rexbidv 3228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑡 = 0 → (∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣) ↔ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}0 = (𝑢 + 𝑣)))
395105, 394spcev 3561 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}0 = (𝑢 + 𝑣) → ∃𝑡∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣))
396392, 395ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ∃𝑡∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)
397 abn0 4334 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)} ≠ ∅ ↔ ∃𝑡∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣))
398396, 397mpbir 234 . . . . . . . . . . . . . . . . . . . . . . . . . 26 {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)} ≠ ∅
399398a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)} ≠ ∅)
400 brralrspcev 5165 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ ∀𝑦 ∈ {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)}𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓))) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)}𝑦 ≤ 𝑥)
401377, 400mpdan 700 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)}𝑦 ≤ 𝑥)
402388, 399, 4013jca 1146 . . . . . . . . . . . . . . . . . . . . . . . 24 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → ({𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)} ⊆ ℝ ∧ {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)}𝑦 ≤ 𝑥))
403 suprleub 12276 . . . . . . . . . . . . . . . . . . . . . . . 24 ((({𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)} ⊆ ℝ ∧ {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)}𝑦 ≤ 𝑥) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (sup({𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)}, ℝ, < ) ≤ (vol*‘∪ ran ((,) ∘ 𝑓)) ↔ ∀𝑦 ∈ {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)}𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓))))
404402, 403mpancom 701 . . . . . . . . . . . . . . . . . . . . . . 23 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → (sup({𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)}, ℝ, < ) ≤ (vol*‘∪ ran ((,) ∘ 𝑓)) ↔ ∀𝑦 ∈ {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)}𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓))))
405377, 404mpbird 260 . . . . . . . . . . . . . . . . . . . . . 22 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → sup({𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)}, ℝ, < ) ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))
406303, 405eqbrtrd 5127 . . . . . . . . . . . . . . . . . . . . 21 ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → (sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) + sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < )) ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))
407406adantl 487 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑤 ⊆ ∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) + sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < )) ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))
40845, 163, 164, 297, 407letrd 11460 . . . . . . . . . . . . . . . . . . 19 ((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑤 ⊆ ∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))
40944, 408sylan2 605 . . . . . . . . . . . . . . . . . 18 ((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑤 ⊆ ∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ≠ +∞) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))
41033, 409pm2.61dane 3043 . . . . . . . . . . . . . . . . 17 (((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑤 ⊆ ∪ ran ((,) ∘ 𝑓)) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))
411410adantlr 728 . . . . . . . . . . . . . . . 16 ((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑓:ℕ⟶( ≤ ∩ (ℝ × ℝ))) ∧ 𝑤 ⊆ ∪ ran ((,) ∘ 𝑓)) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))
412 ssid 3953 . . . . . . . . . . . . . . . . . 18 ∪ ran ((,) ∘ 𝑓) ⊆ ∪ ran ((,) ∘ 𝑓)
41320ovollb 25793 . . . . . . . . . . . . . . . . . 18 ((𝑓:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ∪ ran ((,) ∘ 𝑓) ⊆ ∪ ran ((,) ∘ 𝑓)) → (vol*‘∪ ran ((,) ∘ 𝑓)) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))
414412, 413mpan2 704 . . . . . . . . . . . . . . . . 17 (𝑓:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → (vol*‘∪ ran ((,) ∘ 𝑓)) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))
415414ad2antlr 740 . . . . . . . . . . . . . . . 16 ((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑓:ℕ⟶( ≤ ∩ (ℝ × ℝ))) ∧ 𝑤 ⊆ ∪ ran ((,) ∘ 𝑓)) → (vol*‘∪ ran ((,) ∘ 𝑓)) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))
41612, 18, 27, 411, 415xrletrd 13284 . . . . . . . . . . . . . . 15 ((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑓:ℕ⟶( ≤ ∩ (ℝ × ℝ))) ∧ 𝑤 ⊆ ∪ ran ((,) ∘ 𝑓)) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))
417416adantr 486 . . . . . . . . . . . . . 14 (((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑓:ℕ⟶( ≤ ∩ (ℝ × ℝ))) ∧ 𝑤 ⊆ ∪ ran ((,) ∘ 𝑓)) ∧ 𝑢 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < )) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))
418 simpr 490 . . . . . . . . . . . . . 14 (((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑓:ℕ⟶( ≤ ∩ (ℝ × ℝ))) ∧ 𝑤 ⊆ ∪ ran ((,) ∘ 𝑓)) ∧ 𝑢 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < )) → 𝑢 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))
419417, 418breqtrrd 5133 . . . . . . . . . . . . 13 (((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑓:ℕ⟶( ≤ ∩ (ℝ × ℝ))) ∧ 𝑤 ⊆ ∪ ran ((,) ∘ 𝑓)) ∧ 𝑢 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < )) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ 𝑢)
420419expl 463 . . . . . . . . . . . 12 (((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑓:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → ((𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑢 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < )) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ 𝑢))
4213, 420sylan2 605 . . . . . . . . . . 11 (((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)) → ((𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑢 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < )) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ 𝑢))
422421rexlimdva 3164 . . . . . . . . . 10 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) → (∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑢 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < )) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ 𝑢))
423422ralrimivw 3159 . . . . . . . . 9 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) → ∀𝑢 ∈ ℝ* (∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑢 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < )) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ 𝑢))
424 eqeq1 2765 . . . . . . . . . . . 12 (𝑣 = 𝑢 → (𝑣 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ↔ 𝑢 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < )))
425424anbi2d 642 . . . . . . . . . . 11 (𝑣 = 𝑢 → ((𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < )) ↔ (𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑢 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))))
426425rexbidv 3187 . . . . . . . . . 10 (𝑣 = 𝑢 → (∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < )) ↔ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑢 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))))
427426ralrab 3652 . . . . . . . . 9 (∀𝑢 ∈ {𝑣 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ 𝑢 ↔ ∀𝑢 ∈ ℝ* (∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑢 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < )) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ 𝑢))
428423, 427sylibr 237 . . . . . . . 8 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) → ∀𝑢 ∈ {𝑣 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ 𝑢)
429 ssrab2 4028 . . . . . . . . 9 {𝑣 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} ⊆ ℝ*
43011adantl 487 . . . . . . . . 9 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ∈ ℝ*)
431 infxrgelb 13459 . . . . . . . . 9 (({𝑣 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} ⊆ ℝ* ∧ ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ∈ ℝ*) → (((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ inf({𝑣 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}, ℝ*, < ) ↔ ∀𝑢 ∈ {𝑣 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ 𝑢))
432429, 430, 431sylancr 599 . . . . . . . 8 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) → (((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ inf({𝑣 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}, ℝ*, < ) ↔ ∀𝑢 ∈ {𝑣 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ 𝑢))
433428, 432mpbird 260 . . . . . . 7 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ inf({𝑣 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}, ℝ*, < ))
434 eqid 2761 . . . . . . . . 9 {𝑣 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} = {𝑣 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}
435434ovolval 25787 . . . . . . . 8 (𝑤 ⊆ ℝ → (vol*‘𝑤) = inf({𝑣 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}, ℝ*, < ))
436435ad2antrl 741 . . . . . . 7 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) → (vol*‘𝑤) = inf({𝑣 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}, ℝ*, < ))
437433, 436breqtrrd 5133 . . . . . 6 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ (vol*‘𝑤))
438437expr 462 . . . . 5 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ 𝑤 ⊆ ℝ) → ((vol*‘𝑤) ∈ ℝ → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ (vol*‘𝑤)))
4392, 438sylan2 605 . . . 4 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ 𝑤 ∈ 𝒫 ℝ) → ((vol*‘𝑤) ∈ ℝ → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ (vol*‘𝑤)))
440439ralrimiva 3155 . . 3 (((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) → ∀𝑤 ∈ 𝒫 ℝ((vol*‘𝑤) ∈ ℝ → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ (vol*‘𝑤)))
441 ismbl2 25841 . . . . 5 (𝐴 ∈ dom vol ↔ (𝐴 ⊆ ℝ ∧ ∀𝑤 ∈ 𝒫 ℝ((vol*‘𝑤) ∈ ℝ → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ (vol*‘𝑤))))
442441baibr 546 . . . 4 (𝐴 ⊆ ℝ → (∀𝑤 ∈ 𝒫 ℝ((vol*‘𝑤) ∈ ℝ → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ (vol*‘𝑤)) ↔ 𝐴 ∈ dom vol))
443442ad2antrr 739 . . 3 (((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) → (∀𝑤 ∈ 𝒫 ℝ((vol*‘𝑤) ∈ ℝ → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ (vol*‘𝑤)) ↔ 𝐴 ∈ dom vol))
444440, 443mpbid 235 . 2 (((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) → 𝐴 ∈ dom vol)
4451, 444impbida 813 1 ((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) → (𝐴 ∈ dom vol ↔ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )))
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145  {cab 2739   ≠ wne 2956  ∀wral 3077  ∃wrex 3087  {crab 3413   ∖ cdif 3896   ∪ cun 3897   ∩ cin 3898   ⊆ wss 3899  ∅c0 4279  𝒫 cpw 4557  ∪ cuni 4867   class class class wbr 5103   Or wor 5558   × cxp 5649  dom cdm 5651  ran crn 5652   ∘ ccom 5655  ⟶wf 6533  ‘cfv 6537  (class class class)co 7418   ↑m cmap 8840  supcsup 9425  infcinf 9426  ℝcr 11192  0cc0 11193  1c1 11194   + caddc 11196  +∞cpnf 11333  ℝ*cxr 11335   < clt 11336   ≤ cle 11337   − cmin 11534  ℕcn 12328  (,)cioo 13469  [,)cico 13471  seqcseq 14137  abscabs 15394  topGenctg 17601  Topctop 23204  TopBasesctb 23256  Clsdccld 23327  vol*covol 25776  volcvol 25777
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-inf2 9635  ax-cnex 11249  ax-resscn 11250  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-addrcl 11254  ax-mulcl 11255  ax-mulrcl 11256  ax-mulcom 11257  ax-addass 11258  ax-mulass 11259  ax-distr 11260  ax-i2m1 11261  ax-1ne0 11262  ax-1rid 11263  ax-rnegex 11264  ax-rrecex 11265  ax-cnre 11266  ax-pre-lttri 11267  ax-pre-lttrn 11268  ax-pre-ltadd 11269  ax-pre-mulgt0 11270  ax-pre-sup 11271
This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-disj 5071  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-se 5605  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7375  df-ov 7421  df-oprab 7422  df-mpo 7423  df-of 7691  df-om 7876  df-1st 7999  df-2nd 8000  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-1o 8469  df-2o 8470  df-oadd 8473  df-omul 8474  df-er 8710  df-map 8842  df-pm 8843  df-en 8967  df-dom 8968  df-sdom 8969  df-fin 8970  df-fi 9396  df-sup 9427  df-inf 9428  df-oi 9497  df-dju 9975  df-card 10013  df-acn 10016  df-pnf 11338  df-mnf 11339  df-xr 11340  df-ltxr 11341  df-le 11342  df-sub 11536  df-neg 11537  df-div 11967  df-nn 12329  df-2 12398  df-3 12399  df-4 12400  df-n0 12600  df-z 12687  df-uz 12959  df-q 13069  df-rp 13114  df-xneg 13234  df-xadd 13235  df-xmul 13236  df-ioo 13473  df-ico 13475  df-icc 13476  df-fz 13633  df-fzo 13782  df-fl 13925  df-seq 14138  df-exp 14198  df-hash 14468  df-cj 15259  df-re 15260  df-im 15261  df-sqrt 15395  df-abs 15396  df-clim 15648  df-rlim 15649  df-sum 15847  df-rest 17586  df-topgen 17607  df-psmet 21663  df-xmet 21664  df-met 21665  df-bl 21666  df-mopn 21667  df-top 23205  df-topon 23222  df-bases 23257  df-cld 23330  df-cmp 23698  df-conn 23723  df-ovol 25778  df-vol 25779
This theorem is used by: (None)
  Copyright terms: Public domain W3C validator