Metamath Proof Explorer

Theorem ovnovollem2

Description: if I is a cover of ( B ^m { A } ) in RR^ 1 , then F is the corresponding cover in the reals. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses ovnovollem2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
ovnovollem2.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
ovnovollem2.i ⊢ ( 𝜑 → 𝐼 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) )
ovnovollem2.s ⊢ ( 𝜑 → ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) )
ovnovollem2.z ⊢ ( 𝜑 → 𝑍 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
ovnovollem2.f ⊢ 𝐹 = ( 𝑗 ∈ ℕ ↦ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝐴 ) )
Assertion ovnovollem2 ( 𝜑 → ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑍 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) )

Proof

Step Hyp Ref Expression
1 ovnovollem2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 ovnovollem2.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3 ovnovollem2.i ⊢ ( 𝜑 → 𝐼 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) )
4 ovnovollem2.s ⊢ ( 𝜑 → ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) )
5 ovnovollem2.z ⊢ ( 𝜑 → 𝑍 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
6 ovnovollem2.f ⊢ 𝐹 = ( 𝑗 ∈ ℕ ↦ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝐴 ) )
7 elmapi ⊢ ( 𝐼 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) → 𝐼 : ℕ ⟶ ( ( ℝ × ℝ ) ↑m { 𝐴 } ) )
8 3 7 syl ⊢ ( 𝜑 → 𝐼 : ℕ ⟶ ( ( ℝ × ℝ ) ↑m { 𝐴 } ) )
9 8 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝐼 : ℕ ⟶ ( ( ℝ × ℝ ) ↑m { 𝐴 } ) )
10 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ )
11 9 10 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐼 ‘ 𝑗 ) ∈ ( ( ℝ × ℝ ) ↑m { 𝐴 } ) )
12 elmapi ⊢ ( ( 𝐼 ‘ 𝑗 ) ∈ ( ( ℝ × ℝ ) ↑m { 𝐴 } ) → ( 𝐼 ‘ 𝑗 ) : { 𝐴 } ⟶ ( ℝ × ℝ ) )
13 11 12 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐼 ‘ 𝑗 ) : { 𝐴 } ⟶ ( ℝ × ℝ ) )
14 snidg ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 } )
15 1 14 syl ⊢ ( 𝜑 → 𝐴 ∈ { 𝐴 } )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝐴 ∈ { 𝐴 } )
17 13 16 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐼 ‘ 𝑗 ) ‘ 𝐴 ) ∈ ( ℝ × ℝ ) )
18 17 6 fmptd ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ℝ × ℝ ) )
19 reex ⊢ ℝ ∈ V
20 19 19 xpex ⊢ ( ℝ × ℝ ) ∈ V
21 nnex ⊢ ℕ ∈ V
22 20 21 elmap ⊢ ( 𝐹 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ↔ 𝐹 : ℕ ⟶ ( ℝ × ℝ ) )
23 22 a1i ⊢ ( 𝜑 → ( 𝐹 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ↔ 𝐹 : ℕ ⟶ ( ℝ × ℝ ) ) )
24 18 23 mpbird ⊢ ( 𝜑 → 𝐹 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) )
25 elsni ⊢ ( 𝑘 ∈ { 𝐴 } → 𝑘 = 𝐴 )
26 25 fveq2d ⊢ ( 𝑘 ∈ { 𝐴 } → ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝐴 ) )
27 26 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ { 𝐴 } ) → ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝐴 ) )
28 elmapfun ⊢ ( ( 𝐼 ‘ 𝑗 ) ∈ ( ( ℝ × ℝ ) ↑m { 𝐴 } ) → Fun ( 𝐼 ‘ 𝑗 ) )
29 11 28 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → Fun ( 𝐼 ‘ 𝑗 ) )
30 13 fdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → dom ( 𝐼 ‘ 𝑗 ) = { 𝐴 } )
31 30 eqcomd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → { 𝐴 } = dom ( 𝐼 ‘ 𝑗 ) )
32 16 31 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝐴 ∈ dom ( 𝐼 ‘ 𝑗 ) )
33 fvco ⊢ ( ( Fun ( 𝐼 ‘ 𝑗 ) ∧ 𝐴 ∈ dom ( 𝐼 ‘ 𝑗 ) ) → ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝐴 ) = ( [,) ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝐴 ) ) )
34 29 32 33 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝐴 ) = ( [,) ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝐴 ) ) )
35 34 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ { 𝐴 } ) → ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝐴 ) = ( [,) ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝐴 ) ) )
36 id ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℕ )
37 fvexd ⊢ ( 𝑗 ∈ ℕ → ( ( 𝐼 ‘ 𝑗 ) ‘ 𝐴 ) ∈ V )
38 6 fvmpt2 ⊢ ( ( 𝑗 ∈ ℕ ∧ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝐴 ) ∈ V ) → ( 𝐹 ‘ 𝑗 ) = ( ( 𝐼 ‘ 𝑗 ) ‘ 𝐴 ) )
39 36 37 38 syl2anc ⊢ ( 𝑗 ∈ ℕ → ( 𝐹 ‘ 𝑗 ) = ( ( 𝐼 ‘ 𝑗 ) ‘ 𝐴 ) )
40 39 eqcomd ⊢ ( 𝑗 ∈ ℕ → ( ( 𝐼 ‘ 𝑗 ) ‘ 𝐴 ) = ( 𝐹 ‘ 𝑗 ) )
41 40 fveq2d ⊢ ( 𝑗 ∈ ℕ → ( [,) ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝐴 ) ) = ( [,) ‘ ( 𝐹 ‘ 𝑗 ) ) )
42 41 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( [,) ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝐴 ) ) = ( [,) ‘ ( 𝐹 ‘ 𝑗 ) ) )
43 18 ffund ⊢ ( 𝜑 → Fun 𝐹 )
44 43 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → Fun 𝐹 )
45 6 17 dmmptd ⊢ ( 𝜑 → dom 𝐹 = ℕ )
46 45 eqcomd ⊢ ( 𝜑 → ℕ = dom 𝐹 )
47 46 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ℕ = dom 𝐹 )
48 10 47 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ dom 𝐹 )
49 fvco ⊢ ( ( Fun 𝐹 ∧ 𝑗 ∈ dom 𝐹 ) → ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) = ( [,) ‘ ( 𝐹 ‘ 𝑗 ) ) )
50 44 48 49 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) = ( [,) ‘ ( 𝐹 ‘ 𝑗 ) ) )
51 50 eqcomd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( [,) ‘ ( 𝐹 ‘ 𝑗 ) ) = ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) )
52 42 51 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( [,) ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝐴 ) ) = ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) )
53 52 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ { 𝐴 } ) → ( [,) ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝐴 ) ) = ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) )
54 27 35 53 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ { 𝐴 } ) → ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) )
55 54 ixpeq2dva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) = X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) )
56 snex ⊢ { 𝐴 } ∈ V
57 fvex ⊢ ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) ∈ V
58 56 57 ixpconst ⊢ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) = ( ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) ↑m { 𝐴 } )
59 58 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) = ( ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) ↑m { 𝐴 } ) )
60 55 59 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) ↑m { 𝐴 } ) )
61 60 iuneq2dv ⊢ ( 𝜑 → ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) = ∪ 𝑗 ∈ ℕ ( ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) ↑m { 𝐴 } ) )
62 nfv ⊢ Ⅎ 𝑗 𝜑
63 21 a1i ⊢ ( 𝜑 → ℕ ∈ V )
64 fvexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) ∈ V )
65 62 63 64 1 iunmapsn ⊢ ( 𝜑 → ∪ 𝑗 ∈ ℕ ( ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) ↑m { 𝐴 } ) = ( ∪ 𝑗 ∈ ℕ ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) ↑m { 𝐴 } ) )
66 61 65 eqtrd ⊢ ( 𝜑 → ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ∪ 𝑗 ∈ ℕ ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) ↑m { 𝐴 } ) )
67 4 66 sseqtrd ⊢ ( 𝜑 → ( 𝐵 ↑m { 𝐴 } ) ⊆ ( ∪ 𝑗 ∈ ℕ ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) ↑m { 𝐴 } ) )
68 21 57 iunex ⊢ ∪ 𝑗 ∈ ℕ ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) ∈ V
69 68 a1i ⊢ ( 𝜑 → ∪ 𝑗 ∈ ℕ ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) ∈ V )
70 56 a1i ⊢ ( 𝜑 → { 𝐴 } ∈ V )
71 15 ne0d ⊢ ( 𝜑 → { 𝐴 } ≠ ∅ )
72 2 69 70 71 mapss2 ⊢ ( 𝜑 → ( 𝐵 ⊆ ∪ 𝑗 ∈ ℕ ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) ↔ ( 𝐵 ↑m { 𝐴 } ) ⊆ ( ∪ 𝑗 ∈ ℕ ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) ↑m { 𝐴 } ) ) )
73 67 72 mpbird ⊢ ( 𝜑 → 𝐵 ⊆ ∪ 𝑗 ∈ ℕ ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) )
74 icof ⊢ [,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ*
75 74 a1i ⊢ ( 𝜑 → [,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ* )
76 rexpssxrxp ⊢ ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* )
77 76 a1i ⊢ ( 𝜑 → ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* ) )
78 75 77 18 fcoss ⊢ ( 𝜑 → ( [,) ∘ 𝐹 ) : ℕ ⟶ 𝒫 ℝ* )
79 78 ffnd ⊢ ( 𝜑 → ( [,) ∘ 𝐹 ) Fn ℕ )
80 fniunfv ⊢ ( ( [,) ∘ 𝐹 ) Fn ℕ → ∪ 𝑗 ∈ ℕ ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) = ∪ ran ( [,) ∘ 𝐹 ) )
81 79 80 syl ⊢ ( 𝜑 → ∪ 𝑗 ∈ ℕ ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) = ∪ ran ( [,) ∘ 𝐹 ) )
82 73 81 sseqtrd ⊢ ( 𝜑 → 𝐵 ⊆ ∪ ran ( [,) ∘ 𝐹 ) )
83 nfcv ⊢ Ⅎ 𝑗 𝐹
84 ressxr ⊢ ℝ ⊆ ℝ*
85 xpss2 ⊢ ( ℝ ⊆ ℝ* → ( ℝ × ℝ ) ⊆ ( ℝ × ℝ* ) )
86 84 85 ax-mp ⊢ ( ℝ × ℝ ) ⊆ ( ℝ × ℝ* )
87 86 a1i ⊢ ( 𝜑 → ( ℝ × ℝ ) ⊆ ( ℝ × ℝ* ) )
88 18 87 fssd ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ℝ × ℝ* ) )
89 83 88 volicofmpt ⊢ ( 𝜑 → ( ( vol ∘ [,) ) ∘ 𝐹 ) = ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ) ) ) )
90 1 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝐴 ∈ 𝑉 )
91 fvexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐼 ‘ 𝑗 ) ‘ 𝐴 ) ∈ V )
92 10 91 38 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) = ( ( 𝐼 ‘ 𝑗 ) ‘ 𝐴 ) )
93 92 17 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) ∈ ( ℝ × ℝ ) )
94 1st2nd2 ⊢ ( ( 𝐹 ‘ 𝑗 ) ∈ ( ℝ × ℝ ) → ( 𝐹 ‘ 𝑗 ) = ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ⟩ )
95 93 94 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) = ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ⟩ )
96 95 fveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( [,) ‘ ( 𝐹 ‘ 𝑗 ) ) = ( [,) ‘ ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ⟩ ) )
97 df-ov ⊢ ( ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ) = ( [,) ‘ ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ⟩ )
98 97 eqcomi ⊢ ( [,) ‘ ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ⟩ ) = ( ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) )
99 98 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( [,) ‘ ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ⟩ ) = ( ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ) )
100 50 96 99 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) = ( ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ) )
101 34 52 100 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝐴 ) = ( ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ) )
102 101 fveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝐴 ) ) = ( vol ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ) ) )
103 xp1st ⊢ ( ( 𝐹 ‘ 𝑗 ) ∈ ( ℝ × ℝ ) → ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ )
104 93 103 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ )
105 xp2nd ⊢ ( ( 𝐹 ‘ 𝑗 ) ∈ ( ℝ × ℝ ) → ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ )
106 93 105 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ )
107 volicore ⊢ ( ( ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ ) → ( vol ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ) ) ∈ ℝ )
108 104 106 107 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ) ) ∈ ℝ )
109 102 108 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝐴 ) ) ∈ ℝ )
110 109 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝐴 ) ) ∈ ℂ )
111 2fveq3 ⊢ ( 𝑘 = 𝐴 → ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝐴 ) ) )
112 111 prodsn ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝐴 ) ) ∈ ℂ ) → ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝐴 ) ) )
113 90 110 112 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝐴 ) ) )
114 113 102 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ) ) = ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
115 114 mpteq2dva ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) )
116 89 115 eqtrd ⊢ ( 𝜑 → ( ( vol ∘ [,) ) ∘ 𝐹 ) = ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) )
117 116 fveq2d ⊢ ( 𝜑 → ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝐹 ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
118 5 117 eqtr4d ⊢ ( 𝜑 → 𝑍 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝐹 ) ) )
119 82 118 jca ⊢ ( 𝜑 → ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝐹 ) ∧ 𝑍 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝐹 ) ) ) )
120 coeq2 ⊢ ( 𝑓 = 𝐹 → ( [,) ∘ 𝑓 ) = ( [,) ∘ 𝐹 ) )
121 120 rneqd ⊢ ( 𝑓 = 𝐹 → ran ( [,) ∘ 𝑓 ) = ran ( [,) ∘ 𝐹 ) )
122 121 unieqd ⊢ ( 𝑓 = 𝐹 → ∪ ran ( [,) ∘ 𝑓 ) = ∪ ran ( [,) ∘ 𝐹 ) )
123 122 sseq2d ⊢ ( 𝑓 = 𝐹 → ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ↔ 𝐵 ⊆ ∪ ran ( [,) ∘ 𝐹 ) ) )
124 coeq2 ⊢ ( 𝑓 = 𝐹 → ( ( vol ∘ [,) ) ∘ 𝑓 ) = ( ( vol ∘ [,) ) ∘ 𝐹 ) )
125 124 fveq2d ⊢ ( 𝑓 = 𝐹 → ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝐹 ) ) )
126 125 eqeq2d ⊢ ( 𝑓 = 𝐹 → ( 𝑍 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ↔ 𝑍 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝐹 ) ) ) )
127 123 126 anbi12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑍 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ↔ ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝐹 ) ∧ 𝑍 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝐹 ) ) ) ) )
128 127 rspcev ⊢ ( ( 𝐹 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ∧ ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝐹 ) ∧ 𝑍 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝐹 ) ) ) ) → ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑍 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) )
129 24 119 128 syl2anc ⊢ ( 𝜑 → ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑍 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) )