Metamath Proof Explorer

Theorem ovnovollem1

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

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

Proof

Step Hyp Ref Expression
1 ovnovollem1.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 ovnovollem1.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) )
3 ovnovollem1.i ⊢ 𝐼 = ( 𝑗 ∈ ℕ ↦ { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } )
4 ovnovollem1.s ⊢ ( 𝜑 → 𝐵 ⊆ ∪ ran ( [,) ∘ 𝐹 ) )
5 ovnovollem1.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
6 ovnovollem1.z ⊢ ( 𝜑 → 𝑍 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝐹 ) ) )
7 eqidd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } = { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } )
8 1 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝐴 ∈ 𝑉 )
9 elmapi ⊢ ( 𝐹 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → 𝐹 : ℕ ⟶ ( ℝ × ℝ ) )
10 2 9 syl ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ℝ × ℝ ) )
11 10 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) ∈ ( ℝ × ℝ ) )
12 fsng ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝑗 ) ∈ ( ℝ × ℝ ) ) → ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } : { 𝐴 } ⟶ { ( 𝐹 ‘ 𝑗 ) } ↔ { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } = { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } ) )
13 8 11 12 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } : { 𝐴 } ⟶ { ( 𝐹 ‘ 𝑗 ) } ↔ { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } = { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } ) )
14 7 13 mpbird ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } : { 𝐴 } ⟶ { ( 𝐹 ‘ 𝑗 ) } )
15 11 snssd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → { ( 𝐹 ‘ 𝑗 ) } ⊆ ( ℝ × ℝ ) )
16 14 15 fssd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } : { 𝐴 } ⟶ ( ℝ × ℝ ) )
17 reex ⊢ ℝ ∈ V
18 17 17 xpex ⊢ ( ℝ × ℝ ) ∈ V
19 18 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ℝ × ℝ ) ∈ V )
20 snex ⊢ { 𝐴 } ∈ V
21 20 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → { 𝐴 } ∈ V )
22 19 21 elmapd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } ∈ ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↔ { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } : { 𝐴 } ⟶ ( ℝ × ℝ ) ) )
23 16 22 mpbird ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } ∈ ( ( ℝ × ℝ ) ↑m { 𝐴 } ) )
24 23 3 fmptd ⊢ ( 𝜑 → 𝐼 : ℕ ⟶ ( ( ℝ × ℝ ) ↑m { 𝐴 } ) )
25 ovexd ⊢ ( 𝜑 → ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ∈ V )
26 nnex ⊢ ℕ ∈ V
27 26 a1i ⊢ ( 𝜑 → ℕ ∈ V )
28 25 27 elmapd ⊢ ( 𝜑 → ( 𝐼 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ↔ 𝐼 : ℕ ⟶ ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ) )
29 24 28 mpbird ⊢ ( 𝜑 → 𝐼 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) )
30 icof ⊢ [,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ*
31 30 a1i ⊢ ( 𝜑 → [,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ* )
32 rexpssxrxp ⊢ ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* )
33 32 a1i ⊢ ( 𝜑 → ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* ) )
34 31 33 10 fcoss ⊢ ( 𝜑 → ( [,) ∘ 𝐹 ) : ℕ ⟶ 𝒫 ℝ* )
35 34 ffnd ⊢ ( 𝜑 → ( [,) ∘ 𝐹 ) Fn ℕ )
36 fniunfv ⊢ ( ( [,) ∘ 𝐹 ) Fn ℕ → ∪ 𝑗 ∈ ℕ ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) = ∪ ran ( [,) ∘ 𝐹 ) )
37 35 36 syl ⊢ ( 𝜑 → ∪ 𝑗 ∈ ℕ ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) = ∪ ran ( [,) ∘ 𝐹 ) )
38 37 eqcomd ⊢ ( 𝜑 → ∪ ran ( [,) ∘ 𝐹 ) = ∪ 𝑗 ∈ ℕ ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) )
39 4 38 sseqtrd ⊢ ( 𝜑 → 𝐵 ⊆ ∪ 𝑗 ∈ ℕ ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) )
40 fvex ⊢ ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) ∈ V
41 26 40 iunex ⊢ ∪ 𝑗 ∈ ℕ ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) ∈ V
42 41 a1i ⊢ ( 𝜑 → ∪ 𝑗 ∈ ℕ ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) ∈ V )
43 20 a1i ⊢ ( 𝜑 → { 𝐴 } ∈ V )
44 1 snn0d ⊢ ( 𝜑 → { 𝐴 } ≠ ∅ )
45 5 42 43 44 mapss2 ⊢ ( 𝜑 → ( 𝐵 ⊆ ∪ 𝑗 ∈ ℕ ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) ↔ ( 𝐵 ↑m { 𝐴 } ) ⊆ ( ∪ 𝑗 ∈ ℕ ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) ↑m { 𝐴 } ) ) )
46 39 45 mpbid ⊢ ( 𝜑 → ( 𝐵 ↑m { 𝐴 } ) ⊆ ( ∪ 𝑗 ∈ ℕ ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) ↑m { 𝐴 } ) )
47 nfv ⊢ Ⅎ 𝑗 𝜑
48 fvexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( [,) ‘ ( 𝐹 ‘ 𝑗 ) ) ∈ V )
49 47 27 48 1 iunmapsn ⊢ ( 𝜑 → ∪ 𝑗 ∈ ℕ ( ( [,) ‘ ( 𝐹 ‘ 𝑗 ) ) ↑m { 𝐴 } ) = ( ∪ 𝑗 ∈ ℕ ( [,) ‘ ( 𝐹 ‘ 𝑗 ) ) ↑m { 𝐴 } ) )
50 49 eqcomd ⊢ ( 𝜑 → ( ∪ 𝑗 ∈ ℕ ( [,) ‘ ( 𝐹 ‘ 𝑗 ) ) ↑m { 𝐴 } ) = ∪ 𝑗 ∈ ℕ ( ( [,) ‘ ( 𝐹 ‘ 𝑗 ) ) ↑m { 𝐴 } ) )
51 elmapfun ⊢ ( 𝐹 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) → Fun 𝐹 )
52 2 51 syl ⊢ ( 𝜑 → Fun 𝐹 )
53 52 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → Fun 𝐹 )
54 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ )
55 10 fdmd ⊢ ( 𝜑 → dom 𝐹 = ℕ )
56 55 eqcomd ⊢ ( 𝜑 → ℕ = dom 𝐹 )
57 56 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ℕ = dom 𝐹 )
58 54 57 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ dom 𝐹 )
59 fvco ⊢ ( ( Fun 𝐹 ∧ 𝑗 ∈ dom 𝐹 ) → ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) = ( [,) ‘ ( 𝐹 ‘ 𝑗 ) ) )
60 53 58 59 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) = ( [,) ‘ ( 𝐹 ‘ 𝑗 ) ) )
61 60 iuneq2dv ⊢ ( 𝜑 → ∪ 𝑗 ∈ ℕ ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) = ∪ 𝑗 ∈ ℕ ( [,) ‘ ( 𝐹 ‘ 𝑗 ) ) )
62 61 oveq1d ⊢ ( 𝜑 → ( ∪ 𝑗 ∈ ℕ ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) ↑m { 𝐴 } ) = ( ∪ 𝑗 ∈ ℕ ( [,) ‘ ( 𝐹 ‘ 𝑗 ) ) ↑m { 𝐴 } ) )
63 14 ffund ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → Fun { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } )
64 id ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℕ )
65 snex ⊢ { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } ∈ V
66 65 a1i ⊢ ( 𝑗 ∈ ℕ → { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } ∈ V )
67 3 fvmpt2 ⊢ ( ( 𝑗 ∈ ℕ ∧ { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } ∈ V ) → ( 𝐼 ‘ 𝑗 ) = { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } )
68 64 66 67 syl2anc ⊢ ( 𝑗 ∈ ℕ → ( 𝐼 ‘ 𝑗 ) = { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } )
69 68 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐼 ‘ 𝑗 ) = { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } )
70 69 funeqd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( Fun ( 𝐼 ‘ 𝑗 ) ↔ Fun { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } ) )
71 63 70 mpbird ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → Fun ( 𝐼 ‘ 𝑗 ) )
72 71 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ { 𝐴 } ) → Fun ( 𝐼 ‘ 𝑗 ) )
73 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ { 𝐴 } ) → 𝑘 ∈ { 𝐴 } )
74 69 dmeqd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → dom ( 𝐼 ‘ 𝑗 ) = dom { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } )
75 14 fdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → dom { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } = { 𝐴 } )
76 74 75 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → dom ( 𝐼 ‘ 𝑗 ) = { 𝐴 } )
77 76 eleq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑘 ∈ dom ( 𝐼 ‘ 𝑗 ) ↔ 𝑘 ∈ { 𝐴 } ) )
78 77 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ { 𝐴 } ) → ( 𝑘 ∈ dom ( 𝐼 ‘ 𝑗 ) ↔ 𝑘 ∈ { 𝐴 } ) )
79 73 78 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ { 𝐴 } ) → 𝑘 ∈ dom ( 𝐼 ‘ 𝑗 ) )
80 fvco ⊢ ( ( Fun ( 𝐼 ‘ 𝑗 ) ∧ 𝑘 ∈ dom ( 𝐼 ‘ 𝑗 ) ) → ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( [,) ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑘 ) ) )
81 72 79 80 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ { 𝐴 } ) → ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( [,) ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑘 ) ) )
82 68 fveq1d ⊢ ( 𝑗 ∈ ℕ → ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑘 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } ‘ 𝑘 ) )
83 82 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ { 𝐴 } ) → ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑘 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } ‘ 𝑘 ) )
84 elsni ⊢ ( 𝑘 ∈ { 𝐴 } → 𝑘 = 𝐴 )
85 84 fveq2d ⊢ ( 𝑘 ∈ { 𝐴 } → ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } ‘ 𝑘 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } ‘ 𝐴 ) )
86 85 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ { 𝐴 } ) → ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } ‘ 𝑘 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } ‘ 𝐴 ) )
87 fvexd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑗 ) ∈ V )
88 fvsng ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝑗 ) ∈ V ) → ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } ‘ 𝐴 ) = ( 𝐹 ‘ 𝑗 ) )
89 1 87 88 syl2anc ⊢ ( 𝜑 → ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } ‘ 𝐴 ) = ( 𝐹 ‘ 𝑗 ) )
90 89 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ { 𝐴 } ) → ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } ‘ 𝐴 ) = ( 𝐹 ‘ 𝑗 ) )
91 83 86 90 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ { 𝐴 } ) → ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) )
92 91 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ { 𝐴 } ) → ( [,) ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑘 ) ) = ( [,) ‘ ( 𝐹 ‘ 𝑗 ) ) )
93 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ { 𝐴 } ) → ( [,) ‘ ( 𝐹 ‘ 𝑗 ) ) = ( [,) ‘ ( 𝐹 ‘ 𝑗 ) ) )
94 81 92 93 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ { 𝐴 } ) → ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( [,) ‘ ( 𝐹 ‘ 𝑗 ) ) )
95 94 ixpeq2dva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) = X 𝑘 ∈ { 𝐴 } ( [,) ‘ ( 𝐹 ‘ 𝑗 ) ) )
96 fvex ⊢ ( [,) ‘ ( 𝐹 ‘ 𝑗 ) ) ∈ V
97 20 96 ixpconst ⊢ X 𝑘 ∈ { 𝐴 } ( [,) ‘ ( 𝐹 ‘ 𝑗 ) ) = ( ( [,) ‘ ( 𝐹 ‘ 𝑗 ) ) ↑m { 𝐴 } )
98 97 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → X 𝑘 ∈ { 𝐴 } ( [,) ‘ ( 𝐹 ‘ 𝑗 ) ) = ( ( [,) ‘ ( 𝐹 ‘ 𝑗 ) ) ↑m { 𝐴 } ) )
99 95 98 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( [,) ‘ ( 𝐹 ‘ 𝑗 ) ) ↑m { 𝐴 } ) )
100 99 iuneq2dv ⊢ ( 𝜑 → ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) = ∪ 𝑗 ∈ ℕ ( ( [,) ‘ ( 𝐹 ‘ 𝑗 ) ) ↑m { 𝐴 } ) )
101 50 62 100 3eqtr4d ⊢ ( 𝜑 → ( ∪ 𝑗 ∈ ℕ ( ( [,) ∘ 𝐹 ) ‘ 𝑗 ) ↑m { 𝐴 } ) = ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) )
102 46 101 sseqtrd ⊢ ( 𝜑 → ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) )
103 nfcv ⊢ Ⅎ 𝑗 𝐹
104 ressxr ⊢ ℝ ⊆ ℝ*
105 xpss2 ⊢ ( ℝ ⊆ ℝ* → ( ℝ × ℝ ) ⊆ ( ℝ × ℝ* ) )
106 104 105 ax-mp ⊢ ( ℝ × ℝ ) ⊆ ( ℝ × ℝ* )
107 106 a1i ⊢ ( 𝜑 → ( ℝ × ℝ ) ⊆ ( ℝ × ℝ* ) )
108 10 107 fssd ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ℝ × ℝ* ) )
109 103 108 volicofmpt ⊢ ( 𝜑 → ( ( vol ∘ [,) ) ∘ 𝐹 ) = ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ) ) ) )
110 68 coeq2d ⊢ ( 𝑗 ∈ ℕ → ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) = ( [,) ∘ { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } ) )
111 110 fveq1d ⊢ ( 𝑗 ∈ ℕ → ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝐴 ) = ( ( [,) ∘ { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } ) ‘ 𝐴 ) )
112 111 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝐴 ) = ( ( [,) ∘ { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } ) ‘ 𝐴 ) )
113 snidg ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 } )
114 1 113 syl ⊢ ( 𝜑 → 𝐴 ∈ { 𝐴 } )
115 dmsnopg ⊢ ( ( 𝐹 ‘ 𝑗 ) ∈ V → dom { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } = { 𝐴 } )
116 87 115 syl ⊢ ( 𝜑 → dom { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } = { 𝐴 } )
117 114 116 eleqtrrd ⊢ ( 𝜑 → 𝐴 ∈ dom { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } )
118 117 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝐴 ∈ dom { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } )
119 fvco ⊢ ( ( Fun { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } ∧ 𝐴 ∈ dom { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } ) → ( ( [,) ∘ { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } ) ‘ 𝐴 ) = ( [,) ‘ ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } ‘ 𝐴 ) ) )
120 63 118 119 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( [,) ∘ { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } ) ‘ 𝐴 ) = ( [,) ‘ ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } ‘ 𝐴 ) ) )
121 fvexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) ∈ V )
122 8 121 88 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } ‘ 𝐴 ) = ( 𝐹 ‘ 𝑗 ) )
123 1st2nd2 ⊢ ( ( 𝐹 ‘ 𝑗 ) ∈ ( ℝ × ℝ ) → ( 𝐹 ‘ 𝑗 ) = ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ⟩ )
124 11 123 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) = ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ⟩ )
125 122 124 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } ‘ 𝐴 ) = ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ⟩ )
126 125 fveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( [,) ‘ ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } ‘ 𝐴 ) ) = ( [,) ‘ ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ⟩ ) )
127 df-ov ⊢ ( ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ) = ( [,) ‘ ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ⟩ )
128 127 eqcomi ⊢ ( [,) ‘ ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ⟩ ) = ( ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) )
129 128 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( [,) ‘ ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ⟩ ) = ( ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ) )
130 126 129 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( [,) ‘ ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝑗 ) ⟩ } ‘ 𝐴 ) ) = ( ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ) )
131 112 120 130 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝐴 ) = ( ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ) )
132 131 fveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝐴 ) ) = ( vol ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ) ) )
133 xp1st ⊢ ( ( 𝐹 ‘ 𝑗 ) ∈ ( ℝ × ℝ ) → ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ )
134 11 133 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ )
135 xp2nd ⊢ ( ( 𝐹 ‘ 𝑗 ) ∈ ( ℝ × ℝ ) → ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ )
136 11 135 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ )
137 volicore ⊢ ( ( ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ ) → ( vol ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ) ) ∈ ℝ )
138 134 136 137 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ) ) ∈ ℝ )
139 132 138 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝐴 ) ) ∈ ℝ )
140 139 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝐴 ) ) ∈ ℂ )
141 2fveq3 ⊢ ( 𝑘 = 𝐴 → ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝐴 ) ) )
142 141 prodsn ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝐴 ) ) ∈ ℂ ) → ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝐴 ) ) )
143 8 140 142 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝐴 ) ) )
144 143 132 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ) ) = ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
145 144 mpteq2dva ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑗 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑗 ) ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) )
146 109 145 eqtrd ⊢ ( 𝜑 → ( ( vol ∘ [,) ) ∘ 𝐹 ) = ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) )
147 146 fveq2d ⊢ ( 𝜑 → ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝐹 ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
148 6 147 eqtrd ⊢ ( 𝜑 → 𝑍 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
149 102 148 jca ⊢ ( 𝜑 → ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑍 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
150 fveq1 ⊢ ( 𝑖 = 𝐼 → ( 𝑖 ‘ 𝑗 ) = ( 𝐼 ‘ 𝑗 ) )
151 150 coeq2d ⊢ ( 𝑖 = 𝐼 → ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) = ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) )
152 151 fveq1d ⊢ ( 𝑖 = 𝐼 → ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) )
153 152 ixpeq2dv ⊢ ( 𝑖 = 𝐼 → X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) )
154 153 iuneq2d ⊢ ( 𝑖 = 𝐼 → ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) )
155 154 sseq2d ⊢ ( 𝑖 = 𝐼 → ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ↔ ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
156 simpl ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑘 ∈ { 𝐴 } ) → 𝑖 = 𝐼 )
157 156 fveq1d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑘 ∈ { 𝐴 } ) → ( 𝑖 ‘ 𝑗 ) = ( 𝐼 ‘ 𝑗 ) )
158 157 coeq2d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑘 ∈ { 𝐴 } ) → ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) = ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) )
159 158 fveq1d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑘 ∈ { 𝐴 } ) → ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) )
160 159 fveq2d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑘 ∈ { 𝐴 } ) → ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
161 160 prodeq2dv ⊢ ( 𝑖 = 𝐼 → ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
162 161 mpteq2dv ⊢ ( 𝑖 = 𝐼 → ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) = ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) )
163 162 fveq2d ⊢ ( 𝑖 = 𝐼 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
164 163 eqeq2d ⊢ ( 𝑖 = 𝐼 → ( 𝑍 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ↔ 𝑍 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
165 155 164 anbi12d ⊢ ( 𝑖 = 𝐼 → ( ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑍 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ↔ ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑍 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
166 165 rspcev ⊢ ( ( 𝐼 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ∧ ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑍 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑍 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
167 29 149 166 syl2anc ⊢ ( 𝜑 → ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑍 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )