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 33121
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 33120 . 2 (((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ 𝐴 ∈ dom vol) → (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < ))
2 elpwi 4146 . . . . 5 (𝑤 ∈ 𝒫 ℝ → 𝑤 ⊆ ℝ)
3 elmapi 7839 . . . . . . . . . . . 12 (𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ) → 𝑓:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
4 inss1 3817 . . . . . . . . . . . . . . . . . . . 20 (𝑤𝐴) ⊆ 𝑤
5 ovolsscl 23194 . . . . . . . . . . . . . . . . . . . 20 (((𝑤𝐴) ⊆ 𝑤𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) → (vol*‘(𝑤𝐴)) ∈ ℝ)
64, 5mp3an1 1408 . . . . . . . . . . . . . . . . . . 19 ((𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) → (vol*‘(𝑤𝐴)) ∈ ℝ)
7 difss 3721 . . . . . . . . . . . . . . . . . . . 20 (𝑤𝐴) ⊆ 𝑤
8 ovolsscl 23194 . . . . . . . . . . . . . . . . . . . 20 (((𝑤𝐴) ⊆ 𝑤𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) → (vol*‘(𝑤𝐴)) ∈ ℝ)
97, 8mp3an1 1408 . . . . . . . . . . . . . . . . . . 19 ((𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) → (vol*‘(𝑤𝐴)) ∈ ℝ)
106, 9readdcld 10029 . . . . . . . . . . . . . . . . . 18 ((𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) → ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ∈ ℝ)
1110rexrd 10049 . . . . . . . . . . . . . . . . 17 ((𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) → ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ∈ ℝ*)
1211ad3antlr 766 . . . . . . . . . . . . . . . 16 ((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑓:ℕ⟶( ≤ ∩ (ℝ × ℝ))) ∧ 𝑤 ran ((,) ∘ 𝑓)) → ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ∈ ℝ*)
13 rncoss 5356 . . . . . . . . . . . . . . . . . . 19 ran ((,) ∘ 𝑓) ⊆ ran (,)
1413unissi 4434 . . . . . . . . . . . . . . . . . 18 ran ((,) ∘ 𝑓) ⊆ ran (,)
15 unirnioo 12231 . . . . . . . . . . . . . . . . . 18 ℝ = ran (,)
1614, 15sseqtr4i 3623 . . . . . . . . . . . . . . . . 17 ran ((,) ∘ 𝑓) ⊆ ℝ
17 ovolcl 23186 . . . . . . . . . . . . . . . . 17 ( ran ((,) ∘ 𝑓) ⊆ ℝ → (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ*)
1816, 17mp1i 13 . . . . . . . . . . . . . . . 16 ((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑓:ℕ⟶( ≤ ∩ (ℝ × ℝ))) ∧ 𝑤 ran ((,) ∘ 𝑓)) → (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ*)
19 eqid 2621 . . . . . . . . . . . . . . . . . . 19 ((abs ∘ − ) ∘ 𝑓) = ((abs ∘ − ) ∘ 𝑓)
20 eqid 2621 . . . . . . . . . . . . . . . . . . 19 seq1( + , ((abs ∘ − ) ∘ 𝑓)) = seq1( + , ((abs ∘ − ) ∘ 𝑓))
2119, 20ovolsf 23181 . . . . . . . . . . . . . . . . . 18 (𝑓:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → seq1( + , ((abs ∘ − ) ∘ 𝑓)):ℕ⟶(0[,)+∞))
22 frn 6020 . . . . . . . . . . . . . . . . . . 19 (seq1( + , ((abs ∘ − ) ∘ 𝑓)):ℕ⟶(0[,)+∞) → ran seq1( + , ((abs ∘ − ) ∘ 𝑓)) ⊆ (0[,)+∞))
23 icossxr 12216 . . . . . . . . . . . . . . . . . . 19 (0[,)+∞) ⊆ ℝ*
2422, 23syl6ss 3600 . . . . . . . . . . . . . . . . . 18 (seq1( + , ((abs ∘ − ) ∘ 𝑓)):ℕ⟶(0[,)+∞) → ran seq1( + , ((abs ∘ − ) ∘ 𝑓)) ⊆ ℝ*)
25 supxrcl 12104 . . . . . . . . . . . . . . . . . 18 (ran seq1( + , ((abs ∘ − ) ∘ 𝑓)) ⊆ ℝ* → sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ∈ ℝ*)
2621, 24, 253syl 18 . . . . . . . . . . . . . . . . 17 (𝑓:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ∈ ℝ*)
2726ad2antlr 762 . . . . . . . . . . . . . . . 16 ((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑓:ℕ⟶( ≤ ∩ (ℝ × ℝ))) ∧ 𝑤 ran ((,) ∘ 𝑓)) → sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ∈ ℝ*)
28 pnfge 11924 . . . . . . . . . . . . . . . . . . . . . 22 (((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ∈ ℝ* → ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ +∞)
2911, 28syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) → ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ +∞)
3029ad2antrr 761 . . . . . . . . . . . . . . . . . . . 20 ((((𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) ∧ 𝑤 ran ((,) ∘ 𝑓)) ∧ (vol*‘ ran ((,) ∘ 𝑓)) = +∞) → ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ +∞)
31 simpr 477 . . . . . . . . . . . . . . . . . . . 20 ((((𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) ∧ 𝑤 ran ((,) ∘ 𝑓)) ∧ (vol*‘ ran ((,) ∘ 𝑓)) = +∞) → (vol*‘ ran ((,) ∘ 𝑓)) = +∞)
3230, 31breqtrrd 4651 . . . . . . . . . . . . . . . . . . 19 ((((𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) ∧ 𝑤 ran ((,) ∘ 𝑓)) ∧ (vol*‘ ran ((,) ∘ 𝑓)) = +∞) → ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ (vol*‘ ran ((,) ∘ 𝑓)))
3332adantlll 753 . . . . . . . . . . . . . . . . . 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 11955 . . . . . . . . . . . . . . . . . . . . . 22 ((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ* → ((vol*‘ ran ((,) ∘ 𝑓)) = +∞ ↔ ¬ (vol*‘ ran ((,) ∘ 𝑓)) < +∞))
3634, 35ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 ((vol*‘ ran ((,) ∘ 𝑓)) = +∞ ↔ ¬ (vol*‘ ran ((,) ∘ 𝑓)) < +∞)
3736necon2abii 2840 . . . . . . . . . . . . . . . . . . . 20 ((vol*‘ ran ((,) ∘ 𝑓)) < +∞ ↔ (vol*‘ ran ((,) ∘ 𝑓)) ≠ +∞)
38 ovolge0 23189 . . . . . . . . . . . . . . . . . . . . . 22 ( ran ((,) ∘ 𝑓) ⊆ ℝ → 0 ≤ (vol*‘ ran ((,) ∘ 𝑓)))
3916, 38ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 0 ≤ (vol*‘ ran ((,) ∘ 𝑓))
40 0re 10000 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ ℝ
41 xrre3 11961 . . . . . . . . . . . . . . . . . . . . . 22 ((((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ* ∧ 0 ∈ ℝ) ∧ (0 ≤ (vol*‘ ran ((,) ∘ 𝑓)) ∧ (vol*‘ ran ((,) ∘ 𝑓)) < +∞)) → (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ)
4234, 40, 41mpanl12 717 . . . . . . . . . . . . . . . . . . . . 21 ((0 ≤ (vol*‘ ran ((,) ∘ 𝑓)) ∧ (vol*‘ ran ((,) ∘ 𝑓)) < +∞) → (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ)
4339, 42mpan 705 . . . . . . . . . . . . . . . . . . . 20 ((vol*‘ ran ((,) ∘ 𝑓)) < +∞ → (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ)
4437, 43sylbir 225 . . . . . . . . . . . . . . . . . . 19 ((vol*‘ ran ((,) ∘ 𝑓)) ≠ +∞ → (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ)
4510ad3antlr 766 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑤 ran ((,) ∘ 𝑓)) ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ∈ ℝ)
46 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)) → 𝑧 = (vol‘𝑎))
47 eleq1 2686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑏 = 𝑎 → (𝑏 ∈ dom vol ↔ 𝑎 ∈ dom vol))
48 uniretop 22506 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ℝ = (topGen‘ran (,))
4948cldss 20773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑏 ∈ (Clsd‘(topGen‘ran (,))) → 𝑏 ⊆ ℝ)
50 dfss4 3842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑏 ⊆ ℝ ↔ (ℝ ∖ (ℝ ∖ 𝑏)) = 𝑏)
5149, 50sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑏 ∈ (Clsd‘(topGen‘ran (,))) → (ℝ ∖ (ℝ ∖ 𝑏)) = 𝑏)
52 rembl 23248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ℝ ∈ dom vol
5348cldopn 20775 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑏 ∈ (Clsd‘(topGen‘ran (,))) → (ℝ ∖ 𝑏) ∈ (topGen‘ran (,)))
54 opnmbl 23310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((ℝ ∖ 𝑏) ∈ (topGen‘ran (,)) → (ℝ ∖ 𝑏) ∈ dom vol)
5553, 54syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑏 ∈ (Clsd‘(topGen‘ran (,))) → (ℝ ∖ 𝑏) ∈ dom vol)
56 difmbl 23251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((ℝ ∈ dom vol ∧ (ℝ ∖ 𝑏) ∈ dom vol) → (ℝ ∖ (ℝ ∖ 𝑏)) ∈ dom vol)
5752, 55, 56sylancr 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑏 ∈ (Clsd‘(topGen‘ran (,))) → (ℝ ∖ (ℝ ∖ 𝑏)) ∈ dom vol)
5851, 57eqeltrrd 2699 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑏 ∈ (Clsd‘(topGen‘ran (,))) → 𝑏 ∈ dom vol)
5947, 58vtoclga 3262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎 ∈ (Clsd‘(topGen‘ran (,))) → 𝑎 ∈ dom vol)
60 mblvol 23238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎 ∈ dom vol → (vol‘𝑎) = (vol*‘𝑎))
6159, 60syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 ∈ (Clsd‘(topGen‘ran (,))) → (vol‘𝑎) = (vol*‘𝑎))
6246, 61sylan9eqr 2677 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))) → 𝑧 = (vol*‘𝑎))
6362adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)))) → 𝑧 = (vol*‘𝑎))
64 inss1 3817 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ( ran ((,) ∘ 𝑓) ∩ 𝐴) ⊆ ran ((,) ∘ 𝑓)
65 sstr 3596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ⊆ ran ((,) ∘ 𝑓)) → 𝑎 ran ((,) ∘ 𝑓))
6664, 65mpan2 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) → 𝑎 ran ((,) ∘ 𝑓))
6766ad2antrl 763 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))) → 𝑎 ran ((,) ∘ 𝑓))
68 ovolsscl 23194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑎 ran ((,) ∘ 𝑓) ∧ ran ((,) ∘ 𝑓) ⊆ ℝ ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘𝑎) ∈ ℝ)
6916, 68mp3an2 1409 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑎 ran ((,) ∘ 𝑓) ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘𝑎) ∈ ℝ)
7069ancoms 469 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ 𝑎 ran ((,) ∘ 𝑓)) → (vol*‘𝑎) ∈ ℝ)
7167, 70sylan2 491 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)))) → (vol*‘𝑎) ∈ ℝ)
7263, 71eqeltrd 2698 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)))) → 𝑧 ∈ ℝ)
7372rexlimdvaa 3027 . . . . . . . . . . . . . . . . . . . . . . . 24 ((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ → (∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)) → 𝑧 ∈ ℝ))
7473abssdv 3661 . . . . . . . . . . . . . . . . . . . . . . 23 ((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ → {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ⊆ ℝ)
75 eqeq1 2625 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 = 𝑦 → (𝑧 = (vol‘𝑎) ↔ 𝑦 = (vol‘𝑎)))
7675anbi2d 739 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = 𝑦 → ((𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)) ↔ (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑦 = (vol‘𝑎))))
7776rexbidv 3047 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 = 𝑦 → (∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)) ↔ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑦 = (vol‘𝑎))))
7877ralab 3354 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑦 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}𝑦 ≤ (vol*‘ ran ((,) ∘ 𝑓)) ↔ ∀𝑦(∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑦 = (vol‘𝑎)) → 𝑦 ≤ (vol*‘ ran ((,) ∘ 𝑓))))
79 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑦 = (vol‘𝑎)) → 𝑦 = (vol‘𝑎))
8079, 61sylan9eqr 2677 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑦 = (vol‘𝑎))) → 𝑦 = (vol*‘𝑎))
81 ovolss 23193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑎 ran ((,) ∘ 𝑓) ∧ ran ((,) ∘ 𝑓) ⊆ ℝ) → (vol*‘𝑎) ≤ (vol*‘ ran ((,) ∘ 𝑓)))
8266, 16, 81sylancl 693 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) → (vol*‘𝑎) ≤ (vol*‘ ran ((,) ∘ 𝑓)))
8382ad2antrl 763 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑦 = (vol‘𝑎))) → (vol*‘𝑎) ≤ (vol*‘ ran ((,) ∘ 𝑓)))
8480, 83eqbrtrd 4645 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑦 = (vol‘𝑎))) → 𝑦 ≤ (vol*‘ ran ((,) ∘ 𝑓)))
8584rexlimiva 3023 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑦 = (vol‘𝑎)) → 𝑦 ≤ (vol*‘ ran ((,) ∘ 𝑓)))
8678, 85mpgbir 1723 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑦 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}𝑦 ≤ (vol*‘ ran ((,) ∘ 𝑓))
87 breq2 4627 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = (vol*‘ ran ((,) ∘ 𝑓)) → (𝑦𝑥𝑦 ≤ (vol*‘ ran ((,) ∘ 𝑓))))
8887ralbidv 2982 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = (vol*‘ ran ((,) ∘ 𝑓)) → (∀𝑦 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}𝑦𝑥 ↔ ∀𝑦 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}𝑦 ≤ (vol*‘ ran ((,) ∘ 𝑓))))
8988rspcev 3299 . . . . . . . . . . . . . . . . . . . . . . . 24 (((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ ∀𝑦 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}𝑦 ≤ (vol*‘ ran ((,) ∘ 𝑓))) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}𝑦𝑥)
9086, 89mpan2 706 . . . . . . . . . . . . . . . . . . . . . . 23 ((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}𝑦𝑥)
91 retop 22505 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (topGen‘ran (,)) ∈ Top
92 0cld 20782 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((topGen‘ran (,)) ∈ Top → ∅ ∈ (Clsd‘(topGen‘ran (,))))
9391, 92ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ∅ ∈ (Clsd‘(topGen‘ran (,)))
94 0ss 3950 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ∅ ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴)
95 0mbl 23247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ∅ ∈ dom vol
96 mblvol 23238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
9795, 96ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (vol‘∅) = (vol*‘∅)
98 ovol0 23201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (vol*‘∅) = 0
9997, 98eqtr2i 2644 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 0 = (vol‘∅)
10094, 99pm3.2i 471 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∅ ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 0 = (vol‘∅))
101 sseq1 3611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎 = ∅ → (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ↔ ∅ ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴)))
102 fveq2 6158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 = ∅ → (vol‘𝑎) = (vol‘∅))
103102eqeq2d 2631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎 = ∅ → (0 = (vol‘𝑎) ↔ 0 = (vol‘∅)))
104101, 103anbi12d 746 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 = ∅ → ((𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 0 = (vol‘𝑎)) ↔ (∅ ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 0 = (vol‘∅))))
105104rspcev 3299 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((∅ ∈ (Clsd‘(topGen‘ran (,))) ∧ (∅ ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 0 = (vol‘∅))) → ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 0 = (vol‘𝑎)))
10693, 100, 105mp2an 707 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 0 = (vol‘𝑎))
107 c0ex 9994 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 0 ∈ V
108 eqeq1 2625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 = 0 → (𝑧 = (vol‘𝑎) ↔ 0 = (vol‘𝑎)))
109108anbi2d 739 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 = 0 → ((𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)) ↔ (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 0 = (vol‘𝑎))))
110109rexbidv 3047 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = 0 → (∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)) ↔ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 0 = (vol‘𝑎))))
111107, 110elab 3338 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ↔ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 0 = (vol‘𝑎)))
112106, 111mpbir 221 . . . . . . . . . . . . . . . . . . . . . . . . 25 0 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}
113112ne0ii 3905 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ≠ ∅
114 suprcl 10943 . . . . . . . . . . . . . . . . . . . . . . . 24 (({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ⊆ ℝ ∧ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}𝑦𝑥) → sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) ∈ ℝ)
115113, 114mp3an2 1409 . . . . . . . . . . . . . . . . . . . . . . 23 (({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}𝑦𝑥) → sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) ∈ ℝ)
11674, 90, 115syl2anc 692 . . . . . . . . . . . . . . . . . . . . . 22 ((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ → sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) ∈ ℝ)
117 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐)) → 𝑧 = (vol‘𝑐))
118 eleq1 2686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑏 = 𝑐 → (𝑏 ∈ dom vol ↔ 𝑐 ∈ dom vol))
119118, 58vtoclga 3262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ (Clsd‘(topGen‘ran (,))) → 𝑐 ∈ dom vol)
120 mblvol 23238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ dom vol → (vol‘𝑐) = (vol*‘𝑐))
121119, 120syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 ∈ (Clsd‘(topGen‘ran (,))) → (vol‘𝑐) = (vol*‘𝑐))
122117, 121sylan9eqr 2677 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑐 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))) → 𝑧 = (vol*‘𝑐))
123122adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑐 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐)))) → 𝑧 = (vol*‘𝑐))
124 difss2 3723 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) → 𝑐 ran ((,) ∘ 𝑓))
125124ad2antrl 763 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑐 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))) → 𝑐 ran ((,) ∘ 𝑓))
126 ovolsscl 23194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑐 ran ((,) ∘ 𝑓) ∧ ran ((,) ∘ 𝑓) ⊆ ℝ ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘𝑐) ∈ ℝ)
12716, 126mp3an2 1409 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑐 ran ((,) ∘ 𝑓) ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘𝑐) ∈ ℝ)
128127ancoms 469 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ 𝑐 ran ((,) ∘ 𝑓)) → (vol*‘𝑐) ∈ ℝ)
129125, 128sylan2 491 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑐 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐)))) → (vol*‘𝑐) ∈ ℝ)
130123, 129eqeltrd 2698 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑐 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐)))) → 𝑧 ∈ ℝ)
131130rexlimdvaa 3027 . . . . . . . . . . . . . . . . . . . . . . . 24 ((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ → (∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐)) → 𝑧 ∈ ℝ))
132131abssdv 3661 . . . . . . . . . . . . . . . . . . . . . . 23 ((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ → {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))} ⊆ ℝ)
133 eqeq1 2625 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 = 𝑦 → (𝑧 = (vol‘𝑐) ↔ 𝑦 = (vol‘𝑐)))
134133anbi2d 739 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = 𝑦 → ((𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐)) ↔ (𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑦 = (vol‘𝑐))))
135134rexbidv 3047 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 = 𝑦 → (∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐)) ↔ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑦 = (vol‘𝑐))))
136135ralab 3354 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦 ≤ (vol*‘ ran ((,) ∘ 𝑓)) ↔ ∀𝑦(∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑦 = (vol‘𝑐)) → 𝑦 ≤ (vol*‘ ran ((,) ∘ 𝑓))))
137 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑦 = (vol‘𝑐)) → 𝑦 = (vol‘𝑐))
138137, 121sylan9eqr 2677 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑐 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑦 = (vol‘𝑐))) → 𝑦 = (vol*‘𝑐))
139 ovolss 23193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑐 ran ((,) ∘ 𝑓) ∧ ran ((,) ∘ 𝑓) ⊆ ℝ) → (vol*‘𝑐) ≤ (vol*‘ ran ((,) ∘ 𝑓)))
140124, 16, 139sylancl 693 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) → (vol*‘𝑐) ≤ (vol*‘ ran ((,) ∘ 𝑓)))
141140ad2antrl 763 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑐 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑦 = (vol‘𝑐))) → (vol*‘𝑐) ≤ (vol*‘ ran ((,) ∘ 𝑓)))
142138, 141eqbrtrd 4645 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑐 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑦 = (vol‘𝑐))) → 𝑦 ≤ (vol*‘ ran ((,) ∘ 𝑓)))
143142rexlimiva 3023 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑦 = (vol‘𝑐)) → 𝑦 ≤ (vol*‘ ran ((,) ∘ 𝑓)))
144136, 143mpgbir 1723 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦 ≤ (vol*‘ ran ((,) ∘ 𝑓))
14587ralbidv 2982 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = (vol*‘ ran ((,) ∘ 𝑓)) → (∀𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦𝑥 ↔ ∀𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦 ≤ (vol*‘ ran ((,) ∘ 𝑓))))
146145rspcev 3299 . . . . . . . . . . . . . . . . . . . . . . . 24 (((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ ∀𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦 ≤ (vol*‘ ran ((,) ∘ 𝑓))) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦𝑥)
147144, 146mpan2 706 . . . . . . . . . . . . . . . . . . . . . . 23 ((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦𝑥)
148 0ss 3950 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ∅ ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴)
149148, 99pm3.2i 471 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∅ ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 0 = (vol‘∅))
150 sseq1 3611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = ∅ → (𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ↔ ∅ ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴)))
151 fveq2 6158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 = ∅ → (vol‘𝑐) = (vol‘∅))
152151eqeq2d 2631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = ∅ → (0 = (vol‘𝑐) ↔ 0 = (vol‘∅)))
153150, 152anbi12d 746 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 = ∅ → ((𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 0 = (vol‘𝑐)) ↔ (∅ ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 0 = (vol‘∅))))
154153rspcev 3299 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((∅ ∈ (Clsd‘(topGen‘ran (,))) ∧ (∅ ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 0 = (vol‘∅))) → ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 0 = (vol‘𝑐)))
15593, 149, 154mp2an 707 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 0 = (vol‘𝑐))
156 eqeq1 2625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 = 0 → (𝑧 = (vol‘𝑐) ↔ 0 = (vol‘𝑐)))
157156anbi2d 739 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 = 0 → ((𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐)) ↔ (𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 0 = (vol‘𝑐))))
158157rexbidv 3047 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = 0 → (∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐)) ↔ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 0 = (vol‘𝑐))))
159107, 158elab 3338 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))} ↔ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 0 = (vol‘𝑐)))
160155, 159mpbir 221 . . . . . . . . . . . . . . . . . . . . . . . . 25 0 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}
161160ne0ii 3905 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))} ≠ ∅
162 suprcl 10943 . . . . . . . . . . . . . . . . . . . . . . . 24 (({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))} ⊆ ℝ ∧ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦𝑥) → sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < ) ∈ ℝ)
163161, 162mp3an2 1409 . . . . . . . . . . . . . . . . . . . . . . 23 (({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))} ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦𝑥) → sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < ) ∈ ℝ)
164132, 147, 163syl2anc 692 . . . . . . . . . . . . . . . . . . . . . 22 ((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ → sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < ) ∈ ℝ)
165116, 164readdcld 10029 . . . . . . . . . . . . . . . . . . . . 21 ((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ → (sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) + sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < )) ∈ ℝ)
166165adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑤 ran ((,) ∘ 𝑓)) ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → (sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) + sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < )) ∈ ℝ)
167 simpr 477 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑤 ran ((,) ∘ 𝑓)) ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ)
1686ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) ∧ 𝑤 ran ((,) ∘ 𝑓)) ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘(𝑤𝐴)) ∈ ℝ)
1699ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) ∧ 𝑤 ran ((,) ∘ 𝑓)) ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘(𝑤𝐴)) ∈ ℝ)
170 ovolsscl 23194 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((( ran ((,) ∘ 𝑓) ∩ 𝐴) ⊆ ran ((,) ∘ 𝑓) ∧ ran ((,) ∘ 𝑓) ⊆ ℝ ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘( ran ((,) ∘ 𝑓) ∩ 𝐴)) ∈ ℝ)
17164, 16, 170mp3an12 1411 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ → (vol*‘( ran ((,) ∘ 𝑓) ∩ 𝐴)) ∈ ℝ)
172171adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) ∧ 𝑤 ran ((,) ∘ 𝑓)) ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘( ran ((,) ∘ 𝑓) ∩ 𝐴)) ∈ ℝ)
173 difss 3721 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ( ran ((,) ∘ 𝑓) ∖ 𝐴) ⊆ ran ((,) ∘ 𝑓)
174 ovolsscl 23194 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((( ran ((,) ∘ 𝑓) ∖ 𝐴) ⊆ ran ((,) ∘ 𝑓) ∧ ran ((,) ∘ 𝑓) ⊆ ℝ ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘( ran ((,) ∘ 𝑓) ∖ 𝐴)) ∈ ℝ)
175173, 16, 174mp3an12 1411 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ → (vol*‘( ran ((,) ∘ 𝑓) ∖ 𝐴)) ∈ ℝ)
176175adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) ∧ 𝑤 ran ((,) ∘ 𝑓)) ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘( ran ((,) ∘ 𝑓) ∖ 𝐴)) ∈ ℝ)
177 ssrin 3822 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 ran ((,) ∘ 𝑓) → (𝑤𝐴) ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴))
17864, 16sstri 3597 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ( ran ((,) ∘ 𝑓) ∩ 𝐴) ⊆ ℝ
179 ovolss 23193 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑤𝐴) ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ⊆ ℝ) → (vol*‘(𝑤𝐴)) ≤ (vol*‘( ran ((,) ∘ 𝑓) ∩ 𝐴)))
180177, 178, 179sylancl 693 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 ran ((,) ∘ 𝑓) → (vol*‘(𝑤𝐴)) ≤ (vol*‘( ran ((,) ∘ 𝑓) ∩ 𝐴)))
181180ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) ∧ 𝑤 ran ((,) ∘ 𝑓)) ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘(𝑤𝐴)) ≤ (vol*‘( ran ((,) ∘ 𝑓) ∩ 𝐴)))
182 ssdif 3729 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 ran ((,) ∘ 𝑓) → (𝑤𝐴) ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴))
183173, 16sstri 3597 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ( ran ((,) ∘ 𝑓) ∖ 𝐴) ⊆ ℝ
184 ovolss 23193 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑤𝐴) ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ⊆ ℝ) → (vol*‘(𝑤𝐴)) ≤ (vol*‘( ran ((,) ∘ 𝑓) ∖ 𝐴)))
185182, 183, 184sylancl 693 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 ran ((,) ∘ 𝑓) → (vol*‘(𝑤𝐴)) ≤ (vol*‘( ran ((,) ∘ 𝑓) ∖ 𝐴)))
186185ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) ∧ 𝑤 ran ((,) ∘ 𝑓)) ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘(𝑤𝐴)) ≤ (vol*‘( ran ((,) ∘ 𝑓) ∖ 𝐴)))
187168, 169, 172, 176, 181, 186le2addd 10606 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) ∧ 𝑤 ran ((,) ∘ 𝑓)) ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ ((vol*‘( ran ((,) ∘ 𝑓) ∩ 𝐴)) + (vol*‘( ran ((,) ∘ 𝑓) ∖ 𝐴))))
188 dfin4 3849 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( ran ((,) ∘ 𝑓) ∩ 𝐴) = ( ran ((,) ∘ 𝑓) ∖ ( ran ((,) ∘ 𝑓) ∖ 𝐴))
189188fveq2i 6161 . . . . . . . . . . . . . . . . . . . . . . . 24 (vol*‘( ran ((,) ∘ 𝑓) ∩ 𝐴)) = (vol*‘( ran ((,) ∘ 𝑓) ∖ ( ran ((,) ∘ 𝑓) ∖ 𝐴)))
190189oveq1i 6625 . . . . . . . . . . . . . . . . . . . . . . 23 ((vol*‘( ran ((,) ∘ 𝑓) ∩ 𝐴)) + (vol*‘( ran ((,) ∘ 𝑓) ∖ 𝐴))) = ((vol*‘( ran ((,) ∘ 𝑓) ∖ ( ran ((,) ∘ 𝑓) ∖ 𝐴))) + (vol*‘( ran ((,) ∘ 𝑓) ∖ 𝐴)))
191187, 190syl6breq 4664 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) ∧ 𝑤 ran ((,) ∘ 𝑓)) ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ ((vol*‘( ran ((,) ∘ 𝑓) ∖ ( ran ((,) ∘ 𝑓) ∖ 𝐴))) + (vol*‘( ran ((,) ∘ 𝑓) ∖ 𝐴))))
192191adantlll 753 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑤 ran ((,) ∘ 𝑓)) ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ ((vol*‘( ran ((,) ∘ 𝑓) ∖ ( ran ((,) ∘ 𝑓) ∖ 𝐴))) + (vol*‘( ran ((,) ∘ 𝑓) ∖ 𝐴))))
193 simpll 789 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑤 ran ((,) ∘ 𝑓)) → ((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )))
194188sseq2i 3615 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ↔ 𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∖ ( ran ((,) ∘ 𝑓) ∖ 𝐴)))
195194anbi1i 730 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)) ↔ (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∖ ( ran ((,) ∘ 𝑓) ∖ 𝐴)) ∧ 𝑧 = (vol‘𝑎)))
196195rexbii 3036 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)) ↔ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∖ ( ran ((,) ∘ 𝑓) ∖ 𝐴)) ∧ 𝑧 = (vol‘𝑎)))
197196abbii 2736 . . . . . . . . . . . . . . . . . . . . . . . . 25 {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} = {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∖ ( ran ((,) ∘ 𝑓) ∖ 𝐴)) ∧ 𝑧 = (vol‘𝑎))}
198197supeq1i 8313 . . . . . . . . . . . . . . . . . . . . . . . 24 sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) = sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∖ ( ran ((,) ∘ 𝑓) ∖ 𝐴)) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < )
19916jctl 563 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ → ( ran ((,) ∘ 𝑓) ⊆ ℝ ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ))
200199adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → ( ran ((,) ∘ 𝑓) ⊆ ℝ ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ))
201175, 183jctil 559 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ → (( ran ((,) ∘ 𝑓) ∖ 𝐴) ⊆ ℝ ∧ (vol*‘( ran ((,) ∘ 𝑓) ∖ 𝐴)) ∈ ℝ))
202201adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → (( ran ((,) ∘ 𝑓) ∖ 𝐴) ⊆ ℝ ∧ (vol*‘( ran ((,) ∘ 𝑓) ∖ 𝐴)) ∈ ℝ))
203 ltso 10078 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 < Or ℝ
204203a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ → < Or ℝ)
205 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ → (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ)
206 vex 3193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑥 ∈ V
207 eqeq1 2625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 = 𝑥 → (𝑧 = (vol‘𝑐) ↔ 𝑥 = (vol‘𝑐)))
208207anbi2d 739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 = 𝑥 → ((𝑐 ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐)) ↔ (𝑐 ran ((,) ∘ 𝑓) ∧ 𝑥 = (vol‘𝑐))))
209208rexbidv 3047 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧 = 𝑥 → (∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐)) ↔ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ran ((,) ∘ 𝑓) ∧ 𝑥 = (vol‘𝑐))))
210206, 209elab 3338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))} ↔ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ran ((,) ∘ 𝑓) ∧ 𝑥 = (vol‘𝑐)))
21116, 139mpan2 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 ran ((,) ∘ 𝑓) → (vol*‘𝑐) ≤ (vol*‘ ran ((,) ∘ 𝑓)))
212211ad2antrl 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑐 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑐 ran ((,) ∘ 𝑓) ∧ 𝑥 = (vol‘𝑐))) → (vol*‘𝑐) ≤ (vol*‘ ran ((,) ∘ 𝑓)))
21348cldss 20773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑐 ∈ (Clsd‘(topGen‘ran (,))) → 𝑐 ⊆ ℝ)
214 ovolcl 23186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑐 ⊆ ℝ → (vol*‘𝑐) ∈ ℝ*)
215213, 214syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑐 ∈ (Clsd‘(topGen‘ran (,))) → (vol*‘𝑐) ∈ ℝ*)
216 xrlenlt 10063 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((vol*‘𝑐) ∈ ℝ* ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ*) → ((vol*‘𝑐) ≤ (vol*‘ ran ((,) ∘ 𝑓)) ↔ ¬ (vol*‘ ran ((,) ∘ 𝑓)) < (vol*‘𝑐)))
217215, 34, 216sylancl 693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 ∈ (Clsd‘(topGen‘ran (,))) → ((vol*‘𝑐) ≤ (vol*‘ ran ((,) ∘ 𝑓)) ↔ ¬ (vol*‘ ran ((,) ∘ 𝑓)) < (vol*‘𝑐)))
218217adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑐 ran ((,) ∘ 𝑓) ∧ 𝑥 = (vol‘𝑐))) → ((vol*‘𝑐) ≤ (vol*‘ ran ((,) ∘ 𝑓)) ↔ ¬ (vol*‘ ran ((,) ∘ 𝑓)) < (vol*‘𝑐)))
219 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑥 = (vol‘𝑐) → 𝑥 = (vol‘𝑐))
220219, 121sylan9eqr 2677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑐 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑥 = (vol‘𝑐)) → 𝑥 = (vol*‘𝑐))
221 breq2 4627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑥 = (vol*‘𝑐) → ((vol*‘ ran ((,) ∘ 𝑓)) < 𝑥 ↔ (vol*‘ ran ((,) ∘ 𝑓)) < (vol*‘𝑐)))
222221notbid 308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑥 = (vol*‘𝑐) → (¬ (vol*‘ ran ((,) ∘ 𝑓)) < 𝑥 ↔ ¬ (vol*‘ ran ((,) ∘ 𝑓)) < (vol*‘𝑐)))
223220, 222syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑐 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑥 = (vol‘𝑐)) → (¬ (vol*‘ ran ((,) ∘ 𝑓)) < 𝑥 ↔ ¬ (vol*‘ ran ((,) ∘ 𝑓)) < (vol*‘𝑐)))
224223adantrl 751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑐 ran ((,) ∘ 𝑓) ∧ 𝑥 = (vol‘𝑐))) → (¬ (vol*‘ ran ((,) ∘ 𝑓)) < 𝑥 ↔ ¬ (vol*‘ ran ((,) ∘ 𝑓)) < (vol*‘𝑐)))
225218, 224bitr4d 271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑐 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑐 ran ((,) ∘ 𝑓) ∧ 𝑥 = (vol‘𝑐))) → ((vol*‘𝑐) ≤ (vol*‘ ran ((,) ∘ 𝑓)) ↔ ¬ (vol*‘ ran ((,) ∘ 𝑓)) < 𝑥))
226212, 225mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑐 ∈ (Clsd‘(topGen‘ran (,))) ∧ (𝑐 ran ((,) ∘ 𝑓) ∧ 𝑥 = (vol‘𝑐))) → ¬ (vol*‘ ran ((,) ∘ 𝑓)) < 𝑥)
227226rexlimiva 3023 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ran ((,) ∘ 𝑓) ∧ 𝑥 = (vol‘𝑐)) → ¬ (vol*‘ ran ((,) ∘ 𝑓)) < 𝑥)
228210, 227sylbi 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))} → ¬ (vol*‘ ran ((,) ∘ 𝑓)) < 𝑥)
229228adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ 𝑥 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))}) → ¬ (vol*‘ ran ((,) ∘ 𝑓)) < 𝑥)
230 retopbas 22504 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ran (,) ∈ TopBases
231 bastg 20710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (ran (,) ∈ TopBases → ran (,) ⊆ (topGen‘ran (,)))
232230, 231ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ran (,) ⊆ (topGen‘ran (,))
23313, 232sstri 3597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ran ((,) ∘ 𝑓) ⊆ (topGen‘ran (,))
234 uniopn 20642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((topGen‘ran (,)) ∈ Top ∧ ran ((,) ∘ 𝑓) ⊆ (topGen‘ran (,))) → ran ((,) ∘ 𝑓) ∈ (topGen‘ran (,)))
23591, 233, 234mp2an 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ran ((,) ∘ 𝑓) ∈ (topGen‘ran (,))
236 mblfinlem2 33118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (( ran ((,) ∘ 𝑓) ∈ (topGen‘ran (,)) ∧ 𝑥 ∈ ℝ ∧ 𝑥 < (vol*‘ ran ((,) ∘ 𝑓))) → ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ran ((,) ∘ 𝑓) ∧ 𝑥 < (vol*‘𝑐)))
237235, 236mp3an1 1408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑥 ∈ ℝ ∧ 𝑥 < (vol*‘ ran ((,) ∘ 𝑓))) → ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ran ((,) ∘ 𝑓) ∧ 𝑥 < (vol*‘𝑐)))
238121eqcomd 2627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑐 ∈ (Clsd‘(topGen‘ran (,))) → (vol*‘𝑐) = (vol‘𝑐))
239238anim1i 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑐 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑥 < (vol*‘𝑐)) → ((vol*‘𝑐) = (vol‘𝑐) ∧ 𝑥 < (vol*‘𝑐)))
240239ex 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 ∈ (Clsd‘(topGen‘ran (,))) → (𝑥 < (vol*‘𝑐) → ((vol*‘𝑐) = (vol‘𝑐) ∧ 𝑥 < (vol*‘𝑐))))
241240anim2d 588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 ∈ (Clsd‘(topGen‘ran (,))) → ((𝑐 ran ((,) ∘ 𝑓) ∧ 𝑥 < (vol*‘𝑐)) → (𝑐 ran ((,) ∘ 𝑓) ∧ ((vol*‘𝑐) = (vol‘𝑐) ∧ 𝑥 < (vol*‘𝑐)))))
242 fvex 6168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (vol*‘𝑐) ∈ V
243 eqeq1 2625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑦 = (vol*‘𝑐) → (𝑦 = (vol‘𝑐) ↔ (vol*‘𝑐) = (vol‘𝑐)))
244243anbi2d 739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 = (vol*‘𝑐) → ((𝑐 ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ↔ (𝑐 ran ((,) ∘ 𝑓) ∧ (vol*‘𝑐) = (vol‘𝑐))))
245 breq2 4627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 = (vol*‘𝑐) → (𝑥 < 𝑦𝑥 < (vol*‘𝑐)))
246244, 245anbi12d 746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 = (vol*‘𝑐) → (((𝑐 ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦) ↔ ((𝑐 ran ((,) ∘ 𝑓) ∧ (vol*‘𝑐) = (vol‘𝑐)) ∧ 𝑥 < (vol*‘𝑐))))
247242, 246spcev 3290 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑐 ran ((,) ∘ 𝑓) ∧ (vol*‘𝑐) = (vol‘𝑐)) ∧ 𝑥 < (vol*‘𝑐)) → ∃𝑦((𝑐 ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦))
248247anasss 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 ran ((,) ∘ 𝑓) ∧ ((vol*‘𝑐) = (vol‘𝑐) ∧ 𝑥 < (vol*‘𝑐))) → ∃𝑦((𝑐 ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦))
249241, 248syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 ∈ (Clsd‘(topGen‘ran (,))) → ((𝑐 ran ((,) ∘ 𝑓) ∧ 𝑥 < (vol*‘𝑐)) → ∃𝑦((𝑐 ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦)))
250249reximia 3005 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ran ((,) ∘ 𝑓) ∧ 𝑥 < (vol*‘𝑐)) → ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))∃𝑦((𝑐 ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦))
251237, 250syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑥 ∈ ℝ ∧ 𝑥 < (vol*‘ ran ((,) ∘ 𝑓))) → ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))∃𝑦((𝑐 ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦))
252 r19.41v 3083 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))((𝑐 ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦) ↔ (∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦))
253252exbii 1771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∃𝑦𝑐 ∈ (Clsd‘(topGen‘ran (,)))((𝑐 ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦) ↔ ∃𝑦(∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦))
254 rexcom4 3215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))∃𝑦((𝑐 ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦) ↔ ∃𝑦𝑐 ∈ (Clsd‘(topGen‘ran (,)))((𝑐 ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦))
255133anbi2d 739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 = 𝑦 → ((𝑐 ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐)) ↔ (𝑐 ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐))))
256255rexbidv 3047 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 = 𝑦 → (∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐)) ↔ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐))))
257256rexab 3356 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∃𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))}𝑥 < 𝑦 ↔ ∃𝑦(∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦))
258253, 254, 2573bitr4i 292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))∃𝑦((𝑐 ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦) ↔ ∃𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))}𝑥 < 𝑦)
259251, 258sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑥 ∈ ℝ ∧ 𝑥 < (vol*‘ ran ((,) ∘ 𝑓))) → ∃𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))}𝑥 < 𝑦)
260259adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (vol*‘ ran ((,) ∘ 𝑓)))) → ∃𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))}𝑥 < 𝑦)
261204, 205, 229, 260eqsupd 8323 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ → sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < ) = (vol*‘ ran ((,) ∘ 𝑓)))
262261eqcomd 2627 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ → (vol*‘ ran ((,) ∘ 𝑓)) = sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < ))
263262adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘ ran ((,) ∘ 𝑓)) = sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < ))
264 sseq1 3611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 = 𝑎 → (𝑐 ran ((,) ∘ 𝑓) ↔ 𝑎 ran ((,) ∘ 𝑓)))
265 fveq2 6158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑐 = 𝑎 → (vol‘𝑐) = (vol‘𝑎))
266265eqeq2d 2631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 = 𝑎 → (𝑧 = (vol‘𝑐) ↔ 𝑧 = (vol‘𝑎)))
267264, 266anbi12d 746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = 𝑎 → ((𝑐 ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐)) ↔ (𝑎 ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑎))))
268267cbvrexv 3164 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐)) ↔ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑎)))
269268abbii 2736 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))} = {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑎))}
270269supeq1i 8313 . . . . . . . . . . . . . . . . . . . . . . . . . 26 sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < ) = sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < )
271263, 270syl6eq 2671 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘ ran ((,) ∘ 𝑓)) = sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ))
272 sseq1 3611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 = 𝑎 → (𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ↔ 𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴)))
273272, 266anbi12d 746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = 𝑎 → ((𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐)) ↔ (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑎))))
274273cbvrexv 3164 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐)) ↔ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑎)))
275274abbii 2736 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))} = {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑎))}
276275supeq1i 8313 . . . . . . . . . . . . . . . . . . . . . . . . . 26 sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < ) = sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < )
277 simpll 789 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ))
278 eqeq1 2625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = 𝑧 → (𝑦 = (vol‘𝑏) ↔ 𝑧 = (vol‘𝑏)))
279278anbi2d 739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = 𝑧 → ((𝑏𝐴𝑦 = (vol‘𝑏)) ↔ (𝑏𝐴𝑧 = (vol‘𝑏))))
280279rexbidv 3047 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = 𝑧 → (∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏)) ↔ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑧 = (vol‘𝑏))))
281 sseq1 3611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑏 = 𝑐 → (𝑏𝐴𝑐𝐴))
282 fveq2 6158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑏 = 𝑐 → (vol‘𝑏) = (vol‘𝑐))
283282eqeq2d 2631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑏 = 𝑐 → (𝑧 = (vol‘𝑏) ↔ 𝑧 = (vol‘𝑐)))
284281, 283anbi12d 746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑏 = 𝑐 → ((𝑏𝐴𝑧 = (vol‘𝑏)) ↔ (𝑐𝐴𝑧 = (vol‘𝑐))))
285284cbvrexv 3164 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑧 = (vol‘𝑏)) ↔ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐𝐴𝑧 = (vol‘𝑐)))
286280, 285syl6bb 276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = 𝑧 → (∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏)) ↔ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐𝐴𝑧 = (vol‘𝑐))))
287286cbvabv 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 {𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))} = {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐𝐴𝑧 = (vol‘𝑐))}
288287supeq1i 8313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < ) = sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐𝐴𝑧 = (vol‘𝑐))}, ℝ, < )
289288eqeq2i 2633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < ) ↔ (vol*‘𝐴) = sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐𝐴𝑧 = (vol‘𝑐))}, ℝ, < ))
290289biimpi 206 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < ) → (vol*‘𝐴) = sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐𝐴𝑧 = (vol‘𝑐))}, ℝ, < ))
291290ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘𝐴) = sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐𝐴𝑧 = (vol‘𝑐))}, ℝ, < ))
292 mblfinlem3 33119 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ((,) ∘ 𝑓) ∖ 𝐴)))
293200, 277, 263, 291, 292syl112anc 1327 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < ) = (vol*‘( ran ((,) ∘ 𝑓) ∖ 𝐴)))
294276, 293syl5reqr 2670 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘( ran ((,) ∘ 𝑓) ∖ 𝐴)) = sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ))
295 mblfinlem3 33119 . . . . . . . . . . . . . . . . . . . . . . . . 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 ((,) ∘ 𝑓) ∖ 𝐴))))
296200, 202, 271, 294, 295syl112anc 1327 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∖ ( ran ((,) ∘ 𝑓) ∖ 𝐴)) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) = (vol*‘( ran ((,) ∘ 𝑓) ∖ ( ran ((,) ∘ 𝑓) ∖ 𝐴))))
297198, 296syl5eq 2667 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) = (vol*‘( ran ((,) ∘ 𝑓) ∖ ( ran ((,) ∘ 𝑓) ∖ 𝐴))))
298297, 293oveq12d 6633 . . . . . . . . . . . . . . . . . . . . . 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 ((,) ∘ 𝑓) ∖ 𝐴))))
299193, 298sylan 488 . . . . . . . . . . . . . . . . . . . . 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 ((,) ∘ 𝑓) ∖ 𝐴))))
300192, 299breqtrrd 4651 . . . . . . . . . . . . . . . . . . . 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‘𝑐))}, ℝ, < )))
301 ne0i 3903 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} → {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ≠ ∅)
302112, 301mp1i 13 . . . . . . . . . . . . . . . . . . . . . . 23 ((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ → {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ≠ ∅)
303 ne0i 3903 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))} → {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))} ≠ ∅)
304160, 303mp1i 13 . . . . . . . . . . . . . . . . . . . . . . 23 ((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ → {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))} ≠ ∅)
305 eqid 2621 . . . . . . . . . . . . . . . . . . . . . . 23 {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)} = {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)}
30674, 302, 90, 132, 304, 147, 305supadd 10951 . . . . . . . . . . . . . . . . . . . . . 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‘𝑐))}𝑡 = (𝑢 + 𝑣)}, ℝ, < ))
307 reeanv 3101 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))((𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑢 = (vol‘𝑎)) ∧ (𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑣 = (vol‘𝑐))) ↔ (∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑢 = (vol‘𝑎)) ∧ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑣 = (vol‘𝑐))))
308 vex 3193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑢 ∈ V
309 eqeq1 2625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧 = 𝑢 → (𝑧 = (vol‘𝑎) ↔ 𝑢 = (vol‘𝑎)))
310309anbi2d 739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 = 𝑢 → ((𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)) ↔ (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑢 = (vol‘𝑎))))
311310rexbidv 3047 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 = 𝑢 → (∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)) ↔ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑢 = (vol‘𝑎))))
312308, 311elab 3338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ↔ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑢 = (vol‘𝑎)))
313 vex 3193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑣 ∈ V
314 eqeq1 2625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧 = 𝑣 → (𝑧 = (vol‘𝑐) ↔ 𝑣 = (vol‘𝑐)))
315314anbi2d 739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 = 𝑣 → ((𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐)) ↔ (𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑣 = (vol‘𝑐))))
316315rexbidv 3047 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 = 𝑣 → (∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐)) ↔ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑣 = (vol‘𝑐))))
317313, 316elab 3338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))} ↔ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑣 = (vol‘𝑐)))
318312, 317anbi12i 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}) ↔ (∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑢 = (vol‘𝑎)) ∧ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑣 = (vol‘𝑐))))
319307, 318bitr4i 267 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))((𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑢 = (vol‘𝑎)) ∧ (𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑣 = (vol‘𝑐))) ↔ (𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}))
320 an4 864 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴)) ∧ (𝑢 = (vol‘𝑎) ∧ 𝑣 = (vol‘𝑐))) ↔ ((𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑢 = (vol‘𝑎)) ∧ (𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑣 = (vol‘𝑐))))
321 oveq12 6624 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑢 = (vol‘𝑎) ∧ 𝑣 = (vol‘𝑐)) → (𝑢 + 𝑣) = ((vol‘𝑎) + (vol‘𝑐)))
32259adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,)))) → 𝑎 ∈ dom vol)
323322ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴))) → 𝑎 ∈ dom vol)
324119adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,)))) → 𝑐 ∈ dom vol)
325324ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴))) → 𝑐 ∈ dom vol)
326 ss2in 3824 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴)) → (𝑎𝑐) ⊆ (( ran ((,) ∘ 𝑓) ∩ 𝐴) ∩ ( ran ((,) ∘ 𝑓) ∖ 𝐴)))
327188ineq1i 3794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (( ran ((,) ∘ 𝑓) ∩ 𝐴) ∩ ( ran ((,) ∘ 𝑓) ∖ 𝐴)) = (( ran ((,) ∘ 𝑓) ∖ ( ran ((,) ∘ 𝑓) ∖ 𝐴)) ∩ ( ran ((,) ∘ 𝑓) ∖ 𝐴))
328 incom 3789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (( ran ((,) ∘ 𝑓) ∖ ( ran ((,) ∘ 𝑓) ∖ 𝐴)) ∩ ( ran ((,) ∘ 𝑓) ∖ 𝐴)) = (( ran ((,) ∘ 𝑓) ∖ 𝐴) ∩ ( ran ((,) ∘ 𝑓) ∖ ( ran ((,) ∘ 𝑓) ∖ 𝐴)))
329 disjdif 4018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (( ran ((,) ∘ 𝑓) ∖ 𝐴) ∩ ( ran ((,) ∘ 𝑓) ∖ ( ran ((,) ∘ 𝑓) ∖ 𝐴))) = ∅
330327, 328, 3293eqtri 2647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (( ran ((,) ∘ 𝑓) ∩ 𝐴) ∩ ( ran ((,) ∘ 𝑓) ∖ 𝐴)) = ∅
331326, 330syl6sseq 3636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴)) → (𝑎𝑐) ⊆ ∅)
332 ss0 3952 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑎𝑐) ⊆ ∅ → (𝑎𝑐) = ∅)
333331, 332syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴)) → (𝑎𝑐) = ∅)
334333adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴))) → (𝑎𝑐) = ∅)
33561adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,)))) → (vol‘𝑎) = (vol*‘𝑎))
336335ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴))) → (vol‘𝑎) = (vol*‘𝑎))
33766, 16jctir 560 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) → (𝑎 ran ((,) ∘ 𝑓) ∧ ran ((,) ∘ 𝑓) ⊆ ℝ))
338683expa 1262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑎 ran ((,) ∘ 𝑓) ∧ ran ((,) ∘ 𝑓) ⊆ ℝ) ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘𝑎) ∈ ℝ)
339337, 338sylan 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘𝑎) ∈ ℝ)
340339ancoms 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ 𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴)) → (vol*‘𝑎) ∈ ℝ)
341340ad2ant2r 782 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴))) → (vol*‘𝑎) ∈ ℝ)
342336, 341eqeltrd 2698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴))) → (vol‘𝑎) ∈ ℝ)
343121adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,)))) → (vol‘𝑐) = (vol*‘𝑐))
344343ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴))) → (vol‘𝑐) = (vol*‘𝑐))
345124, 16jctir 560 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) → (𝑐 ran ((,) ∘ 𝑓) ∧ ran ((,) ∘ 𝑓) ⊆ ℝ))
3461263expa 1262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑐 ran ((,) ∘ 𝑓) ∧ ran ((,) ∘ 𝑓) ⊆ ℝ) ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘𝑐) ∈ ℝ)
347345, 346sylan 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘𝑐) ∈ ℝ)
348347ancoms 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ 𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴)) → (vol*‘𝑐) ∈ ℝ)
349348ad2ant2rl 784 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴))) → (vol*‘𝑐) ∈ ℝ)
350344, 349eqeltrd 2698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴))) → (vol‘𝑐) ∈ ℝ)
351 volun 23253 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝑎 ∈ dom vol ∧ 𝑐 ∈ dom vol ∧ (𝑎𝑐) = ∅) ∧ ((vol‘𝑎) ∈ ℝ ∧ (vol‘𝑐) ∈ ℝ)) → (vol‘(𝑎𝑐)) = ((vol‘𝑎) + (vol‘𝑐)))
352323, 325, 334, 342, 350, 351syl32anc 1331 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴))) → (vol‘(𝑎𝑐)) = ((vol‘𝑎) + (vol‘𝑐)))
353 unmbl 23245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑎 ∈ dom vol ∧ 𝑐 ∈ dom vol) → (𝑎𝑐) ∈ dom vol)
35459, 119, 353syl2an 494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,)))) → (𝑎𝑐) ∈ dom vol)
355 mblvol 23238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑎𝑐) ∈ dom vol → (vol‘(𝑎𝑐)) = (vol*‘(𝑎𝑐)))
356354, 355syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,)))) → (vol‘(𝑎𝑐)) = (vol*‘(𝑎𝑐)))
357356ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴))) → (vol‘(𝑎𝑐)) = (vol*‘(𝑎𝑐)))
358352, 357eqtr3d 2657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴))) → ((vol‘𝑎) + (vol‘𝑐)) = (vol*‘(𝑎𝑐)))
359321, 358sylan9eqr 2677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴))) ∧ (𝑢 = (vol‘𝑎) ∧ 𝑣 = (vol‘𝑐))) → (𝑢 + 𝑣) = (vol*‘(𝑎𝑐)))
360 eqtr 2640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑦 = (𝑢 + 𝑣) ∧ (𝑢 + 𝑣) = (vol*‘(𝑎𝑐))) → 𝑦 = (vol*‘(𝑎𝑐)))
361360ancoms 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑢 + 𝑣) = (vol*‘(𝑎𝑐)) ∧ 𝑦 = (𝑢 + 𝑣)) → 𝑦 = (vol*‘(𝑎𝑐)))
362359, 361sylan 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴))) ∧ (𝑢 = (vol‘𝑎) ∧ 𝑣 = (vol‘𝑐))) ∧ 𝑦 = (𝑢 + 𝑣)) → 𝑦 = (vol*‘(𝑎𝑐)))
36366, 124anim12i 589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴)) → (𝑎 ran ((,) ∘ 𝑓) ∧ 𝑐 ran ((,) ∘ 𝑓)))
364 unss 3771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑎 ran ((,) ∘ 𝑓) ∧ 𝑐 ran ((,) ∘ 𝑓)) ↔ (𝑎𝑐) ⊆ ran ((,) ∘ 𝑓))
365363, 364sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴)) → (𝑎𝑐) ⊆ ran ((,) ∘ 𝑓))
366 ovolss 23193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑎𝑐) ⊆ ran ((,) ∘ 𝑓) ∧ ran ((,) ∘ 𝑓) ⊆ ℝ) → (vol*‘(𝑎𝑐)) ≤ (vol*‘ ran ((,) ∘ 𝑓)))
367365, 16, 366sylancl 693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴)) → (vol*‘(𝑎𝑐)) ≤ (vol*‘ ran ((,) ∘ 𝑓)))
368367ad3antlr 766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴))) ∧ (𝑢 = (vol‘𝑎) ∧ 𝑣 = (vol‘𝑐))) ∧ 𝑦 = (𝑢 + 𝑣)) → (vol*‘(𝑎𝑐)) ≤ (vol*‘ ran ((,) ∘ 𝑓)))
369362, 368eqbrtrd 4645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴))) ∧ (𝑢 = (vol‘𝑎) ∧ 𝑣 = (vol‘𝑐))) ∧ 𝑦 = (𝑢 + 𝑣)) → 𝑦 ≤ (vol*‘ ran ((,) ∘ 𝑓)))
370369ex 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) ∧ (𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴))) ∧ (𝑢 = (vol‘𝑎) ∧ 𝑣 = (vol‘𝑐))) → (𝑦 = (𝑢 + 𝑣) → 𝑦 ≤ (vol*‘ ran ((,) ∘ 𝑓))))
371370expl 647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) → (((𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴)) ∧ (𝑢 = (vol‘𝑎) ∧ 𝑣 = (vol‘𝑐))) → (𝑦 = (𝑢 + 𝑣) → 𝑦 ≤ (vol*‘ ran ((,) ∘ 𝑓)))))
372320, 371syl5bir 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈ (Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))) → (((𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑢 = (vol‘𝑎)) ∧ (𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑣 = (vol‘𝑐))) → (𝑦 = (𝑢 + 𝑣) → 𝑦 ≤ (vol*‘ ran ((,) ∘ 𝑓)))))
373372rexlimdvva 3033 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ → (∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))((𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑢 = (vol‘𝑎)) ∧ (𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑣 = (vol‘𝑐))) → (𝑦 = (𝑢 + 𝑣) → 𝑦 ≤ (vol*‘ ran ((,) ∘ 𝑓)))))
374319, 373syl5bir 233 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ → ((𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}) → (𝑦 = (𝑢 + 𝑣) → 𝑦 ≤ (vol*‘ ran ((,) ∘ 𝑓)))))
375374rexlimdvv 3032 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ → (∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦 = (𝑢 + 𝑣) → 𝑦 ≤ (vol*‘ ran ((,) ∘ 𝑓))))
376375alrimiv 1852 . . . . . . . . . . . . . . . . . . . . . . . 24 ((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ → ∀𝑦(∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦 = (𝑢 + 𝑣) → 𝑦 ≤ (vol*‘ ran ((,) ∘ 𝑓))))
377 eqeq1 2625 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = 𝑦 → (𝑡 = (𝑢 + 𝑣) ↔ 𝑦 = (𝑢 + 𝑣)))
3783772rexbidv 3052 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑦 → (∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣) ↔ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦 = (𝑢 + 𝑣)))
379378ralab 3354 . . . . . . . . . . . . . . . . . . . . . . . 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 ((,) ∘ 𝑓))))
380376, 379sylibr 224 . . . . . . . . . . . . . . . . . . . . . . 23 ((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ → ∀𝑦 ∈ {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)}𝑦 ≤ (vol*‘ ran ((,) ∘ 𝑓)))
381 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))})) ∧ 𝑡 = (𝑢 + 𝑣)) → 𝑡 = (𝑢 + 𝑣))
38274sselda 3588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ 𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}) → 𝑢 ∈ ℝ)
383132sselda 3588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}) → 𝑣 ∈ ℝ)
384 readdcl 9979 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → (𝑢 + 𝑣) ∈ ℝ)
385382, 383, 384syl2an 494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ 𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}) ∧ ((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))})) → (𝑢 + 𝑣) ∈ ℝ)
386385anandis 872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))})) → (𝑢 + 𝑣) ∈ ℝ)
387386adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))})) ∧ 𝑡 = (𝑢 + 𝑣)) → (𝑢 + 𝑣) ∈ ℝ)
388381, 387eqeltrd 2698 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))})) ∧ 𝑡 = (𝑢 + 𝑣)) → 𝑡 ∈ ℝ)
389388ex 450 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))})) → (𝑡 = (𝑢 + 𝑣) → 𝑡 ∈ ℝ))
390389rexlimdvva 3033 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ → (∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣) → 𝑡 ∈ ℝ))
391390abssdv 3661 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ → {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)} ⊆ ℝ)
392 00id 10171 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (0 + 0) = 0
393392eqcomi 2630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 0 = (0 + 0)
394 rspceov 6657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 = (𝑢 + 𝑣))
395112, 160, 393, 394mp3an 1421 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}0 = (𝑢 + 𝑣)
396 eqeq1 2625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑡 = 0 → (𝑡 = (𝑢 + 𝑣) ↔ 0 = (𝑢 + 𝑣)))
3973962rexbidv 3052 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑡 = 0 → (∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣) ↔ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}0 = (𝑢 + 𝑣)))
398107, 397spcev 3290 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}0 = (𝑢 + 𝑣) → ∃𝑡𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣))
399395, 398ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑡𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)
400 abn0 3934 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)} ≠ ∅ ↔ ∃𝑡𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣))
401399, 400mpbir 221 . . . . . . . . . . . . . . . . . . . . . . . . . 26 {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)} ≠ ∅
402401a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ → {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)} ≠ ∅)
40387ralbidv 2982 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = (vol*‘ ran ((,) ∘ 𝑓)) → (∀𝑦 ∈ {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)}𝑦𝑥 ↔ ∀𝑦 ∈ {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)}𝑦 ≤ (vol*‘ ran ((,) ∘ 𝑓))))
404403rspcev 3299 . . . . . . . . . . . . . . . . . . . . . . . . . 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‘𝑐))}𝑡 = (𝑢 + 𝑣)}𝑦𝑥)
405380, 404mpdan 701 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)}𝑦𝑥)
406391, 402, 4053jca 1240 . . . . . . . . . . . . . . . . . . . . . . . 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‘𝑐))}𝑡 = (𝑢 + 𝑣)}𝑦𝑥))
407 suprleub 10949 . . . . . . . . . . . . . . . . . . . . . . . 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 ((,) ∘ 𝑓))))
408406, 407mpancom 702 . . . . . . . . . . . . . . . . . . . . . . 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 ((,) ∘ 𝑓))))
409380, 408mpbird 247 . . . . . . . . . . . . . . . . . . . . . 22 ((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ → sup({𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)}, ℝ, < ) ≤ (vol*‘ ran ((,) ∘ 𝑓)))
410306, 409eqbrtrd 4645 . . . . . . . . . . . . . . . . . . . . 21 ((vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ → (sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ( ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) + sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ( ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < )) ≤ (vol*‘ ran ((,) ∘ 𝑓)))
411410adantl 482 . . . . . . . . . . . . . . . . . . . 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 ((,) ∘ 𝑓)))
41245, 166, 167, 300, 411letrd 10154 . . . . . . . . . . . . . . . . . . 19 ((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑤 ran ((,) ∘ 𝑓)) ∧ (vol*‘ ran ((,) ∘ 𝑓)) ∈ ℝ) → ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ (vol*‘ ran ((,) ∘ 𝑓)))
41344, 412sylan2 491 . . . . . . . . . . . . . . . . . 18 ((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑤 ran ((,) ∘ 𝑓)) ∧ (vol*‘ ran ((,) ∘ 𝑓)) ≠ +∞) → ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ (vol*‘ ran ((,) ∘ 𝑓)))
41433, 413pm2.61dane 2877 . . . . . . . . . . . . . . . . 17 (((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑤 ran ((,) ∘ 𝑓)) → ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ (vol*‘ ran ((,) ∘ 𝑓)))
415414adantlr 750 . . . . . . . . . . . . . . . 16 ((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑓:ℕ⟶( ≤ ∩ (ℝ × ℝ))) ∧ 𝑤 ran ((,) ∘ 𝑓)) → ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ (vol*‘ ran ((,) ∘ 𝑓)))
416 ssid 3609 . . . . . . . . . . . . . . . . . 18 ran ((,) ∘ 𝑓) ⊆ ran ((,) ∘ 𝑓)
41720ovollb 23187 . . . . . . . . . . . . . . . . . 18 ((𝑓:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ran ((,) ∘ 𝑓) ⊆ ran ((,) ∘ 𝑓)) → (vol*‘ ran ((,) ∘ 𝑓)) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))
418416, 417mpan2 706 . . . . . . . . . . . . . . . . 17 (𝑓:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → (vol*‘ ran ((,) ∘ 𝑓)) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))
419418ad2antlr 762 . . . . . . . . . . . . . . . 16 ((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑓:ℕ⟶( ≤ ∩ (ℝ × ℝ))) ∧ 𝑤 ran ((,) ∘ 𝑓)) → (vol*‘ ran ((,) ∘ 𝑓)) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))
42012, 18, 27, 415, 419xrletrd 11953 . . . . . . . . . . . . . . 15 ((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑓:ℕ⟶( ≤ ∩ (ℝ × ℝ))) ∧ 𝑤 ran ((,) ∘ 𝑓)) → ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))
421420adantr 481 . . . . . . . . . . . . . 14 (((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑓:ℕ⟶( ≤ ∩ (ℝ × ℝ))) ∧ 𝑤 ran ((,) ∘ 𝑓)) ∧ 𝑢 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < )) → ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))
422 simpr 477 . . . . . . . . . . . . . 14 (((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑓:ℕ⟶( ≤ ∩ (ℝ × ℝ))) ∧ 𝑤 ran ((,) ∘ 𝑓)) ∧ 𝑢 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < )) → 𝑢 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))
423421, 422breqtrrd 4651 . . . . . . . . . . . . 13 (((((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑓:ℕ⟶( ≤ ∩ (ℝ × ℝ))) ∧ 𝑤 ran ((,) ∘ 𝑓)) ∧ 𝑢 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < )) → ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ 𝑢)
424423expl 647 . . . . . . . . . . . 12 (((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑓:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → ((𝑤 ran ((,) ∘ 𝑓) ∧ 𝑢 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < )) → ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ 𝑢))
4253, 424sylan2 491 . . . . . . . . . . 11 (((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) ∧ 𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)) → ((𝑤 ran ((,) ∘ 𝑓) ∧ 𝑢 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < )) → ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ 𝑢))
426425rexlimdva 3026 . . . . . . . . . 10 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) → (∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑤 ran ((,) ∘ 𝑓) ∧ 𝑢 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < )) → ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ 𝑢))
427426ralrimivw 2963 . . . . . . . . 9 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) → ∀𝑢 ∈ ℝ* (∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑤 ran ((,) ∘ 𝑓) ∧ 𝑢 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < )) → ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ 𝑢))
428 eqeq1 2625 . . . . . . . . . . . 12 (𝑣 = 𝑢 → (𝑣 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ↔ 𝑢 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < )))
429428anbi2d 739 . . . . . . . . . . 11 (𝑣 = 𝑢 → ((𝑤 ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < )) ↔ (𝑤 ran ((,) ∘ 𝑓) ∧ 𝑢 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))))
430429rexbidv 3047 . . . . . . . . . 10 (𝑣 = 𝑢 → (∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑤 ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < )) ↔ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑤 ran ((,) ∘ 𝑓) ∧ 𝑢 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))))
431430ralrab 3355 . . . . . . . . 9 (∀𝑢 ∈ {𝑣 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑤 ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ 𝑢 ↔ ∀𝑢 ∈ ℝ* (∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑤 ran ((,) ∘ 𝑓) ∧ 𝑢 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < )) → ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ 𝑢))
432427, 431sylibr 224 . . . . . . . 8 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) → ∀𝑢 ∈ {𝑣 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑤 ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ 𝑢)
433 ssrab2 3672 . . . . . . . . 9 {𝑣 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑤 ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} ⊆ ℝ*
43411adantl 482 . . . . . . . . 9 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) → ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ∈ ℝ*)
435 infxrgelb 12124 . . . . . . . . 9 (({𝑣 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑤 ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} ⊆ ℝ* ∧ ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ∈ ℝ*) → (((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ inf({𝑣 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑤 ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}, ℝ*, < ) ↔ ∀𝑢 ∈ {𝑣 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑤 ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ 𝑢))
436433, 434, 435sylancr 694 . . . . . . . 8 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) → (((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ inf({𝑣 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑤 ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}, ℝ*, < ) ↔ ∀𝑢 ∈ {𝑣 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑤 ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ 𝑢))
437432, 436mpbird 247 . . . . . . 7 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) → ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ inf({𝑣 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑤 ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}, ℝ*, < ))
438 eqid 2621 . . . . . . . . 9 {𝑣 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑤 ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} = {𝑣 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑤 ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}
439438ovolval 23182 . . . . . . . 8 (𝑤 ⊆ ℝ → (vol*‘𝑤) = inf({𝑣 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑤 ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}, ℝ*, < ))
440439ad2antrl 763 . . . . . . 7 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) → (vol*‘𝑤) = inf({𝑣 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑤 ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}, ℝ*, < ))
441437, 440breqtrrd 4651 . . . . . 6 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ)) → ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ (vol*‘𝑤))
442441expr 642 . . . . 5 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ 𝑤 ⊆ ℝ) → ((vol*‘𝑤) ∈ ℝ → ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ (vol*‘𝑤)))
4432, 442sylan2 491 . . . 4 ((((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ 𝑤 ∈ 𝒫 ℝ) → ((vol*‘𝑤) ∈ ℝ → ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ (vol*‘𝑤)))
444443ralrimiva 2962 . . 3 (((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) → ∀𝑤 ∈ 𝒫 ℝ((vol*‘𝑤) ∈ ℝ → ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ (vol*‘𝑤)))
445 ismbl2 23235 . . . . 5 (𝐴 ∈ dom vol ↔ (𝐴 ⊆ ℝ ∧ ∀𝑤 ∈ 𝒫 ℝ((vol*‘𝑤) ∈ ℝ → ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ (vol*‘𝑤))))
446445baibr 944 . . . 4 (𝐴 ⊆ ℝ → (∀𝑤 ∈ 𝒫 ℝ((vol*‘𝑤) ∈ ℝ → ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ (vol*‘𝑤)) ↔ 𝐴 ∈ dom vol))
447446ad2antrr 761 . . 3 (((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) → (∀𝑤 ∈ 𝒫 ℝ((vol*‘𝑤) ∈ ℝ → ((vol*‘(𝑤𝐴)) + (vol*‘(𝑤𝐴))) ≤ (vol*‘𝑤)) ↔ 𝐴 ∈ dom vol))
448444, 447mpbid 222 . 2 (((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )) → 𝐴 ∈ dom vol)
4491, 448impbida 876 1 ((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) → (𝐴 ∈ dom vol ↔ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1036  wal 1478   = wceq 1480  wex 1701  wcel 1987  {cab 2607  wne 2790  wral 2908  wrex 2909  {crab 2912  cdif 3557  cun 3558  cin 3559  wss 3560  c0 3897  𝒫 cpw 4136   cuni 4409   class class class wbr 4623   Or wor 5004   × cxp 5082  dom cdm 5084  ran crn 5085  ccom 5088  wf 5853  cfv 5857  (class class class)co 6615  𝑚 cmap 7817  supcsup 8306  infcinf 8307  cr 9895  0cc0 9896  1c1 9897   + caddc 9899  +∞cpnf 10031  *cxr 10033   < clt 10034  cle 10035  cmin 10226  cn 10980  (,)cioo 12133  [,)cico 12135  seqcseq 12757  abscabs 13924  topGenctg 16038  Topctop 20638  TopBasesctb 20689  Clsdccld 20760  vol*covol 23171  volcvol 23172
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914  ax-inf2 8498  ax-cnex 9952  ax-resscn 9953  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-addrcl 9957  ax-mulcl 9958  ax-mulrcl 9959  ax-mulcom 9960  ax-addass 9961  ax-mulass 9962  ax-distr 9963  ax-i2m1 9964  ax-1ne0 9965  ax-1rid 9966  ax-rnegex 9967  ax-rrecex 9968  ax-cnre 9969  ax-pre-lttri 9970  ax-pre-lttrn 9971  ax-pre-ltadd 9972  ax-pre-mulgt0 9973  ax-pre-sup 9974
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2913  df-rex 2914  df-reu 2915  df-rmo 2916  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-int 4448  df-iun 4494  df-iin 4495  df-disj 4594  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-se 5044  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-isom 5866  df-riota 6576  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-of 6862  df-om 7028  df-1st 7128  df-2nd 7129  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-1o 7520  df-2o 7521  df-oadd 7524  df-omul 7525  df-er 7702  df-map 7819  df-pm 7820  df-en 7916  df-dom 7917  df-sdom 7918  df-fin 7919  df-fi 8277  df-sup 8308  df-inf 8309  df-oi 8375  df-card 8725  df-acn 8728  df-cda 8950  df-pnf 10036  df-mnf 10037  df-xr 10038  df-ltxr 10039  df-le 10040  df-sub 10228  df-neg 10229  df-div 10645  df-nn 10981  df-2 11039  df-3 11040  df-4 11041  df-n0 11253  df-z 11338  df-uz 11648  df-q 11749  df-rp 11793  df-xneg 11906  df-xadd 11907  df-xmul 11908  df-ioo 12137  df-ico 12139  df-icc 12140  df-fz 12285  df-fzo 12423  df-fl 12549  df-seq 12758  df-exp 12817  df-hash 13074  df-cj 13789  df-re 13790  df-im 13791  df-sqrt 13925  df-abs 13926  df-clim 14169  df-rlim 14170  df-sum 14367  df-rest 16023  df-topgen 16044  df-psmet 19678  df-xmet 19679  df-met 19680  df-bl 19681  df-mopn 19682  df-top 20639  df-topon 20656  df-bases 20690  df-cld 20763  df-cmp 21130  df-conn 21155  df-ovol 23173  df-vol 23174
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator