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 ssrab2 ⊢ { 𝑧 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) } ⊆ ℝ*
4 2 3 eqsstri ⊢ 𝑄 ⊆ ℝ*
5 infxrcl ⊢ ( 𝑄 ⊆ ℝ* → inf ( 𝑄 , ℝ* , < ) ∈ ℝ* )
6 4 5 mp1i ⊢ ( ⊤ → inf ( 𝑄 , ℝ* , < ) ∈ ℝ* )
7 ssrab2 ⊢ { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) } ⊆ ℝ*
8 1 7 eqsstri ⊢ 𝑀 ⊆ ℝ*
9 infxrcl ⊢ ( 𝑀 ⊆ ℝ* → inf ( 𝑀 , ℝ* , < ) ∈ ℝ* )
10 8 9 mp1i ⊢ ( ⊤ → inf ( 𝑀 , ℝ* , < ) ∈ ℝ* )
11 4 a1i ⊢ ( ⊤ → 𝑄 ⊆ ℝ* )
12 8 a1i ⊢ ( ⊤ → 𝑀 ⊆ ℝ* )
13 simpr ⊢ ( ( 𝑦 ∈ 𝑀 ∧ 𝑤 ∈ ℝ+ ) → 𝑤 ∈ ℝ+ )
14 1 rabeq2i ⊢ ( 𝑦 ∈ 𝑀 ↔ ( 𝑦 ∈ ℝ* ∧ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) )
15 14 biimpi ⊢ ( 𝑦 ∈ 𝑀 → ( 𝑦 ∈ ℝ* ∧ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) )
16 15 simprd ⊢ ( 𝑦 ∈ 𝑀 → ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) )
17 16 adantr ⊢ ( ( 𝑦 ∈ 𝑀 ∧ 𝑤 ∈ ℝ+ ) → ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) )
18 coeq2 ⊢ ( 𝑔 = 𝑓 → ( (,) ∘ 𝑔 ) = ( (,) ∘ 𝑓 ) )
19 18 rneqd ⊢ ( 𝑔 = 𝑓 → ran ( (,) ∘ 𝑔 ) = ran ( (,) ∘ 𝑓 ) )
20 19 unieqd ⊢ ( 𝑔 = 𝑓 → ∪ ran ( (,) ∘ 𝑔 ) = ∪ ran ( (,) ∘ 𝑓 ) )
21 20 sseq2d ⊢ ( 𝑔 = 𝑓 → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ↔ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) )
22 coeq2 ⊢ ( 𝑔 = 𝑓 → ( ( vol ∘ (,) ) ∘ 𝑔 ) = ( ( vol ∘ (,) ) ∘ 𝑓 ) )
23 22 fveq2d ⊢ ( 𝑔 = 𝑓 → ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) )
24 23 eqeq2d ⊢ ( 𝑔 = 𝑓 → ( 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ↔ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) )
25 21 24 anbi12d ⊢ ( 𝑔 = 𝑓 → ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) ↔ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ) )
26 25 cbvrexvw ⊢ ( ∃ 𝑔 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) ↔ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) )
27 26 rabbii ⊢ { 𝑧 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) } = { 𝑧 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) }
28 2 27 eqtr4i ⊢ 𝑄 = { 𝑧 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) }
29 simp3r ⊢ ( ( 𝑤 ∈ ℝ+ ∧ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) → 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) )
30 eqid ⊢ ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ ( 𝑚 ∈ ℕ ↦ ⟨ ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) − ( 𝑤 / ( 2 ↑ 𝑚 ) ) ) , ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) ⟩ ) ) ) = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ ( 𝑚 ∈ ℕ ↦ ⟨ ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) − ( 𝑤 / ( 2 ↑ 𝑚 ) ) ) , ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) ⟩ ) ) )
31 elmapi ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → 𝑓 : ℕ ⟶ ( ℝ × ℝ ) )
32 31 3ad2ant2 ⊢ ( ( 𝑤 ∈ ℝ+ ∧ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) → 𝑓 : ℕ ⟶ ( ℝ × ℝ ) )
33 simp3l ⊢ ( ( 𝑤 ∈ ℝ+ ∧ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) → 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) )
34 simp1 ⊢ ( ( 𝑤 ∈ ℝ+ ∧ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) → 𝑤 ∈ ℝ+ )
35 2fveq3 ⊢ ( 𝑚 = 𝑛 → ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) = ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) )
36 oveq2 ⊢ ( 𝑚 = 𝑛 → ( 2 ↑ 𝑚 ) = ( 2 ↑ 𝑛 ) )
37 36 oveq2d ⊢ ( 𝑚 = 𝑛 → ( 𝑤 / ( 2 ↑ 𝑚 ) ) = ( 𝑤 / ( 2 ↑ 𝑛 ) ) )
38 35 37 oveq12d ⊢ ( 𝑚 = 𝑛 → ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) − ( 𝑤 / ( 2 ↑ 𝑚 ) ) ) = ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) − ( 𝑤 / ( 2 ↑ 𝑛 ) ) ) )
39 2fveq3 ⊢ ( 𝑚 = 𝑛 → ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) = ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) )
40 38 39 opeq12d ⊢ ( 𝑚 = 𝑛 → ⟨ ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) − ( 𝑤 / ( 2 ↑ 𝑚 ) ) ) , ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) ⟩ = ⟨ ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) − ( 𝑤 / ( 2 ↑ 𝑛 ) ) ) , ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ )
41 40 cbvmptv ⊢ ( 𝑚 ∈ ℕ ↦ ⟨ ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) − ( 𝑤 / ( 2 ↑ 𝑚 ) ) ) , ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) ⟩ ) = ( 𝑛 ∈ ℕ ↦ ⟨ ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) − ( 𝑤 / ( 2 ↑ 𝑛 ) ) ) , ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ )
42 28 29 30 32 33 34 41 ovolval5lem2 ⊢ ( ( 𝑤 ∈ ℝ+ ∧ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) → ∃ 𝑧 ∈ 𝑄 𝑧 ≤ ( 𝑦 +𝑒 𝑤 ) )
43 42 3exp ⊢ ( 𝑤 ∈ ℝ+ → ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → ( ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) → ∃ 𝑧 ∈ 𝑄 𝑧 ≤ ( 𝑦 +𝑒 𝑤 ) ) ) )
44 43 rexlimdv ⊢ ( 𝑤 ∈ ℝ+ → ( ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) → ∃ 𝑧 ∈ 𝑄 𝑧 ≤ ( 𝑦 +𝑒 𝑤 ) ) )
45 44 imp ⊢ ( ( 𝑤 ∈ ℝ+ ∧ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) → ∃ 𝑧 ∈ 𝑄 𝑧 ≤ ( 𝑦 +𝑒 𝑤 ) )
46 13 17 45 syl2anc ⊢ ( ( 𝑦 ∈ 𝑀 ∧ 𝑤 ∈ ℝ+ ) → ∃ 𝑧 ∈ 𝑄 𝑧 ≤ ( 𝑦 +𝑒 𝑤 ) )
47 46 3adant1 ⊢ ( ( ⊤ ∧ 𝑦 ∈ 𝑀 ∧ 𝑤 ∈ ℝ+ ) → ∃ 𝑧 ∈ 𝑄 𝑧 ≤ ( 𝑦 +𝑒 𝑤 ) )
48 11 12 47 infleinf ⊢ ( ⊤ → inf ( 𝑄 , ℝ* , < ) ≤ inf ( 𝑀 , ℝ* , < ) )
49 eqeq1 ⊢ ( 𝑧 = 𝑦 → ( 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ↔ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) )
50 49 anbi2d ⊢ ( 𝑧 = 𝑦 → ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ↔ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ) )
51 50 rexbidv ⊢ ( 𝑧 = 𝑦 → ( ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ↔ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ) )
52 51 cbvrabv ⊢ { 𝑧 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) } = { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) }
53 simpr ⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) → 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) )
54 ioossico ⊢ ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) (,) ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⊆ ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) [,) ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) )
55 54 a1i ⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) (,) ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⊆ ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) [,) ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
56 31 adantr ⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → 𝑓 : ℕ ⟶ ( ℝ × ℝ ) )
57 simpr ⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
58 56 57 fvovco ⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( (,) ∘ 𝑓 ) ‘ 𝑛 ) = ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) (,) ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
59 56 57 fvovco ⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( [,) ∘ 𝑓 ) ‘ 𝑛 ) = ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) [,) ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
60 58 59 sseq12d ⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( ( (,) ∘ 𝑓 ) ‘ 𝑛 ) ⊆ ( ( [,) ∘ 𝑓 ) ‘ 𝑛 ) ↔ ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) (,) ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⊆ ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) [,) ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) )
61 55 60 mpbird ⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( (,) ∘ 𝑓 ) ‘ 𝑛 ) ⊆ ( ( [,) ∘ 𝑓 ) ‘ 𝑛 ) )
62 61 ralrimiva ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → ∀ 𝑛 ∈ ℕ ( ( (,) ∘ 𝑓 ) ‘ 𝑛 ) ⊆ ( ( [,) ∘ 𝑓 ) ‘ 𝑛 ) )
63 ss2iun ⊢ ( ∀ 𝑛 ∈ ℕ ( ( (,) ∘ 𝑓 ) ‘ 𝑛 ) ⊆ ( ( [,) ∘ 𝑓 ) ‘ 𝑛 ) → ∪ 𝑛 ∈ ℕ ( ( (,) ∘ 𝑓 ) ‘ 𝑛 ) ⊆ ∪ 𝑛 ∈ ℕ ( ( [,) ∘ 𝑓 ) ‘ 𝑛 ) )
64 62 63 syl ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → ∪ 𝑛 ∈ ℕ ( ( (,) ∘ 𝑓 ) ‘ 𝑛 ) ⊆ ∪ 𝑛 ∈ ℕ ( ( [,) ∘ 𝑓 ) ‘ 𝑛 ) )
65 ioof ⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
66 65 a1i ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ )
67 rexpssxrxp ⊢ ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* )
68 67 a1i ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* ) )
69 31 68 fssd ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → 𝑓 : ℕ ⟶ ( ℝ* × ℝ* ) )
70 fco ⊢ ( ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ ∧ 𝑓 : ℕ ⟶ ( ℝ* × ℝ* ) ) → ( (,) ∘ 𝑓 ) : ℕ ⟶ 𝒫 ℝ )
71 66 69 70 syl2anc ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → ( (,) ∘ 𝑓 ) : ℕ ⟶ 𝒫 ℝ )
72 71 ffnd ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → ( (,) ∘ 𝑓 ) Fn ℕ )
73 fniunfv ⊢ ( ( (,) ∘ 𝑓 ) Fn ℕ → ∪ 𝑛 ∈ ℕ ( ( (,) ∘ 𝑓 ) ‘ 𝑛 ) = ∪ ran ( (,) ∘ 𝑓 ) )
74 72 73 syl ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → ∪ 𝑛 ∈ ℕ ( ( (,) ∘ 𝑓 ) ‘ 𝑛 ) = ∪ ran ( (,) ∘ 𝑓 ) )
75 icof ⊢ [,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ*
76 75 a1i ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → [,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ* )
77 fco ⊢ ( ( [,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ* ∧ 𝑓 : ℕ ⟶ ( ℝ* × ℝ* ) ) → ( [,) ∘ 𝑓 ) : ℕ ⟶ 𝒫 ℝ* )
78 76 69 77 syl2anc ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → ( [,) ∘ 𝑓 ) : ℕ ⟶ 𝒫 ℝ* )
79 78 ffnd ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → ( [,) ∘ 𝑓 ) Fn ℕ )
80 fniunfv ⊢ ( ( [,) ∘ 𝑓 ) Fn ℕ → ∪ 𝑛 ∈ ℕ ( ( [,) ∘ 𝑓 ) ‘ 𝑛 ) = ∪ ran ( [,) ∘ 𝑓 ) )
81 79 80 syl ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → ∪ 𝑛 ∈ ℕ ( ( [,) ∘ 𝑓 ) ‘ 𝑛 ) = ∪ ran ( [,) ∘ 𝑓 ) )
82 74 81 sseq12d ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → ( ∪ 𝑛 ∈ ℕ ( ( (,) ∘ 𝑓 ) ‘ 𝑛 ) ⊆ ∪ 𝑛 ∈ ℕ ( ( [,) ∘ 𝑓 ) ‘ 𝑛 ) ↔ ∪ ran ( (,) ∘ 𝑓 ) ⊆ ∪ ran ( [,) ∘ 𝑓 ) ) )
83 64 82 mpbid ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → ∪ ran ( (,) ∘ 𝑓 ) ⊆ ∪ ran ( [,) ∘ 𝑓 ) )
84 83 adantr ⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) → ∪ ran ( (,) ∘ 𝑓 ) ⊆ ∪ ran ( [,) ∘ 𝑓 ) )
85 53 84 sstrd ⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) → 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) )
86 85 adantrr ⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ) → 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) )
87 simpr ⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) → 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) )
88 31 voliooicof ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → ( ( vol ∘ (,) ) ∘ 𝑓 ) = ( ( vol ∘ [,) ) ∘ 𝑓 ) )
89 88 fveq2d ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) )
90 89 adantr ⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) → ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) )
91 87 90 eqtrd ⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) → 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) )
92 91 adantrl ⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ) → 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) )
93 86 92 jca ⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ) → ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) )
94 93 ex ⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) → ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) )
95 94 reximia ⊢ ( ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) → ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) )
96 95 rgenw ⊢ ∀ 𝑦 ∈ ℝ* ( ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) → ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) )
97 ss2rab ⊢ ( { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) } ⊆ { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) } ↔ ∀ 𝑦 ∈ ℝ* ( ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) → ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) )
98 96 97 mpbir ⊢ { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) } ⊆ { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) }
99 52 98 eqsstri ⊢ { 𝑧 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) } ⊆ { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) }
100 2 1 sseq12i ⊢ ( 𝑄 ⊆ 𝑀 ↔ { 𝑧 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) } ⊆ { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) } )
101 99 100 mpbir ⊢ 𝑄 ⊆ 𝑀
102 infxrss ⊢ ( ( 𝑄 ⊆ 𝑀 ∧ 𝑀 ⊆ ℝ* ) → inf ( 𝑀 , ℝ* , < ) ≤ inf ( 𝑄 , ℝ* , < ) )
103 101 8 102 mp2an ⊢ inf ( 𝑀 , ℝ* , < ) ≤ inf ( 𝑄 , ℝ* , < )
104 103 a1i ⊢ ( ⊤ → inf ( 𝑀 , ℝ* , < ) ≤ inf ( 𝑄 , ℝ* , < ) )
105 6 10 48 104 xrletrid ⊢ ( ⊤ → inf ( 𝑄 , ℝ* , < ) = inf ( 𝑀 , ℝ* , < ) )
106 105 mptru ⊢ inf ( 𝑄 , ℝ* , < ) = inf ( 𝑀 , ℝ* , < )