Metamath Proof Explorer


Theorem ovolval3

Description: The value of the Lebesgue outer measure for subsets of the reals, expressed using sum^ and vol o. (,) . See ovolval and ovolval2 for alternative expressions. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses ovolval3.a ( 𝜑𝐴 ⊆ ℝ )
ovolval3.m 𝑀 = { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) }
Assertion ovolval3 ( 𝜑 → ( vol* ‘ 𝐴 ) = inf ( 𝑀 , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 ovolval3.a ( 𝜑𝐴 ⊆ ℝ )
2 ovolval3.m 𝑀 = { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) }
3 eqid { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( abs ∘ − ) ∘ 𝑓 ) ) ) } = { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( abs ∘ − ) ∘ 𝑓 ) ) ) }
4 1 3 ovolval2 ( 𝜑 → ( vol* ‘ 𝐴 ) = inf ( { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( abs ∘ − ) ∘ 𝑓 ) ) ) } , ℝ* , < ) )
5 reex ℝ ∈ V
6 5 5 xpex ( ℝ × ℝ ) ∈ V
7 inss2 ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
8 mapss ( ( ( ℝ × ℝ ) ∈ V ∧ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ ) ) → ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ⊆ ( ( ℝ × ℝ ) ↑m ℕ ) )
9 6 7 8 mp2an ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ⊆ ( ( ℝ × ℝ ) ↑m ℕ )
10 9 sseli ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) → 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) )
11 elmapi ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → 𝑓 : ℕ ⟶ ( ℝ × ℝ ) )
12 10 11 syl ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) → 𝑓 : ℕ ⟶ ( ℝ × ℝ ) )
13 12 ffvelrnda ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑓𝑛 ) ∈ ( ℝ × ℝ ) )
14 1st2nd2 ( ( 𝑓𝑛 ) ∈ ( ℝ × ℝ ) → ( 𝑓𝑛 ) = ⟨ ( 1st ‘ ( 𝑓𝑛 ) ) , ( 2nd ‘ ( 𝑓𝑛 ) ) ⟩ )
15 13 14 syl ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑓𝑛 ) = ⟨ ( 1st ‘ ( 𝑓𝑛 ) ) , ( 2nd ‘ ( 𝑓𝑛 ) ) ⟩ )
16 15 fveq2d ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( (,) ‘ ( 𝑓𝑛 ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝑓𝑛 ) ) , ( 2nd ‘ ( 𝑓𝑛 ) ) ⟩ ) )
17 df-ov ( ( 1st ‘ ( 𝑓𝑛 ) ) (,) ( 2nd ‘ ( 𝑓𝑛 ) ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝑓𝑛 ) ) , ( 2nd ‘ ( 𝑓𝑛 ) ) ⟩ )
18 17 eqcomi ( (,) ‘ ⟨ ( 1st ‘ ( 𝑓𝑛 ) ) , ( 2nd ‘ ( 𝑓𝑛 ) ) ⟩ ) = ( ( 1st ‘ ( 𝑓𝑛 ) ) (,) ( 2nd ‘ ( 𝑓𝑛 ) ) )
19 18 a1i ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( (,) ‘ ⟨ ( 1st ‘ ( 𝑓𝑛 ) ) , ( 2nd ‘ ( 𝑓𝑛 ) ) ⟩ ) = ( ( 1st ‘ ( 𝑓𝑛 ) ) (,) ( 2nd ‘ ( 𝑓𝑛 ) ) ) )
20 16 19 eqtrd ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( (,) ‘ ( 𝑓𝑛 ) ) = ( ( 1st ‘ ( 𝑓𝑛 ) ) (,) ( 2nd ‘ ( 𝑓𝑛 ) ) ) )
21 20 fveq2d ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( (,) ‘ ( 𝑓𝑛 ) ) ) = ( vol ‘ ( ( 1st ‘ ( 𝑓𝑛 ) ) (,) ( 2nd ‘ ( 𝑓𝑛 ) ) ) ) )
22 xp1st ( ( 𝑓𝑛 ) ∈ ( ℝ × ℝ ) → ( 1st ‘ ( 𝑓𝑛 ) ) ∈ ℝ )
23 13 22 syl ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 1st ‘ ( 𝑓𝑛 ) ) ∈ ℝ )
24 xp2nd ( ( 𝑓𝑛 ) ∈ ( ℝ × ℝ ) → ( 2nd ‘ ( 𝑓𝑛 ) ) ∈ ℝ )
25 13 24 syl ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 2nd ‘ ( 𝑓𝑛 ) ) ∈ ℝ )
26 elmapi ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) → 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
27 26 adantr ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
28 simpr ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
29 ovolfcl ( ( 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝑓𝑛 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝑓𝑛 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝑓𝑛 ) ) ≤ ( 2nd ‘ ( 𝑓𝑛 ) ) ) )
30 27 28 29 syl2anc ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝑓𝑛 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝑓𝑛 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝑓𝑛 ) ) ≤ ( 2nd ‘ ( 𝑓𝑛 ) ) ) )
31 30 simp3d ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 1st ‘ ( 𝑓𝑛 ) ) ≤ ( 2nd ‘ ( 𝑓𝑛 ) ) )
32 volioo ( ( ( 1st ‘ ( 𝑓𝑛 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝑓𝑛 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝑓𝑛 ) ) ≤ ( 2nd ‘ ( 𝑓𝑛 ) ) ) → ( vol ‘ ( ( 1st ‘ ( 𝑓𝑛 ) ) (,) ( 2nd ‘ ( 𝑓𝑛 ) ) ) ) = ( ( 2nd ‘ ( 𝑓𝑛 ) ) − ( 1st ‘ ( 𝑓𝑛 ) ) ) )
33 23 25 31 32 syl3anc ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( ( 1st ‘ ( 𝑓𝑛 ) ) (,) ( 2nd ‘ ( 𝑓𝑛 ) ) ) ) = ( ( 2nd ‘ ( 𝑓𝑛 ) ) − ( 1st ‘ ( 𝑓𝑛 ) ) ) )
34 21 33 eqtrd ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( (,) ‘ ( 𝑓𝑛 ) ) ) = ( ( 2nd ‘ ( 𝑓𝑛 ) ) − ( 1st ‘ ( 𝑓𝑛 ) ) ) )
35 ioof (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
36 ffun ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → Fun (,) )
37 35 36 ax-mp Fun (,)
38 37 a1i ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → Fun (,) )
39 rexpssxrxp ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* )
40 39 13 sseldi ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑓𝑛 ) ∈ ( ℝ* × ℝ* ) )
41 35 fdmi dom (,) = ( ℝ* × ℝ* )
42 41 eqcomi ( ℝ* × ℝ* ) = dom (,)
43 42 a1i ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ℝ* × ℝ* ) = dom (,) )
44 40 43 eleqtrd ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑓𝑛 ) ∈ dom (,) )
45 fvco ( ( Fun (,) ∧ ( 𝑓𝑛 ) ∈ dom (,) ) → ( ( vol ∘ (,) ) ‘ ( 𝑓𝑛 ) ) = ( vol ‘ ( (,) ‘ ( 𝑓𝑛 ) ) ) )
46 38 44 45 syl2anc ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( vol ∘ (,) ) ‘ ( 𝑓𝑛 ) ) = ( vol ‘ ( (,) ‘ ( 𝑓𝑛 ) ) ) )
47 15 fveq2d ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( abs ∘ − ) ‘ ( 𝑓𝑛 ) ) = ( ( abs ∘ − ) ‘ ⟨ ( 1st ‘ ( 𝑓𝑛 ) ) , ( 2nd ‘ ( 𝑓𝑛 ) ) ⟩ ) )
48 df-ov ( ( 1st ‘ ( 𝑓𝑛 ) ) ( abs ∘ − ) ( 2nd ‘ ( 𝑓𝑛 ) ) ) = ( ( abs ∘ − ) ‘ ⟨ ( 1st ‘ ( 𝑓𝑛 ) ) , ( 2nd ‘ ( 𝑓𝑛 ) ) ⟩ )
49 48 eqcomi ( ( abs ∘ − ) ‘ ⟨ ( 1st ‘ ( 𝑓𝑛 ) ) , ( 2nd ‘ ( 𝑓𝑛 ) ) ⟩ ) = ( ( 1st ‘ ( 𝑓𝑛 ) ) ( abs ∘ − ) ( 2nd ‘ ( 𝑓𝑛 ) ) )
50 49 a1i ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( abs ∘ − ) ‘ ⟨ ( 1st ‘ ( 𝑓𝑛 ) ) , ( 2nd ‘ ( 𝑓𝑛 ) ) ⟩ ) = ( ( 1st ‘ ( 𝑓𝑛 ) ) ( abs ∘ − ) ( 2nd ‘ ( 𝑓𝑛 ) ) ) )
51 23 recnd ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 1st ‘ ( 𝑓𝑛 ) ) ∈ ℂ )
52 25 recnd ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 2nd ‘ ( 𝑓𝑛 ) ) ∈ ℂ )
53 eqid ( abs ∘ − ) = ( abs ∘ − )
54 53 cnmetdval ( ( ( 1st ‘ ( 𝑓𝑛 ) ) ∈ ℂ ∧ ( 2nd ‘ ( 𝑓𝑛 ) ) ∈ ℂ ) → ( ( 1st ‘ ( 𝑓𝑛 ) ) ( abs ∘ − ) ( 2nd ‘ ( 𝑓𝑛 ) ) ) = ( abs ‘ ( ( 1st ‘ ( 𝑓𝑛 ) ) − ( 2nd ‘ ( 𝑓𝑛 ) ) ) ) )
55 51 52 54 syl2anc ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝑓𝑛 ) ) ( abs ∘ − ) ( 2nd ‘ ( 𝑓𝑛 ) ) ) = ( abs ‘ ( ( 1st ‘ ( 𝑓𝑛 ) ) − ( 2nd ‘ ( 𝑓𝑛 ) ) ) ) )
56 abssub ( ( ( 1st ‘ ( 𝑓𝑛 ) ) ∈ ℂ ∧ ( 2nd ‘ ( 𝑓𝑛 ) ) ∈ ℂ ) → ( abs ‘ ( ( 1st ‘ ( 𝑓𝑛 ) ) − ( 2nd ‘ ( 𝑓𝑛 ) ) ) ) = ( abs ‘ ( ( 2nd ‘ ( 𝑓𝑛 ) ) − ( 1st ‘ ( 𝑓𝑛 ) ) ) ) )
57 51 52 56 syl2anc ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( abs ‘ ( ( 1st ‘ ( 𝑓𝑛 ) ) − ( 2nd ‘ ( 𝑓𝑛 ) ) ) ) = ( abs ‘ ( ( 2nd ‘ ( 𝑓𝑛 ) ) − ( 1st ‘ ( 𝑓𝑛 ) ) ) ) )
58 23 25 31 abssubge0d ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( abs ‘ ( ( 2nd ‘ ( 𝑓𝑛 ) ) − ( 1st ‘ ( 𝑓𝑛 ) ) ) ) = ( ( 2nd ‘ ( 𝑓𝑛 ) ) − ( 1st ‘ ( 𝑓𝑛 ) ) ) )
59 55 57 58 3eqtrd ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝑓𝑛 ) ) ( abs ∘ − ) ( 2nd ‘ ( 𝑓𝑛 ) ) ) = ( ( 2nd ‘ ( 𝑓𝑛 ) ) − ( 1st ‘ ( 𝑓𝑛 ) ) ) )
60 47 50 59 3eqtrd ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( abs ∘ − ) ‘ ( 𝑓𝑛 ) ) = ( ( 2nd ‘ ( 𝑓𝑛 ) ) − ( 1st ‘ ( 𝑓𝑛 ) ) ) )
61 34 46 60 3eqtr4d ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( vol ∘ (,) ) ‘ ( 𝑓𝑛 ) ) = ( ( abs ∘ − ) ‘ ( 𝑓𝑛 ) ) )
62 61 mpteq2dva ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) → ( 𝑛 ∈ ℕ ↦ ( ( vol ∘ (,) ) ‘ ( 𝑓𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( abs ∘ − ) ‘ ( 𝑓𝑛 ) ) ) )
63 volioof ( vol ∘ (,) ) : ( ℝ* × ℝ* ) ⟶ ( 0 [,] +∞ )
64 63 a1i ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) → ( vol ∘ (,) ) : ( ℝ* × ℝ* ) ⟶ ( 0 [,] +∞ ) )
65 39 a1i ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) → ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* ) )
66 12 65 fssd ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) → 𝑓 : ℕ ⟶ ( ℝ* × ℝ* ) )
67 fcompt ( ( ( vol ∘ (,) ) : ( ℝ* × ℝ* ) ⟶ ( 0 [,] +∞ ) ∧ 𝑓 : ℕ ⟶ ( ℝ* × ℝ* ) ) → ( ( vol ∘ (,) ) ∘ 𝑓 ) = ( 𝑛 ∈ ℕ ↦ ( ( vol ∘ (,) ) ‘ ( 𝑓𝑛 ) ) ) )
68 64 66 67 syl2anc ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) → ( ( vol ∘ (,) ) ∘ 𝑓 ) = ( 𝑛 ∈ ℕ ↦ ( ( vol ∘ (,) ) ‘ ( 𝑓𝑛 ) ) ) )
69 absf abs : ℂ ⟶ ℝ
70 subf − : ( ℂ × ℂ ) ⟶ ℂ
71 fco ( ( abs : ℂ ⟶ ℝ ∧ − : ( ℂ × ℂ ) ⟶ ℂ ) → ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ )
72 69 70 71 mp2an ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ
73 72 a1i ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) → ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ )
74 rr2sscn2 ( ℝ × ℝ ) ⊆ ( ℂ × ℂ )
75 74 a1i ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) → ( ℝ × ℝ ) ⊆ ( ℂ × ℂ ) )
76 12 75 fssd ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) → 𝑓 : ℕ ⟶ ( ℂ × ℂ ) )
77 fcompt ( ( ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ ∧ 𝑓 : ℕ ⟶ ( ℂ × ℂ ) ) → ( ( abs ∘ − ) ∘ 𝑓 ) = ( 𝑛 ∈ ℕ ↦ ( ( abs ∘ − ) ‘ ( 𝑓𝑛 ) ) ) )
78 73 76 77 syl2anc ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) → ( ( abs ∘ − ) ∘ 𝑓 ) = ( 𝑛 ∈ ℕ ↦ ( ( abs ∘ − ) ‘ ( 𝑓𝑛 ) ) ) )
79 62 68 78 3eqtr4d ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) → ( ( vol ∘ (,) ) ∘ 𝑓 ) = ( ( abs ∘ − ) ∘ 𝑓 ) )
80 79 fveq2d ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) → ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) = ( Σ^ ‘ ( ( abs ∘ − ) ∘ 𝑓 ) ) )
81 80 eqeq2d ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) → ( 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ↔ 𝑦 = ( Σ^ ‘ ( ( abs ∘ − ) ∘ 𝑓 ) ) ) )
82 81 anbi2d ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) → ( ( 𝐴 ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ↔ ( 𝐴 ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( abs ∘ − ) ∘ 𝑓 ) ) ) ) )
83 82 rexbiia ( ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ↔ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( abs ∘ − ) ∘ 𝑓 ) ) ) )
84 83 rabbii { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) } = { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( abs ∘ − ) ∘ 𝑓 ) ) ) }
85 2 84 eqtr2i { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( abs ∘ − ) ∘ 𝑓 ) ) ) } = 𝑀
86 85 infeq1i inf ( { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( abs ∘ − ) ∘ 𝑓 ) ) ) } , ℝ* , < ) = inf ( 𝑀 , ℝ* , < )
87 86 a1i ( 𝜑 → inf ( { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( abs ∘ − ) ∘ 𝑓 ) ) ) } , ℝ* , < ) = inf ( 𝑀 , ℝ* , < ) )
88 4 87 eqtrd ( 𝜑 → ( vol* ‘ 𝐴 ) = inf ( 𝑀 , ℝ* , < ) )