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 sselid ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 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 ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )