Metamath Proof Explorer


Theorem ovncvr2

Description: B and T are the left and right side of a cover of A . This cover is made of n-dimensional half-open intervals and approximates the n-dimensional Lebesgue outer volume of A . (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses ovncvr2.x ( 𝜑𝑋 ∈ Fin )
ovncvr2.a ( 𝜑𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
ovncvr2.e ( 𝜑𝐸 ∈ ℝ+ )
ovncvr2.c 𝐶 = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } )
ovncvr2.l 𝐿 = ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) )
ovncvr2.d 𝐷 = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ ( 𝑟 ∈ ℝ+ ↦ { 𝑖 ∈ ( 𝐶𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑟 ) } ) )
ovncvr2.i ( 𝜑𝐼 ∈ ( ( 𝐷𝐴 ) ‘ 𝐸 ) )
ovncvr2.b 𝐵 = ( 𝑗 ∈ ℕ ↦ ( 𝑘𝑋 ↦ ( 1st ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) )
ovncvr2.t 𝑇 = ( 𝑗 ∈ ℕ ↦ ( 𝑘𝑋 ↦ ( 2nd ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) )
Assertion ovncvr2 ( 𝜑 → ( ( ( 𝐵 : ℕ ⟶ ( ℝ ↑m 𝑋 ) ∧ 𝑇 : ℕ ⟶ ( ℝ ↑m 𝑋 ) ) ∧ 𝐴 𝑗 ∈ ℕ X 𝑘𝑋 ( ( ( 𝐵𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇𝑗 ) ‘ 𝑘 ) ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( ( 𝐵𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇𝑗 ) ‘ 𝑘 ) ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝐸 ) ) )

Proof

Step Hyp Ref Expression
1 ovncvr2.x ( 𝜑𝑋 ∈ Fin )
2 ovncvr2.a ( 𝜑𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
3 ovncvr2.e ( 𝜑𝐸 ∈ ℝ+ )
4 ovncvr2.c 𝐶 = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } )
5 ovncvr2.l 𝐿 = ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) )
6 ovncvr2.d 𝐷 = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ ( 𝑟 ∈ ℝ+ ↦ { 𝑖 ∈ ( 𝐶𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑟 ) } ) )
7 ovncvr2.i ( 𝜑𝐼 ∈ ( ( 𝐷𝐴 ) ‘ 𝐸 ) )
8 ovncvr2.b 𝐵 = ( 𝑗 ∈ ℕ ↦ ( 𝑘𝑋 ↦ ( 1st ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) )
9 ovncvr2.t 𝑇 = ( 𝑗 ∈ ℕ ↦ ( 𝑘𝑋 ↦ ( 2nd ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) )
10 sseq1 ( 𝑎 = 𝐴 → ( 𝑎 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) ↔ 𝐴 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) ) )
11 10 rabbidv ( 𝑎 = 𝐴 → { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } = { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝐴 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } )
12 ovexd ( 𝜑 → ( ℝ ↑m 𝑋 ) ∈ V )
13 12 2 ssexd ( 𝜑𝐴 ∈ V )
14 elpwg ( 𝐴 ∈ V → ( 𝐴 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↔ 𝐴 ⊆ ( ℝ ↑m 𝑋 ) ) )
15 13 14 syl ( 𝜑 → ( 𝐴 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↔ 𝐴 ⊆ ( ℝ ↑m 𝑋 ) ) )
16 2 15 mpbird ( 𝜑𝐴 ∈ 𝒫 ( ℝ ↑m 𝑋 ) )
17 ovex ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∈ V
18 17 rabex { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝐴 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } ∈ V
19 18 a1i ( 𝜑 → { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝐴 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } ∈ V )
20 4 11 16 19 fvmptd3 ( 𝜑 → ( 𝐶𝐴 ) = { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝐴 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } )
21 ssrab2 { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝐴 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } ⊆ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ )
22 21 a1i ( 𝜑 → { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝐴 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } ⊆ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) )
23 20 22 eqsstrd ( 𝜑 → ( 𝐶𝐴 ) ⊆ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) )
24 fveq2 ( 𝑎 = 𝐴 → ( 𝐶𝑎 ) = ( 𝐶𝐴 ) )
25 24 eleq2d ( 𝑎 = 𝐴 → ( 𝑖 ∈ ( 𝐶𝑎 ) ↔ 𝑖 ∈ ( 𝐶𝐴 ) ) )
26 fveq2 ( 𝑎 = 𝐴 → ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) = ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) )
27 26 oveq1d ( 𝑎 = 𝐴 → ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑟 ) = ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝑟 ) )
28 27 breq2d ( 𝑎 = 𝐴 → ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑟 ) ↔ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝑟 ) ) )
29 25 28 anbi12d ( 𝑎 = 𝐴 → ( ( 𝑖 ∈ ( 𝐶𝑎 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑟 ) ) ↔ ( 𝑖 ∈ ( 𝐶𝐴 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝑟 ) ) ) )
30 29 rabbidva2 ( 𝑎 = 𝐴 → { 𝑖 ∈ ( 𝐶𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑟 ) } = { 𝑖 ∈ ( 𝐶𝐴 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝑟 ) } )
31 30 mpteq2dv ( 𝑎 = 𝐴 → ( 𝑟 ∈ ℝ+ ↦ { 𝑖 ∈ ( 𝐶𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑟 ) } ) = ( 𝑟 ∈ ℝ+ ↦ { 𝑖 ∈ ( 𝐶𝐴 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝑟 ) } ) )
32 rpex + ∈ V
33 32 mptex ( 𝑟 ∈ ℝ+ ↦ { 𝑖 ∈ ( 𝐶𝐴 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝑟 ) } ) ∈ V
34 33 a1i ( 𝜑 → ( 𝑟 ∈ ℝ+ ↦ { 𝑖 ∈ ( 𝐶𝐴 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝑟 ) } ) ∈ V )
35 6 31 16 34 fvmptd3 ( 𝜑 → ( 𝐷𝐴 ) = ( 𝑟 ∈ ℝ+ ↦ { 𝑖 ∈ ( 𝐶𝐴 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝑟 ) } ) )
36 oveq2 ( 𝑟 = 𝐸 → ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝑟 ) = ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝐸 ) )
37 36 breq2d ( 𝑟 = 𝐸 → ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝑟 ) ↔ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝐸 ) ) )
38 37 rabbidv ( 𝑟 = 𝐸 → { 𝑖 ∈ ( 𝐶𝐴 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝑟 ) } = { 𝑖 ∈ ( 𝐶𝐴 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝐸 ) } )
39 38 adantl ( ( 𝜑𝑟 = 𝐸 ) → { 𝑖 ∈ ( 𝐶𝐴 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝑟 ) } = { 𝑖 ∈ ( 𝐶𝐴 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝐸 ) } )
40 fvex ( 𝐶𝐴 ) ∈ V
41 40 rabex { 𝑖 ∈ ( 𝐶𝐴 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝐸 ) } ∈ V
42 41 a1i ( 𝜑 → { 𝑖 ∈ ( 𝐶𝐴 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝐸 ) } ∈ V )
43 35 39 3 42 fvmptd ( 𝜑 → ( ( 𝐷𝐴 ) ‘ 𝐸 ) = { 𝑖 ∈ ( 𝐶𝐴 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝐸 ) } )
44 7 43 eleqtrd ( 𝜑𝐼 ∈ { 𝑖 ∈ ( 𝐶𝐴 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝐸 ) } )
45 fveq1 ( 𝑖 = 𝐼 → ( 𝑖𝑗 ) = ( 𝐼𝑗 ) )
46 45 fveq2d ( 𝑖 = 𝐼 → ( 𝐿 ‘ ( 𝑖𝑗 ) ) = ( 𝐿 ‘ ( 𝐼𝑗 ) ) )
47 46 mpteq2dv ( 𝑖 = 𝐼 → ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼𝑗 ) ) ) )
48 47 fveq2d ( 𝑖 = 𝐼 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼𝑗 ) ) ) ) )
49 48 breq1d ( 𝑖 = 𝐼 → ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝐸 ) ↔ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝐸 ) ) )
50 49 elrab ( 𝐼 ∈ { 𝑖 ∈ ( 𝐶𝐴 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝐸 ) } ↔ ( 𝐼 ∈ ( 𝐶𝐴 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝐸 ) ) )
51 44 50 sylib ( 𝜑 → ( 𝐼 ∈ ( 𝐶𝐴 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝐸 ) ) )
52 51 simpld ( 𝜑𝐼 ∈ ( 𝐶𝐴 ) )
53 23 52 sseldd ( 𝜑𝐼 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) )
54 elmapi ( 𝐼 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → 𝐼 : ℕ ⟶ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
55 53 54 syl ( 𝜑𝐼 : ℕ ⟶ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
56 55 adantr ( ( 𝜑𝑗 ∈ ℕ ) → 𝐼 : ℕ ⟶ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
57 simpr ( ( 𝜑𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ )
58 56 57 ffvelrnd ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐼𝑗 ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
59 elmapi ( ( 𝐼𝑗 ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) → ( 𝐼𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
60 58 59 syl ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐼𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
61 60 ffvelrnda ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( ( 𝐼𝑗 ) ‘ 𝑘 ) ∈ ( ℝ × ℝ ) )
62 xp1st ( ( ( 𝐼𝑗 ) ‘ 𝑘 ) ∈ ( ℝ × ℝ ) → ( 1st ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ∈ ℝ )
63 61 62 syl ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( 1st ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ∈ ℝ )
64 63 fmpttd ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝑘𝑋 ↦ ( 1st ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) : 𝑋 ⟶ ℝ )
65 reex ℝ ∈ V
66 65 a1i ( 𝜑 → ℝ ∈ V )
67 elmapg ( ( ℝ ∈ V ∧ 𝑋 ∈ Fin ) → ( ( 𝑘𝑋 ↦ ( 1st ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) ∈ ( ℝ ↑m 𝑋 ) ↔ ( 𝑘𝑋 ↦ ( 1st ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) : 𝑋 ⟶ ℝ ) )
68 66 1 67 syl2anc ( 𝜑 → ( ( 𝑘𝑋 ↦ ( 1st ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) ∈ ( ℝ ↑m 𝑋 ) ↔ ( 𝑘𝑋 ↦ ( 1st ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) : 𝑋 ⟶ ℝ ) )
69 68 adantr ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝑘𝑋 ↦ ( 1st ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) ∈ ( ℝ ↑m 𝑋 ) ↔ ( 𝑘𝑋 ↦ ( 1st ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) : 𝑋 ⟶ ℝ ) )
70 64 69 mpbird ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝑘𝑋 ↦ ( 1st ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) ∈ ( ℝ ↑m 𝑋 ) )
71 70 fmpttd ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( 𝑘𝑋 ↦ ( 1st ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) ) : ℕ ⟶ ( ℝ ↑m 𝑋 ) )
72 8 a1i ( 𝜑𝐵 = ( 𝑗 ∈ ℕ ↦ ( 𝑘𝑋 ↦ ( 1st ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) ) )
73 72 feq1d ( 𝜑 → ( 𝐵 : ℕ ⟶ ( ℝ ↑m 𝑋 ) ↔ ( 𝑗 ∈ ℕ ↦ ( 𝑘𝑋 ↦ ( 1st ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) ) : ℕ ⟶ ( ℝ ↑m 𝑋 ) ) )
74 71 73 mpbird ( 𝜑𝐵 : ℕ ⟶ ( ℝ ↑m 𝑋 ) )
75 xp2nd ( ( ( 𝐼𝑗 ) ‘ 𝑘 ) ∈ ( ℝ × ℝ ) → ( 2nd ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ∈ ℝ )
76 61 75 syl ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( 2nd ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ∈ ℝ )
77 76 fmpttd ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝑘𝑋 ↦ ( 2nd ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) : 𝑋 ⟶ ℝ )
78 elmapg ( ( ℝ ∈ V ∧ 𝑋 ∈ Fin ) → ( ( 𝑘𝑋 ↦ ( 2nd ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) ∈ ( ℝ ↑m 𝑋 ) ↔ ( 𝑘𝑋 ↦ ( 2nd ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) : 𝑋 ⟶ ℝ ) )
79 66 1 78 syl2anc ( 𝜑 → ( ( 𝑘𝑋 ↦ ( 2nd ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) ∈ ( ℝ ↑m 𝑋 ) ↔ ( 𝑘𝑋 ↦ ( 2nd ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) : 𝑋 ⟶ ℝ ) )
80 79 adantr ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝑘𝑋 ↦ ( 2nd ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) ∈ ( ℝ ↑m 𝑋 ) ↔ ( 𝑘𝑋 ↦ ( 2nd ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) : 𝑋 ⟶ ℝ ) )
81 77 80 mpbird ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝑘𝑋 ↦ ( 2nd ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) ∈ ( ℝ ↑m 𝑋 ) )
82 81 fmpttd ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( 𝑘𝑋 ↦ ( 2nd ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) ) : ℕ ⟶ ( ℝ ↑m 𝑋 ) )
83 9 a1i ( 𝜑𝑇 = ( 𝑗 ∈ ℕ ↦ ( 𝑘𝑋 ↦ ( 2nd ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) ) )
84 83 feq1d ( 𝜑 → ( 𝑇 : ℕ ⟶ ( ℝ ↑m 𝑋 ) ↔ ( 𝑗 ∈ ℕ ↦ ( 𝑘𝑋 ↦ ( 2nd ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) ) : ℕ ⟶ ( ℝ ↑m 𝑋 ) ) )
85 82 84 mpbird ( 𝜑𝑇 : ℕ ⟶ ( ℝ ↑m 𝑋 ) )
86 74 85 jca ( 𝜑 → ( 𝐵 : ℕ ⟶ ( ℝ ↑m 𝑋 ) ∧ 𝑇 : ℕ ⟶ ( ℝ ↑m 𝑋 ) ) )
87 52 20 eleqtrd ( 𝜑𝐼 ∈ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝐴 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } )
88 fveq1 ( 𝑙 = 𝐼 → ( 𝑙𝑗 ) = ( 𝐼𝑗 ) )
89 88 coeq2d ( 𝑙 = 𝐼 → ( [,) ∘ ( 𝑙𝑗 ) ) = ( [,) ∘ ( 𝐼𝑗 ) ) )
90 89 fveq1d ( 𝑙 = 𝐼 → ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) = ( ( [,) ∘ ( 𝐼𝑗 ) ) ‘ 𝑘 ) )
91 90 ixpeq2dv ( 𝑙 = 𝐼X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) = X 𝑘𝑋 ( ( [,) ∘ ( 𝐼𝑗 ) ) ‘ 𝑘 ) )
92 91 adantr ( ( 𝑙 = 𝐼𝑗 ∈ ℕ ) → X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) = X 𝑘𝑋 ( ( [,) ∘ ( 𝐼𝑗 ) ) ‘ 𝑘 ) )
93 92 iuneq2dv ( 𝑙 = 𝐼 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) = 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝐼𝑗 ) ) ‘ 𝑘 ) )
94 93 sseq2d ( 𝑙 = 𝐼 → ( 𝐴 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) ↔ 𝐴 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝐼𝑗 ) ) ‘ 𝑘 ) ) )
95 94 elrab ( 𝐼 ∈ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝐴 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } ↔ ( 𝐼 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝐴 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝐼𝑗 ) ) ‘ 𝑘 ) ) )
96 87 95 sylib ( 𝜑 → ( 𝐼 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝐴 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝐼𝑗 ) ) ‘ 𝑘 ) ) )
97 96 simprd ( 𝜑𝐴 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝐼𝑗 ) ) ‘ 𝑘 ) )
98 60 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( 𝐼𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
99 simpr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑋 ) → 𝑘𝑋 )
100 98 99 fvovco ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( ( [,) ∘ ( 𝐼𝑗 ) ) ‘ 𝑘 ) = ( ( 1st ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) )
101 mptexg ( 𝑋 ∈ Fin → ( 𝑘𝑋 ↦ ( 1st ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) ∈ V )
102 1 101 syl ( 𝜑 → ( 𝑘𝑋 ↦ ( 1st ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) ∈ V )
103 102 adantr ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝑘𝑋 ↦ ( 1st ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) ∈ V )
104 72 103 fvmpt2d ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐵𝑗 ) = ( 𝑘𝑋 ↦ ( 1st ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) )
105 fvexd ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( 1st ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ∈ V )
106 104 105 fvmpt2d ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( ( 𝐵𝑗 ) ‘ 𝑘 ) = ( 1st ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) )
107 106 eqcomd ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( 1st ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) = ( ( 𝐵𝑗 ) ‘ 𝑘 ) )
108 mptexg ( 𝑋 ∈ Fin → ( 𝑘𝑋 ↦ ( 2nd ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) ∈ V )
109 1 108 syl ( 𝜑 → ( 𝑘𝑋 ↦ ( 2nd ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) ∈ V )
110 109 adantr ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝑘𝑋 ↦ ( 2nd ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) ∈ V )
111 83 110 fvmpt2d ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝑇𝑗 ) = ( 𝑘𝑋 ↦ ( 2nd ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) )
112 fvexd ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( 2nd ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ∈ V )
113 111 112 fvmpt2d ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( ( 𝑇𝑗 ) ‘ 𝑘 ) = ( 2nd ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) )
114 113 eqcomd ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( 2nd ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) = ( ( 𝑇𝑗 ) ‘ 𝑘 ) )
115 107 114 oveq12d ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( ( 1st ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) = ( ( ( 𝐵𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇𝑗 ) ‘ 𝑘 ) ) )
116 100 115 eqtrd ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( ( [,) ∘ ( 𝐼𝑗 ) ) ‘ 𝑘 ) = ( ( ( 𝐵𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇𝑗 ) ‘ 𝑘 ) ) )
117 116 ixpeq2dva ( ( 𝜑𝑗 ∈ ℕ ) → X 𝑘𝑋 ( ( [,) ∘ ( 𝐼𝑗 ) ) ‘ 𝑘 ) = X 𝑘𝑋 ( ( ( 𝐵𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇𝑗 ) ‘ 𝑘 ) ) )
118 117 iuneq2dv ( 𝜑 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝐼𝑗 ) ) ‘ 𝑘 ) = 𝑗 ∈ ℕ X 𝑘𝑋 ( ( ( 𝐵𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇𝑗 ) ‘ 𝑘 ) ) )
119 97 118 sseqtrd ( 𝜑𝐴 𝑗 ∈ ℕ X 𝑘𝑋 ( ( ( 𝐵𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇𝑗 ) ‘ 𝑘 ) ) )
120 5 a1i ( ( 𝜑𝑗 ∈ ℕ ) → 𝐿 = ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) ) )
121 coeq2 ( = ( 𝐼𝑗 ) → ( [,) ∘ ) = ( [,) ∘ ( 𝐼𝑗 ) ) )
122 121 fveq1d ( = ( 𝐼𝑗 ) → ( ( [,) ∘ ) ‘ 𝑘 ) = ( ( [,) ∘ ( 𝐼𝑗 ) ) ‘ 𝑘 ) )
123 122 ad2antlr ( ( ( 𝜑 = ( 𝐼𝑗 ) ) ∧ 𝑘𝑋 ) → ( ( [,) ∘ ) ‘ 𝑘 ) = ( ( [,) ∘ ( 𝐼𝑗 ) ) ‘ 𝑘 ) )
124 123 adantllr ( ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ = ( 𝐼𝑗 ) ) ∧ 𝑘𝑋 ) → ( ( [,) ∘ ) ‘ 𝑘 ) = ( ( [,) ∘ ( 𝐼𝑗 ) ) ‘ 𝑘 ) )
125 100 adantlr ( ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ = ( 𝐼𝑗 ) ) ∧ 𝑘𝑋 ) → ( ( [,) ∘ ( 𝐼𝑗 ) ) ‘ 𝑘 ) = ( ( 1st ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) )
126 115 adantlr ( ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ = ( 𝐼𝑗 ) ) ∧ 𝑘𝑋 ) → ( ( 1st ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) = ( ( ( 𝐵𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇𝑗 ) ‘ 𝑘 ) ) )
127 124 125 126 3eqtrd ( ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ = ( 𝐼𝑗 ) ) ∧ 𝑘𝑋 ) → ( ( [,) ∘ ) ‘ 𝑘 ) = ( ( ( 𝐵𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇𝑗 ) ‘ 𝑘 ) ) )
128 127 fveq2d ( ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ = ( 𝐼𝑗 ) ) ∧ 𝑘𝑋 ) → ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) = ( vol ‘ ( ( ( 𝐵𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇𝑗 ) ‘ 𝑘 ) ) ) )
129 128 prodeq2dv ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ = ( 𝐼𝑗 ) ) → ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) = ∏ 𝑘𝑋 ( vol ‘ ( ( ( 𝐵𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇𝑗 ) ‘ 𝑘 ) ) ) )
130 1 adantr ( ( 𝜑𝑗 ∈ ℕ ) → 𝑋 ∈ Fin )
131 8 fvmpt2 ( ( 𝑗 ∈ ℕ ∧ ( 𝑘𝑋 ↦ ( 1st ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) ∈ V ) → ( 𝐵𝑗 ) = ( 𝑘𝑋 ↦ ( 1st ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) )
132 57 103 131 syl2anc ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐵𝑗 ) = ( 𝑘𝑋 ↦ ( 1st ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) )
133 132 feq1d ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐵𝑗 ) : 𝑋 ⟶ ℝ ↔ ( 𝑘𝑋 ↦ ( 1st ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) : 𝑋 ⟶ ℝ ) )
134 64 133 mpbird ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐵𝑗 ) : 𝑋 ⟶ ℝ )
135 134 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( 𝐵𝑗 ) : 𝑋 ⟶ ℝ )
136 135 99 ffvelrnd ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( ( 𝐵𝑗 ) ‘ 𝑘 ) ∈ ℝ )
137 9 fvmpt2 ( ( 𝑗 ∈ ℕ ∧ ( 𝑘𝑋 ↦ ( 2nd ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) ∈ V ) → ( 𝑇𝑗 ) = ( 𝑘𝑋 ↦ ( 2nd ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) )
138 57 110 137 syl2anc ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝑇𝑗 ) = ( 𝑘𝑋 ↦ ( 2nd ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) )
139 138 feq1d ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝑇𝑗 ) : 𝑋 ⟶ ℝ ↔ ( 𝑘𝑋 ↦ ( 2nd ‘ ( ( 𝐼𝑗 ) ‘ 𝑘 ) ) ) : 𝑋 ⟶ ℝ ) )
140 77 139 mpbird ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝑇𝑗 ) : 𝑋 ⟶ ℝ )
141 140 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( 𝑇𝑗 ) : 𝑋 ⟶ ℝ )
142 141 99 ffvelrnd ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( ( 𝑇𝑗 ) ‘ 𝑘 ) ∈ ℝ )
143 volicore ( ( ( ( 𝐵𝑗 ) ‘ 𝑘 ) ∈ ℝ ∧ ( ( 𝑇𝑗 ) ‘ 𝑘 ) ∈ ℝ ) → ( vol ‘ ( ( ( 𝐵𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇𝑗 ) ‘ 𝑘 ) ) ) ∈ ℝ )
144 136 142 143 syl2anc ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( vol ‘ ( ( ( 𝐵𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇𝑗 ) ‘ 𝑘 ) ) ) ∈ ℝ )
145 130 144 fprodrecl ( ( 𝜑𝑗 ∈ ℕ ) → ∏ 𝑘𝑋 ( vol ‘ ( ( ( 𝐵𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇𝑗 ) ‘ 𝑘 ) ) ) ∈ ℝ )
146 120 129 58 145 fvmptd ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐿 ‘ ( 𝐼𝑗 ) ) = ∏ 𝑘𝑋 ( vol ‘ ( ( ( 𝐵𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇𝑗 ) ‘ 𝑘 ) ) ) )
147 146 eqcomd ( ( 𝜑𝑗 ∈ ℕ ) → ∏ 𝑘𝑋 ( vol ‘ ( ( ( 𝐵𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇𝑗 ) ‘ 𝑘 ) ) ) = ( 𝐿 ‘ ( 𝐼𝑗 ) ) )
148 147 mpteq2dva ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( ( 𝐵𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇𝑗 ) ‘ 𝑘 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼𝑗 ) ) ) )
149 148 fveq2d ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( ( 𝐵𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇𝑗 ) ‘ 𝑘 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼𝑗 ) ) ) ) )
150 51 simprd ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝐸 ) )
151 149 150 eqbrtrd ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( ( 𝐵𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇𝑗 ) ‘ 𝑘 ) ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝐸 ) )
152 86 119 151 jca31 ( 𝜑 → ( ( ( 𝐵 : ℕ ⟶ ( ℝ ↑m 𝑋 ) ∧ 𝑇 : ℕ ⟶ ( ℝ ↑m 𝑋 ) ) ∧ 𝐴 𝑗 ∈ ℕ X 𝑘𝑋 ( ( ( 𝐵𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇𝑗 ) ‘ 𝑘 ) ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( ( 𝐵𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇𝑗 ) ‘ 𝑘 ) ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝐸 ) ) )