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 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐼 ‘ 𝑗 ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
59 elmapi ⊢ ( ( 𝐼 ‘ 𝑗 ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) → ( 𝐼 ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
60 58 59 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐼 ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
61 60 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑘 ) ∈ ( ℝ × ℝ ) )
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 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐵 ‘ 𝑗 ) ‘ 𝑘 ) ∈ ℝ )
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 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝑇 ‘ 𝑗 ) ‘ 𝑘 ) ∈ ℝ )
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* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝐸 ) ) )