Metamath Proof Explorer

Theorem ovnovollem3

Description: The 1-dimensional Lebesgue outer measure agrees with the Lebesgue outer measure on subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses ovnovollem3.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
ovnovollem3.b ⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
ovnovollem3.m ⊢ 𝑀 = { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) }
ovnovollem3.n ⊢ 𝑁 = { 𝑧 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) }
Assertion ovnovollem3 ( 𝜑 → ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝐵 ↑m { 𝐴 } ) ) = ( vol* ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ovnovollem3.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 ovnovollem3.b ⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
3 ovnovollem3.m ⊢ 𝑀 = { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) }
4 ovnovollem3.n ⊢ 𝑁 = { 𝑧 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) }
5 1 snn0d ⊢ ( 𝜑 → { 𝐴 } ≠ ∅ )
6 5 neneqd ⊢ ( 𝜑 → ¬ { 𝐴 } = ∅ )
7 6 iffalsed ⊢ ( 𝜑 → if ( { 𝐴 } = ∅ , 0 , inf ( 𝑀 , ℝ* , < ) ) = inf ( 𝑀 , ℝ* , < ) )
8 snfi ⊢ { 𝐴 } ∈ Fin
9 8 a1i ⊢ ( 𝜑 → { 𝐴 } ∈ Fin )
10 reex ⊢ ℝ ∈ V
11 10 a1i ⊢ ( 𝜑 → ℝ ∈ V )
12 mapss ⊢ ( ( ℝ ∈ V ∧ 𝐵 ⊆ ℝ ) → ( 𝐵 ↑m { 𝐴 } ) ⊆ ( ℝ ↑m { 𝐴 } ) )
13 11 2 12 syl2anc ⊢ ( 𝜑 → ( 𝐵 ↑m { 𝐴 } ) ⊆ ( ℝ ↑m { 𝐴 } ) )
14 9 13 3 ovnval2 ⊢ ( 𝜑 → ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝐵 ↑m { 𝐴 } ) ) = if ( { 𝐴 } = ∅ , 0 , inf ( 𝑀 , ℝ* , < ) ) )
15 2 4 ovolval5 ⊢ ( 𝜑 → ( vol* ‘ 𝐵 ) = inf ( 𝑁 , ℝ* , < ) )
16 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ) ∧ ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) → 𝐴 ∈ 𝑉 )
17 simplr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ) ∧ ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) → 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) )
18 fveq2 ⊢ ( 𝑛 = 𝑗 → ( 𝑓 ‘ 𝑛 ) = ( 𝑓 ‘ 𝑗 ) )
19 18 opeq2d ⊢ ( 𝑛 = 𝑗 → ⟨ 𝐴 , ( 𝑓 ‘ 𝑛 ) ⟩ = ⟨ 𝐴 , ( 𝑓 ‘ 𝑗 ) ⟩ )
20 19 sneqd ⊢ ( 𝑛 = 𝑗 → { ⟨ 𝐴 , ( 𝑓 ‘ 𝑛 ) ⟩ } = { ⟨ 𝐴 , ( 𝑓 ‘ 𝑗 ) ⟩ } )
21 20 cbvmptv ⊢ ( 𝑛 ∈ ℕ ↦ { ⟨ 𝐴 , ( 𝑓 ‘ 𝑛 ) ⟩ } ) = ( 𝑗 ∈ ℕ ↦ { ⟨ 𝐴 , ( 𝑓 ‘ 𝑗 ) ⟩ } )
22 simprl ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ) ∧ ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) → 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) )
23 11 2 ssexd ⊢ ( 𝜑 → 𝐵 ∈ V )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ) → 𝐵 ∈ V )
25 24 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ) ∧ ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) → 𝐵 ∈ V )
26 simprr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ) ∧ ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) → 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) )
27 16 17 21 22 25 26 ovnovollem1 ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ) ∧ ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) → ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
28 27 rexlimdva2 ⊢ ( 𝜑 → ( ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) → ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
29 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ∧ ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → 𝐴 ∈ 𝑉 )
30 23 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ∧ ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → 𝐵 ∈ V )
31 simp2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ∧ ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) )
32 simp3l ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ∧ ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) )
33 fveq2 ⊢ ( 𝑗 = 𝑛 → ( 𝑖 ‘ 𝑗 ) = ( 𝑖 ‘ 𝑛 ) )
34 33 coeq2d ⊢ ( 𝑗 = 𝑛 → ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) = ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) )
35 34 fveq1d ⊢ ( 𝑗 = 𝑛 → ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑘 ) )
36 35 ixpeq2dv ⊢ ( 𝑗 = 𝑛 → X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑘 ) )
37 fveq2 ⊢ ( 𝑘 = 𝑙 → ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑘 ) = ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 ) )
38 37 cbvixpv ⊢ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑘 ) = X 𝑙 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 )
39 38 a1i ⊢ ( 𝑗 = 𝑛 → X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑘 ) = X 𝑙 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 ) )
40 36 39 eqtrd ⊢ ( 𝑗 = 𝑛 → X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = X 𝑙 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 ) )
41 40 cbviunv ⊢ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = ∪ 𝑛 ∈ ℕ X 𝑙 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 )
42 41 sseq2i ⊢ ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ↔ ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑛 ∈ ℕ X 𝑙 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 ) )
43 42 biimpi ⊢ ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) → ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑛 ∈ ℕ X 𝑙 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 ) )
44 32 43 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ∧ ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑛 ∈ ℕ X 𝑙 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 ) )
45 simp3r ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ∧ ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
46 35 fveq2d ⊢ ( 𝑗 = 𝑛 → ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑘 ) ) )
47 46 prodeq2ad ⊢ ( 𝑗 = 𝑛 → ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑘 ) ) )
48 37 fveq2d ⊢ ( 𝑘 = 𝑙 → ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 ) ) )
49 48 cbvprodv ⊢ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑘 ) ) = ∏ 𝑙 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 ) )
50 49 a1i ⊢ ( 𝑗 = 𝑛 → ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑘 ) ) = ∏ 𝑙 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 ) ) )
51 47 50 eqtrd ⊢ ( 𝑗 = 𝑛 → ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ∏ 𝑙 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 ) ) )
52 51 cbvmptv ⊢ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) = ( 𝑛 ∈ ℕ ↦ ∏ 𝑙 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 ) ) )
53 52 fveq2i ⊢ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ∏ 𝑙 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 ) ) ) )
54 53 eqeq2i ⊢ ( 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ↔ 𝑧 = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ∏ 𝑙 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 ) ) ) ) )
55 54 biimpi ⊢ ( 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) → 𝑧 = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ∏ 𝑙 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 ) ) ) ) )
56 45 55 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ∧ ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → 𝑧 = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ∏ 𝑙 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 ) ) ) ) )
57 fveq2 ⊢ ( 𝑚 = 𝑛 → ( 𝑖 ‘ 𝑚 ) = ( 𝑖 ‘ 𝑛 ) )
58 57 fveq1d ⊢ ( 𝑚 = 𝑛 → ( ( 𝑖 ‘ 𝑚 ) ‘ 𝐴 ) = ( ( 𝑖 ‘ 𝑛 ) ‘ 𝐴 ) )
59 58 cbvmptv ⊢ ( 𝑚 ∈ ℕ ↦ ( ( 𝑖 ‘ 𝑚 ) ‘ 𝐴 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝐴 ) )
60 29 30 31 44 56 59 ovnovollem2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ∧ ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) )
61 60 3exp ⊢ ( 𝜑 → ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) → ( ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) ) )
62 61 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) )
63 28 62 impbid ⊢ ( 𝜑 → ( ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ↔ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
64 63 rabbidv ⊢ ( 𝜑 → { 𝑧 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) } = { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } )
65 4 a1i ⊢ ( 𝜑 → 𝑁 = { 𝑧 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) } )
66 3 a1i ⊢ ( 𝜑 → 𝑀 = { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } )
67 64 65 66 3eqtr4d ⊢ ( 𝜑 → 𝑁 = 𝑀 )
68 67 infeq1d ⊢ ( 𝜑 → inf ( 𝑁 , ℝ* , < ) = inf ( 𝑀 , ℝ* , < ) )
69 15 68 eqtrd ⊢ ( 𝜑 → ( vol* ‘ 𝐵 ) = inf ( 𝑀 , ℝ* , < ) )
70 7 14 69 3eqtr4d ⊢ ( 𝜑 → ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝐵 ↑m { 𝐴 } ) ) = ( vol* ‘ 𝐵 ) )