Metamath Proof Explorer

Theorem hoicvrrex

Description: Any subset of the multidimensional reals can be covered by a countable set of half-open intervals, see Definition 115A (b) of Fremlin1 p. 29. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses hoicvrrex.fi ⊢ ( 𝜑 → 𝑋 ∈ Fin )
hoicvrrex.y ⊢ ( 𝜑 → 𝑌 ⊆ ( ℝ ↑m 𝑋 ) )
Assertion hoicvrrex ( 𝜑 → ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝑌 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ +∞ = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 hoicvrrex.fi ⊢ ( 𝜑 → 𝑋 ∈ Fin )
2 hoicvrrex.y ⊢ ( 𝜑 → 𝑌 ⊆ ( ℝ ↑m 𝑋 ) )
3 nnre ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℝ )
4 3 renegcld ⊢ ( 𝑗 ∈ ℕ → - 𝑗 ∈ ℝ )
5 opelxpi ⊢ ( ( - 𝑗 ∈ ℝ ∧ 𝑗 ∈ ℝ ) → ⟨ - 𝑗 , 𝑗 ⟩ ∈ ( ℝ × ℝ ) )
6 4 3 5 syl2anc ⊢ ( 𝑗 ∈ ℕ → ⟨ - 𝑗 , 𝑗 ⟩ ∈ ( ℝ × ℝ ) )
7 6 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ⟨ - 𝑗 , 𝑗 ⟩ ∈ ( ℝ × ℝ ) )
8 eqid ⊢ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) = ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ )
9 7 8 fmptd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) : 𝑋 ⟶ ( ℝ × ℝ ) )
10 reex ⊢ ℝ ∈ V
11 10 10 xpex ⊢ ( ℝ × ℝ ) ∈ V
12 11 a1i ⊢ ( 𝜑 → ( ℝ × ℝ ) ∈ V )
13 elmapg ⊢ ( ( ( ℝ × ℝ ) ∈ V ∧ 𝑋 ∈ Fin ) → ( ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↔ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) : 𝑋 ⟶ ( ℝ × ℝ ) ) )
14 12 1 13 syl2anc ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↔ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) : 𝑋 ⟶ ( ℝ × ℝ ) ) )
15 14 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↔ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) : 𝑋 ⟶ ( ℝ × ℝ ) ) )
16 9 15 mpbird ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
17 eqid ⊢ ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) )
18 16 17 fmptd ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) : ℕ ⟶ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
19 ovex ⊢ ( ( ℝ × ℝ ) ↑m 𝑋 ) ∈ V
20 nnex ⊢ ℕ ∈ V
21 19 20 elmap ⊢ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ↔ ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) : ℕ ⟶ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
22 18 21 sylibr ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) )
23 eqid ⊢ ( 𝑗 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) = ( 𝑗 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) )
24 23 1 hoicvr ⊢ ( 𝜑 → ( ℝ ↑m 𝑋 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) )
25 eqidd ⊢ ( 𝑙 = 𝑘 → ⟨ - 𝑗 , 𝑗 ⟩ = ⟨ - 𝑗 , 𝑗 ⟩ )
26 25 cbvmptv ⊢ ( 𝑙 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) = ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ )
27 26 mpteq2i ⊢ ( 𝑗 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) )
28 27 a1i ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) )
29 28 fveq1d ⊢ ( 𝜑 → ( ( 𝑗 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) = ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) )
30 29 coeq2d ⊢ ( 𝜑 → ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) = ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) )
31 30 fveq1d ⊢ ( 𝜑 → ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) )
32 31 ixpeq2dv ⊢ ( 𝜑 → X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) = X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) )
33 32 iuneq2d ⊢ ( 𝜑 → ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) = ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) )
34 24 33 sseqtrd ⊢ ( 𝜑 → ( ℝ ↑m 𝑋 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) )
35 2 34 sstrd ⊢ ( 𝜑 → 𝑌 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) )
36 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ )
37 16 elexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ∈ V )
38 17 fvmpt2 ⊢ ( ( 𝑗 ∈ ℕ ∧ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ∈ V ) → ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) = ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) )
39 36 37 38 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) = ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) )
40 39 7 fmpt3d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
41 40 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
42 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → 𝑘 ∈ 𝑋 )
43 41 42 fvovco ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( 1st ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ‘ 𝑘 ) ) ) )
44 39 fveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ‘ 𝑘 ) = ( ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ‘ 𝑘 ) )
45 44 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ‘ 𝑘 ) = ( ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ‘ 𝑘 ) )
46 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝑘 ∈ 𝑋 )
47 opex ⊢ ⟨ - 𝑗 , 𝑗 ⟩ ∈ V
48 47 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ⟨ - 𝑗 , 𝑗 ⟩ ∈ V )
49 8 fvmpt2 ⊢ ( ( 𝑘 ∈ 𝑋 ∧ ⟨ - 𝑗 , 𝑗 ⟩ ∈ V ) → ( ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ‘ 𝑘 ) = ⟨ - 𝑗 , 𝑗 ⟩ )
50 46 48 49 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ‘ 𝑘 ) = ⟨ - 𝑗 , 𝑗 ⟩ )
51 50 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ‘ 𝑘 ) = ⟨ - 𝑗 , 𝑗 ⟩ )
52 45 51 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ‘ 𝑘 ) = ⟨ - 𝑗 , 𝑗 ⟩ )
53 52 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 1st ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ‘ 𝑘 ) ) = ( 1st ‘ ⟨ - 𝑗 , 𝑗 ⟩ ) )
54 negex ⊢ - 𝑗 ∈ V
55 vex ⊢ 𝑗 ∈ V
56 54 55 op1st ⊢ ( 1st ‘ ⟨ - 𝑗 , 𝑗 ⟩ ) = - 𝑗
57 56 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 1st ‘ ⟨ - 𝑗 , 𝑗 ⟩ ) = - 𝑗 )
58 53 57 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 1st ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ‘ 𝑘 ) ) = - 𝑗 )
59 52 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 2nd ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ‘ 𝑘 ) ) = ( 2nd ‘ ⟨ - 𝑗 , 𝑗 ⟩ ) )
60 54 55 op2nd ⊢ ( 2nd ‘ ⟨ - 𝑗 , 𝑗 ⟩ ) = 𝑗
61 60 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 2nd ‘ ⟨ - 𝑗 , 𝑗 ⟩ ) = 𝑗 )
62 59 61 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 2nd ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ‘ 𝑘 ) ) = 𝑗 )
63 58 62 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 1st ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ‘ 𝑘 ) ) ) = ( - 𝑗 [,) 𝑗 ) )
64 43 63 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) = ( - 𝑗 [,) 𝑗 ) )
65 64 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( vol ‘ ( - 𝑗 [,) 𝑗 ) ) )
66 volico ⊢ ( ( - 𝑗 ∈ ℝ ∧ 𝑗 ∈ ℝ ) → ( vol ‘ ( - 𝑗 [,) 𝑗 ) ) = if ( - 𝑗 < 𝑗 , ( 𝑗 − - 𝑗 ) , 0 ) )
67 4 3 66 syl2anc ⊢ ( 𝑗 ∈ ℕ → ( vol ‘ ( - 𝑗 [,) 𝑗 ) ) = if ( - 𝑗 < 𝑗 , ( 𝑗 − - 𝑗 ) , 0 ) )
68 nnrp ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℝ+ )
69 neglt ⊢ ( 𝑗 ∈ ℝ+ → - 𝑗 < 𝑗 )
70 68 69 syl ⊢ ( 𝑗 ∈ ℕ → - 𝑗 < 𝑗 )
71 70 iftrued ⊢ ( 𝑗 ∈ ℕ → if ( - 𝑗 < 𝑗 , ( 𝑗 − - 𝑗 ) , 0 ) = ( 𝑗 − - 𝑗 ) )
72 3 recnd ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℂ )
73 72 72 subnegd ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 − - 𝑗 ) = ( 𝑗 + 𝑗 ) )
74 72 2timesd ⊢ ( 𝑗 ∈ ℕ → ( 2 · 𝑗 ) = ( 𝑗 + 𝑗 ) )
75 73 74 eqtr4d ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 − - 𝑗 ) = ( 2 · 𝑗 ) )
76 67 71 75 3eqtrd ⊢ ( 𝑗 ∈ ℕ → ( vol ‘ ( - 𝑗 [,) 𝑗 ) ) = ( 2 · 𝑗 ) )
77 76 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( - 𝑗 [,) 𝑗 ) ) = ( 2 · 𝑗 ) )
78 65 77 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( 2 · 𝑗 ) )
79 78 prodeq2dv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ∏ 𝑘 ∈ 𝑋 ( 2 · 𝑗 ) )
80 1 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑋 ∈ Fin )
81 2cnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 2 ∈ ℂ )
82 72 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℂ )
83 81 82 mulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 2 · 𝑗 ) ∈ ℂ )
84 fprodconst ⊢ ( ( 𝑋 ∈ Fin ∧ ( 2 · 𝑗 ) ∈ ℂ ) → ∏ 𝑘 ∈ 𝑋 ( 2 · 𝑗 ) = ( ( 2 · 𝑗 ) ↑ ( ♯ ‘ 𝑋 ) ) )
85 80 83 84 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ∏ 𝑘 ∈ 𝑋 ( 2 · 𝑗 ) = ( ( 2 · 𝑗 ) ↑ ( ♯ ‘ 𝑋 ) ) )
86 79 85 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( ( 2 · 𝑗 ) ↑ ( ♯ ‘ 𝑋 ) ) )
87 86 mpteq2dva ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 2 · 𝑗 ) ↑ ( ♯ ‘ 𝑋 ) ) ) )
88 87 fveq2d ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 2 · 𝑗 ) ↑ ( ♯ ‘ 𝑋 ) ) ) ) )
89 20 a1i ⊢ ( 𝜑 → ℕ ∈ V )
90 68 ssriv ⊢ ℕ ⊆ ℝ+
91 ioorp ⊢ ( 0 (,) +∞ ) = ℝ+
92 91 eqcomi ⊢ ℝ+ = ( 0 (,) +∞ )
93 90 92 sseqtri ⊢ ℕ ⊆ ( 0 (,) +∞ )
94 ioossicc ⊢ ( 0 (,) +∞ ) ⊆ ( 0 [,] +∞ )
95 93 94 sstri ⊢ ℕ ⊆ ( 0 [,] +∞ )
96 2nn ⊢ 2 ∈ ℕ
97 96 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 2 ∈ ℕ )
98 97 36 nnmulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 2 · 𝑗 ) ∈ ℕ )
99 hashcl ⊢ ( 𝑋 ∈ Fin → ( ♯ ‘ 𝑋 ) ∈ ℕ0 )
100 1 99 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) ∈ ℕ0 )
101 100 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ♯ ‘ 𝑋 ) ∈ ℕ0 )
102 nnexpcl ⊢ ( ( ( 2 · 𝑗 ) ∈ ℕ ∧ ( ♯ ‘ 𝑋 ) ∈ ℕ0 ) → ( ( 2 · 𝑗 ) ↑ ( ♯ ‘ 𝑋 ) ) ∈ ℕ )
103 98 101 102 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 2 · 𝑗 ) ↑ ( ♯ ‘ 𝑋 ) ) ∈ ℕ )
104 95 103 sseldi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 2 · 𝑗 ) ↑ ( ♯ ‘ 𝑋 ) ) ∈ ( 0 [,] +∞ ) )
105 eqid ⊢ ( 𝑗 ∈ ℕ ↦ ( ( 2 · 𝑗 ) ↑ ( ♯ ‘ 𝑋 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 2 · 𝑗 ) ↑ ( ♯ ‘ 𝑋 ) ) )
106 104 105 fmptd ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( ( 2 · 𝑗 ) ↑ ( ♯ ‘ 𝑋 ) ) ) : ℕ ⟶ ( 0 [,] +∞ ) )
107 89 106 sge0xrcl ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 2 · 𝑗 ) ↑ ( ♯ ‘ 𝑋 ) ) ) ) ∈ ℝ* )
108 pnfxr ⊢ +∞ ∈ ℝ*
109 108 a1i ⊢ ( 𝜑 → +∞ ∈ ℝ* )
110 1nn ⊢ 1 ∈ ℕ
111 95 110 sselii ⊢ 1 ∈ ( 0 [,] +∞ )
112 111 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 1 ∈ ( 0 [,] +∞ ) )
113 eqid ⊢ ( 𝑗 ∈ ℕ ↦ 1 ) = ( 𝑗 ∈ ℕ ↦ 1 )
114 112 113 fmptd ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ 1 ) : ℕ ⟶ ( 0 [,] +∞ ) )
115 89 114 sge0xrcl ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ 1 ) ) ∈ ℝ* )
116 nnnfi ⊢ ¬ ℕ ∈ Fin
117 116 a1i ⊢ ( 𝜑 → ¬ ℕ ∈ Fin )
118 1rp ⊢ 1 ∈ ℝ+
119 118 a1i ⊢ ( 𝜑 → 1 ∈ ℝ+ )
120 89 117 119 sge0rpcpnf ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ 1 ) ) = +∞ )
121 120 eqcomd ⊢ ( 𝜑 → +∞ = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ 1 ) ) )
122 109 121 xreqled ⊢ ( 𝜑 → +∞ ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ 1 ) ) )
123 nfv ⊢ Ⅎ 𝑗 𝜑
124 114 fvmptelrn ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 1 ∈ ( 0 [,] +∞ ) )
125 103 nnge1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 1 ≤ ( ( 2 · 𝑗 ) ↑ ( ♯ ‘ 𝑋 ) ) )
126 123 89 124 104 125 sge0lempt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ 1 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 2 · 𝑗 ) ↑ ( ♯ ‘ 𝑋 ) ) ) ) )
127 109 115 107 122 126 xrletrd ⊢ ( 𝜑 → +∞ ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 2 · 𝑗 ) ↑ ( ♯ ‘ 𝑋 ) ) ) ) )
128 107 127 xrgepnfd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 2 · 𝑗 ) ↑ ( ♯ ‘ 𝑋 ) ) ) ) = +∞ )
129 eqidd ⊢ ( 𝜑 → +∞ = +∞ )
130 88 128 129 3eqtrrd ⊢ ( 𝜑 → +∞ = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
131 35 130 jca ⊢ ( 𝜑 → ( 𝑌 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ +∞ = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
132 nfcv ⊢ Ⅎ 𝑗 𝑖
133 nfmpt1 ⊢ Ⅎ 𝑗 ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) )
134 132 133 nfeq ⊢ Ⅎ 𝑗 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) )
135 nfcv ⊢ Ⅎ 𝑘 𝑖
136 nfcv ⊢ Ⅎ 𝑘 ℕ
137 nfmpt1 ⊢ Ⅎ 𝑘 ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ )
138 136 137 nfmpt ⊢ Ⅎ 𝑘 ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) )
139 135 138 nfeq ⊢ Ⅎ 𝑘 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) )
140 fveq1 ⊢ ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) → ( 𝑖 ‘ 𝑗 ) = ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) )
141 140 coeq2d ⊢ ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) → ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) = ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) )
142 141 fveq1d ⊢ ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) → ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) )
143 142 adantr ⊢ ( ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ∧ 𝑘 ∈ 𝑋 ) → ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) )
144 139 143 ixpeq2d ⊢ ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) → X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) )
145 144 adantr ⊢ ( ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ∧ 𝑗 ∈ ℕ ) → X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) )
146 134 145 iuneq2df ⊢ ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) → ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) )
147 146 sseq2d ⊢ ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) → ( 𝑌 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ↔ 𝑌 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
148 142 fveq2d ⊢ ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) → ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
149 148 a1d ⊢ ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) → ( 𝑘 ∈ 𝑋 → ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) )
150 139 149 ralrimi ⊢ ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) → ∀ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
151 150 adantr ⊢ ( ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ∧ 𝑗 ∈ ℕ ) → ∀ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
152 151 prodeq2d ⊢ ( ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ∧ 𝑗 ∈ ℕ ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
153 134 152 mpteq2da ⊢ ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) → ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) = ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) )
154 153 fveq2d ⊢ ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
155 154 eqeq2d ⊢ ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) → ( +∞ = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ↔ +∞ = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
156 147 155 anbi12d ⊢ ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) → ( ( 𝑌 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ +∞ = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ↔ ( 𝑌 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ +∞ = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
157 156 rspcev ⊢ ( ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝑌 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ +∞ = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝑌 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ +∞ = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
158 22 131 157 syl2anc ⊢ ( 𝜑 → ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝑌 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ +∞ = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )