Metamath Proof Explorer

Theorem ovolval5lem3

Description: The value of the Lebesgue outer measure for subsets of the reals, using covers of left-closed right-open intervals are used, instead of open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses ovolval5lem3.m ⊢ 𝑀 = { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) }
ovolval5lem3.q ⊢ 𝑄 = { 𝑧 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) }
Assertion ovolval5lem3 inf ( 𝑄 , ℝ* , < ) = inf ( 𝑀 , ℝ* , < )

Proof

Step Hyp Ref Expression
1 ovolval5lem3.m ⊢ 𝑀 = { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) }
2 ovolval5lem3.q ⊢ 𝑄 = { 𝑧 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) }
3 2 ssrab3 ⊢ 𝑄 ⊆ ℝ*
4 infxrcl ⊢ ( 𝑄 ⊆ ℝ* → inf ( 𝑄 , ℝ* , < ) ∈ ℝ* )
5 3 4 mp1i ⊢ ( ⊤ → inf ( 𝑄 , ℝ* , < ) ∈ ℝ* )
6 1 ssrab3 ⊢ 𝑀 ⊆ ℝ*
7 infxrcl ⊢ ( 𝑀 ⊆ ℝ* → inf ( 𝑀 , ℝ* , < ) ∈ ℝ* )
8 6 7 mp1i ⊢ ( ⊤ → inf ( 𝑀 , ℝ* , < ) ∈ ℝ* )
9 3 a1i ⊢ ( ⊤ → 𝑄 ⊆ ℝ* )
10 6 a1i ⊢ ( ⊤ → 𝑀 ⊆ ℝ* )
11 1 reqabi ⊢ ( 𝑦 ∈ 𝑀 ↔ ( 𝑦 ∈ ℝ* ∧ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) )
12 11 simprbi ⊢ ( 𝑦 ∈ 𝑀 → ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) )
13 coeq2 ⊢ ( 𝑔 = 𝑓 → ( (,) ∘ 𝑔 ) = ( (,) ∘ 𝑓 ) )
14 13 rneqd ⊢ ( 𝑔 = 𝑓 → ran ( (,) ∘ 𝑔 ) = ran ( (,) ∘ 𝑓 ) )
15 14 unieqd ⊢ ( 𝑔 = 𝑓 → ∪ ran ( (,) ∘ 𝑔 ) = ∪ ran ( (,) ∘ 𝑓 ) )
16 15 sseq2d ⊢ ( 𝑔 = 𝑓 → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ↔ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) )
17 coeq2 ⊢ ( 𝑔 = 𝑓 → ( ( vol ∘ (,) ) ∘ 𝑔 ) = ( ( vol ∘ (,) ) ∘ 𝑓 ) )
18 17 fveq2d ⊢ ( 𝑔 = 𝑓 → ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) )
19 18 eqeq2d ⊢ ( 𝑔 = 𝑓 → ( 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ↔ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) )
20 16 19 anbi12d ⊢ ( 𝑔 = 𝑓 → ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) ↔ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ) )
21 20 cbvrexvw ⊢ ( ∃ 𝑔 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) ↔ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) )
22 21 rabbii ⊢ { 𝑧 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) } = { 𝑧 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) }
23 2 22 eqtr4i ⊢ 𝑄 = { 𝑧 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) }
24 simp3r ⊢ ( ( 𝑤 ∈ ℝ+ ∧ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) → 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) )
25 eqid ⊢ ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ ( 𝑚 ∈ ℕ ↦ ⟨ ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) − ( 𝑤 / ( 2 ↑ 𝑚 ) ) ) , ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) ⟩ ) ) ) = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ ( 𝑚 ∈ ℕ ↦ ⟨ ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) − ( 𝑤 / ( 2 ↑ 𝑚 ) ) ) , ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) ⟩ ) ) )
26 elmapi ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → 𝑓 : ℕ ⟶ ( ℝ × ℝ ) )
27 26 3ad2ant2 ⊢ ( ( 𝑤 ∈ ℝ+ ∧ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) → 𝑓 : ℕ ⟶ ( ℝ × ℝ ) )
28 simp3l ⊢ ( ( 𝑤 ∈ ℝ+ ∧ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) → 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) )
29 simp1 ⊢ ( ( 𝑤 ∈ ℝ+ ∧ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) → 𝑤 ∈ ℝ+ )
30 2fveq3 ⊢ ( 𝑚 = 𝑛 → ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) = ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) )
31 oveq2 ⊢ ( 𝑚 = 𝑛 → ( 2 ↑ 𝑚 ) = ( 2 ↑ 𝑛 ) )
32 31 oveq2d ⊢ ( 𝑚 = 𝑛 → ( 𝑤 / ( 2 ↑ 𝑚 ) ) = ( 𝑤 / ( 2 ↑ 𝑛 ) ) )
33 30 32 oveq12d ⊢ ( 𝑚 = 𝑛 → ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) − ( 𝑤 / ( 2 ↑ 𝑚 ) ) ) = ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) − ( 𝑤 / ( 2 ↑ 𝑛 ) ) ) )
34 2fveq3 ⊢ ( 𝑚 = 𝑛 → ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) = ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) )
35 33 34 opeq12d ⊢ ( 𝑚 = 𝑛 → ⟨ ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) − ( 𝑤 / ( 2 ↑ 𝑚 ) ) ) , ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) ⟩ = ⟨ ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) − ( 𝑤 / ( 2 ↑ 𝑛 ) ) ) , ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ )
36 35 cbvmptv ⊢ ( 𝑚 ∈ ℕ ↦ ⟨ ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) − ( 𝑤 / ( 2 ↑ 𝑚 ) ) ) , ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) ⟩ ) = ( 𝑛 ∈ ℕ ↦ ⟨ ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) − ( 𝑤 / ( 2 ↑ 𝑛 ) ) ) , ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ )
37 23 24 25 27 28 29 36 ovolval5lem2 ⊢ ( ( 𝑤 ∈ ℝ+ ∧ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) → ∃ 𝑧 ∈ 𝑄 𝑧 ≤ ( 𝑦 +𝑒 𝑤 ) )
38 37 rexlimdv3a ⊢ ( 𝑤 ∈ ℝ+ → ( ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) → ∃ 𝑧 ∈ 𝑄 𝑧 ≤ ( 𝑦 +𝑒 𝑤 ) ) )
39 12 38 mpan9 ⊢ ( ( 𝑦 ∈ 𝑀 ∧ 𝑤 ∈ ℝ+ ) → ∃ 𝑧 ∈ 𝑄 𝑧 ≤ ( 𝑦 +𝑒 𝑤 ) )
40 39 3adant1 ⊢ ( ( ⊤ ∧ 𝑦 ∈ 𝑀 ∧ 𝑤 ∈ ℝ+ ) → ∃ 𝑧 ∈ 𝑄 𝑧 ≤ ( 𝑦 +𝑒 𝑤 ) )
41 9 10 40 infleinf ⊢ ( ⊤ → inf ( 𝑄 , ℝ* , < ) ≤ inf ( 𝑀 , ℝ* , < ) )
42 eqeq1 ⊢ ( 𝑧 = 𝑦 → ( 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ↔ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) )
43 42 anbi2d ⊢ ( 𝑧 = 𝑦 → ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ↔ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ) )
44 43 rexbidv ⊢ ( 𝑧 = 𝑦 → ( ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ↔ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ) )
45 44 cbvrabv ⊢ { 𝑧 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) } = { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) }
46 simpr ⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) → 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) )
47 ioossico ⊢ ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) (,) ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⊆ ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) [,) ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) )
48 47 a1i ⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) (,) ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⊆ ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) [,) ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
49 26 adantr ⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → 𝑓 : ℕ ⟶ ( ℝ × ℝ ) )
50 simpr ⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
51 49 50 fvovco ⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( (,) ∘ 𝑓 ) ‘ 𝑛 ) = ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) (,) ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
52 49 50 fvovco ⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( [,) ∘ 𝑓 ) ‘ 𝑛 ) = ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) [,) ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
53 48 51 52 3sstr4d ⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( (,) ∘ 𝑓 ) ‘ 𝑛 ) ⊆ ( ( [,) ∘ 𝑓 ) ‘ 𝑛 ) )
54 53 ralrimiva ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → ∀ 𝑛 ∈ ℕ ( ( (,) ∘ 𝑓 ) ‘ 𝑛 ) ⊆ ( ( [,) ∘ 𝑓 ) ‘ 𝑛 ) )
55 ss2iun ⊢ ( ∀ 𝑛 ∈ ℕ ( ( (,) ∘ 𝑓 ) ‘ 𝑛 ) ⊆ ( ( [,) ∘ 𝑓 ) ‘ 𝑛 ) → ∪ 𝑛 ∈ ℕ ( ( (,) ∘ 𝑓 ) ‘ 𝑛 ) ⊆ ∪ 𝑛 ∈ ℕ ( ( [,) ∘ 𝑓 ) ‘ 𝑛 ) )
56 54 55 syl ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → ∪ 𝑛 ∈ ℕ ( ( (,) ∘ 𝑓 ) ‘ 𝑛 ) ⊆ ∪ 𝑛 ∈ ℕ ( ( [,) ∘ 𝑓 ) ‘ 𝑛 ) )
57 ioof ⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
58 57 a1i ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ )
59 rexpssxrxp ⊢ ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* )
60 59 a1i ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* ) )
61 58 60 26 fcoss ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → ( (,) ∘ 𝑓 ) : ℕ ⟶ 𝒫 ℝ )
62 61 ffnd ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → ( (,) ∘ 𝑓 ) Fn ℕ )
63 fniunfv ⊢ ( ( (,) ∘ 𝑓 ) Fn ℕ → ∪ 𝑛 ∈ ℕ ( ( (,) ∘ 𝑓 ) ‘ 𝑛 ) = ∪ ran ( (,) ∘ 𝑓 ) )
64 62 63 syl ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → ∪ 𝑛 ∈ ℕ ( ( (,) ∘ 𝑓 ) ‘ 𝑛 ) = ∪ ran ( (,) ∘ 𝑓 ) )
65 icof ⊢ [,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ*
66 65 a1i ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → [,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ* )
67 66 60 26 fcoss ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → ( [,) ∘ 𝑓 ) : ℕ ⟶ 𝒫 ℝ* )
68 67 ffnd ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → ( [,) ∘ 𝑓 ) Fn ℕ )
69 fniunfv ⊢ ( ( [,) ∘ 𝑓 ) Fn ℕ → ∪ 𝑛 ∈ ℕ ( ( [,) ∘ 𝑓 ) ‘ 𝑛 ) = ∪ ran ( [,) ∘ 𝑓 ) )
70 68 69 syl ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → ∪ 𝑛 ∈ ℕ ( ( [,) ∘ 𝑓 ) ‘ 𝑛 ) = ∪ ran ( [,) ∘ 𝑓 ) )
71 56 64 70 3sstr3d ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → ∪ ran ( (,) ∘ 𝑓 ) ⊆ ∪ ran ( [,) ∘ 𝑓 ) )
72 71 adantr ⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) → ∪ ran ( (,) ∘ 𝑓 ) ⊆ ∪ ran ( [,) ∘ 𝑓 ) )
73 46 72 sstrd ⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) → 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) )
74 simpr ⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) → 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) )
75 26 voliooicof ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → ( ( vol ∘ (,) ) ∘ 𝑓 ) = ( ( vol ∘ [,) ) ∘ 𝑓 ) )
76 75 fveq2d ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) )
77 76 adantr ⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) → ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) )
78 74 77 eqtrd ⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) → 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) )
79 73 78 anim12dan ⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ) → ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) )
80 79 ex ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) → ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) )
81 80 reximia ⊢ ( ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) → ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) )
82 81 a1i ⊢ ( 𝑦 ∈ ℝ* → ( ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) → ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) )
83 82 ss2rabi ⊢ { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) } ⊆ { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) }
84 45 83 eqsstri ⊢ { 𝑧 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) } ⊆ { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) }
85 84 2 1 3sstr4i ⊢ 𝑄 ⊆ 𝑀
86 infxrss ⊢ ( ( 𝑄 ⊆ 𝑀 ∧ 𝑀 ⊆ ℝ* ) → inf ( 𝑀 , ℝ* , < ) ≤ inf ( 𝑄 , ℝ* , < ) )
87 85 6 86 mp2an ⊢ inf ( 𝑀 , ℝ* , < ) ≤ inf ( 𝑄 , ℝ* , < )
88 87 a1i ⊢ ( ⊤ → inf ( 𝑀 , ℝ* , < ) ≤ inf ( 𝑄 , ℝ* , < ) )
89 5 8 41 88 xrletrid ⊢ ( ⊤ → inf ( 𝑄 , ℝ* , < ) = inf ( 𝑀 , ℝ* , < ) )
90 89 mptru ⊢ inf ( 𝑄 , ℝ* , < ) = inf ( 𝑀 , ℝ* , < )