Metamath Proof Explorer


Theorem ovnhoilem2

Description: The Lebesgue outer measure of a multidimensional half-open interval is less than or equal to the product of its length in each dimension. Second part of the proof of Proposition 115D (b) of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses ovnhoilem2.x ( 𝜑𝑋 ∈ Fin )
ovnhoilem2.n ( 𝜑𝑋 ≠ ∅ )
ovnhoilem2.a ( 𝜑𝐴 : 𝑋 ⟶ ℝ )
ovnhoilem2.b ( 𝜑𝐵 : 𝑋 ⟶ ℝ )
ovnhoilem2.i 𝐼 = X 𝑘𝑋 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) )
ovnhoilem2.l 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘𝑥 ( vol ‘ ( ( 𝑎𝑘 ) [,) ( 𝑏𝑘 ) ) ) ) ) )
ovnhoilem2.m 𝑀 = { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) ) }
ovnhoilem2.f 𝐹 = ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ↦ ( 𝑛 ∈ ℕ ↦ ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ) )
ovnhoilem2.s 𝑆 = ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ↦ ( 𝑛 ∈ ℕ ↦ ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ) )
Assertion ovnhoilem2 ( 𝜑 → ( 𝐴 ( 𝐿𝑋 ) 𝐵 ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝐼 ) )

Proof

Step Hyp Ref Expression
1 ovnhoilem2.x ( 𝜑𝑋 ∈ Fin )
2 ovnhoilem2.n ( 𝜑𝑋 ≠ ∅ )
3 ovnhoilem2.a ( 𝜑𝐴 : 𝑋 ⟶ ℝ )
4 ovnhoilem2.b ( 𝜑𝐵 : 𝑋 ⟶ ℝ )
5 ovnhoilem2.i 𝐼 = X 𝑘𝑋 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) )
6 ovnhoilem2.l 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘𝑥 ( vol ‘ ( ( 𝑎𝑘 ) [,) ( 𝑏𝑘 ) ) ) ) ) )
7 ovnhoilem2.m 𝑀 = { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) ) }
8 ovnhoilem2.f 𝐹 = ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ↦ ( 𝑛 ∈ ℕ ↦ ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ) )
9 ovnhoilem2.s 𝑆 = ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ↦ ( 𝑛 ∈ ℕ ↦ ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ) )
10 7 eleq2i ( 𝑧𝑀𝑧 ∈ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } )
11 rabid ( 𝑧 ∈ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ↔ ( 𝑧 ∈ ℝ* ∧ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
12 10 11 bitri ( 𝑧𝑀 ↔ ( 𝑧 ∈ ℝ* ∧ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
13 12 biimpi ( 𝑧𝑀 → ( 𝑧 ∈ ℝ* ∧ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
14 13 simprd ( 𝑧𝑀 → ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
15 14 adantl ( ( 𝜑𝑧𝑀 ) → ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
16 1 3ad2ant1 ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝐼 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → 𝑋 ∈ Fin )
17 3 3ad2ant1 ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝐼 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → 𝐴 : 𝑋 ⟶ ℝ )
18 4 3ad2ant1 ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝐼 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → 𝐵 : 𝑋 ⟶ ℝ )
19 elmapi ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → 𝑖 : ℕ ⟶ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
20 19 ffvelrnda ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑖𝑛 ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
21 elmapi ( ( 𝑖𝑛 ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) → ( 𝑖𝑛 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
22 20 21 syl ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑖𝑛 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
23 22 ffvelrnda ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑙𝑋 ) → ( ( 𝑖𝑛 ) ‘ 𝑙 ) ∈ ( ℝ × ℝ ) )
24 xp1st ( ( ( 𝑖𝑛 ) ‘ 𝑙 ) ∈ ( ℝ × ℝ ) → ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ∈ ℝ )
25 23 24 syl ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑙𝑋 ) → ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ∈ ℝ )
26 25 fmpttd ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) : 𝑋 ⟶ ℝ )
27 reex ℝ ∈ V
28 27 a1i ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ℝ ∈ V )
29 1nn 1 ∈ ℕ
30 29 a1i ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → 1 ∈ ℕ )
31 19 30 ffvelrnd ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( 𝑖 ‘ 1 ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
32 elmapex ( ( 𝑖 ‘ 1 ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) → ( ( ℝ × ℝ ) ∈ V ∧ 𝑋 ∈ V ) )
33 32 simprd ( ( 𝑖 ‘ 1 ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) → 𝑋 ∈ V )
34 31 33 syl ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → 𝑋 ∈ V )
35 34 adantr ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → 𝑋 ∈ V )
36 elmapg ( ( ℝ ∈ V ∧ 𝑋 ∈ V ) → ( ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ∈ ( ℝ ↑m 𝑋 ) ↔ ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) : 𝑋 ⟶ ℝ ) )
37 28 35 36 syl2anc ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ∈ ( ℝ ↑m 𝑋 ) ↔ ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) : 𝑋 ⟶ ℝ ) )
38 26 37 mpbird ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ∈ ( ℝ ↑m 𝑋 ) )
39 38 fmpttd ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( 𝑛 ∈ ℕ ↦ ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ) : ℕ ⟶ ( ℝ ↑m 𝑋 ) )
40 id ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) )
41 nnex ℕ ∈ V
42 41 mptex ( 𝑛 ∈ ℕ ↦ ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ) ∈ V
43 42 a1i ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( 𝑛 ∈ ℕ ↦ ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ) ∈ V )
44 8 fvmpt2 ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝑛 ∈ ℕ ↦ ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ) ∈ V ) → ( 𝐹𝑖 ) = ( 𝑛 ∈ ℕ ↦ ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ) )
45 40 43 44 syl2anc ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( 𝐹𝑖 ) = ( 𝑛 ∈ ℕ ↦ ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ) )
46 45 feq1d ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( ( 𝐹𝑖 ) : ℕ ⟶ ( ℝ ↑m 𝑋 ) ↔ ( 𝑛 ∈ ℕ ↦ ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ) : ℕ ⟶ ( ℝ ↑m 𝑋 ) ) )
47 39 46 mpbird ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( 𝐹𝑖 ) : ℕ ⟶ ( ℝ ↑m 𝑋 ) )
48 47 3ad2ant2 ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝐼 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → ( 𝐹𝑖 ) : ℕ ⟶ ( ℝ ↑m 𝑋 ) )
49 xp2nd ( ( ( 𝑖𝑛 ) ‘ 𝑙 ) ∈ ( ℝ × ℝ ) → ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ∈ ℝ )
50 23 49 syl ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑙𝑋 ) → ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ∈ ℝ )
51 50 fmpttd ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) : 𝑋 ⟶ ℝ )
52 elmapg ( ( ℝ ∈ V ∧ 𝑋 ∈ V ) → ( ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ∈ ( ℝ ↑m 𝑋 ) ↔ ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) : 𝑋 ⟶ ℝ ) )
53 28 35 52 syl2anc ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ∈ ( ℝ ↑m 𝑋 ) ↔ ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) : 𝑋 ⟶ ℝ ) )
54 51 53 mpbird ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ∈ ( ℝ ↑m 𝑋 ) )
55 54 fmpttd ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( 𝑛 ∈ ℕ ↦ ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ) : ℕ ⟶ ( ℝ ↑m 𝑋 ) )
56 41 mptex ( 𝑛 ∈ ℕ ↦ ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ) ∈ V
57 56 a1i ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( 𝑛 ∈ ℕ ↦ ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ) ∈ V )
58 9 fvmpt2 ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝑛 ∈ ℕ ↦ ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ) ∈ V ) → ( 𝑆𝑖 ) = ( 𝑛 ∈ ℕ ↦ ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ) )
59 40 57 58 syl2anc ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( 𝑆𝑖 ) = ( 𝑛 ∈ ℕ ↦ ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ) )
60 59 feq1d ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( ( 𝑆𝑖 ) : ℕ ⟶ ( ℝ ↑m 𝑋 ) ↔ ( 𝑛 ∈ ℕ ↦ ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ) : ℕ ⟶ ( ℝ ↑m 𝑋 ) ) )
61 55 60 mpbird ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( 𝑆𝑖 ) : ℕ ⟶ ( ℝ ↑m 𝑋 ) )
62 61 3ad2ant2 ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝐼 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → ( 𝑆𝑖 ) : ℕ ⟶ ( ℝ ↑m 𝑋 ) )
63 simp3 ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝐼 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) → 𝐼 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) )
64 5 a1i ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝐼 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) → 𝐼 = X 𝑘𝑋 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
65 fveq2 ( 𝑗 = 𝑛 → ( 𝑖𝑗 ) = ( 𝑖𝑛 ) )
66 65 fveq1d ( 𝑗 = 𝑛 → ( ( 𝑖𝑗 ) ‘ 𝑘 ) = ( ( 𝑖𝑛 ) ‘ 𝑘 ) )
67 66 fveq2d ( 𝑗 = 𝑛 → ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) = ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑘 ) ) )
68 66 fveq2d ( 𝑗 = 𝑛 → ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) = ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑘 ) ) )
69 67 68 oveq12d ( 𝑗 = 𝑛 → ( ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) ) = ( ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑘 ) ) ) )
70 69 ixpeq2dv ( 𝑗 = 𝑛X 𝑘𝑋 ( ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) ) = X 𝑘𝑋 ( ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑘 ) ) ) )
71 70 cbviunv 𝑗 ∈ ℕ X 𝑘𝑋 ( ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) ) = 𝑛 ∈ ℕ X 𝑘𝑋 ( ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑘 ) ) )
72 71 a1i ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → 𝑗 ∈ ℕ X 𝑘𝑋 ( ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) ) = 𝑛 ∈ ℕ X 𝑘𝑋 ( ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑘 ) ) ) )
73 19 ffvelrnda ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑗 ∈ ℕ ) → ( 𝑖𝑗 ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
74 elmapi ( ( 𝑖𝑗 ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) → ( 𝑖𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
75 73 74 syl ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑗 ∈ ℕ ) → ( 𝑖𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
76 75 adantr ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( 𝑖𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
77 simpr ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘𝑋 ) → 𝑘𝑋 )
78 76 77 fvovco ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) = ( ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) ) )
79 78 ixpeq2dva ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑗 ∈ ℕ ) → X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) = X 𝑘𝑋 ( ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) ) )
80 79 iuneq2dv ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) = 𝑗 ∈ ℕ X 𝑘𝑋 ( ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) ) )
81 simpl ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) )
82 42 a1i ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑛 ∈ ℕ ↦ ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ) ∈ V )
83 81 82 44 syl2anc ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹𝑖 ) = ( 𝑛 ∈ ℕ ↦ ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ) )
84 83 fveq1d ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹𝑖 ) ‘ 𝑛 ) = ( ( 𝑛 ∈ ℕ ↦ ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ) ‘ 𝑛 ) )
85 simpr ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
86 mptexg ( 𝑋 ∈ V → ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ∈ V )
87 34 86 syl ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ∈ V )
88 87 adantr ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ∈ V )
89 eqid ( 𝑛 ∈ ℕ ↦ ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) )
90 89 fvmpt2 ( ( 𝑛 ∈ ℕ ∧ ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ∈ V ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ) ‘ 𝑛 ) = ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) )
91 85 88 90 syl2anc ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ) ‘ 𝑛 ) = ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) )
92 84 91 eqtrd ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹𝑖 ) ‘ 𝑛 ) = ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) )
93 92 fveq1d ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝐹𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) = ( ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) )
94 93 adantr ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( ( ( 𝐹𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) = ( ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) )
95 eqidd ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑘𝑋 ) → ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) = ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) )
96 simpr ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑘𝑋 ) ∧ 𝑙 = 𝑘 ) → 𝑙 = 𝑘 )
97 96 fveq2d ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑘𝑋 ) ∧ 𝑙 = 𝑘 ) → ( ( 𝑖𝑛 ) ‘ 𝑙 ) = ( ( 𝑖𝑛 ) ‘ 𝑘 ) )
98 97 fveq2d ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑘𝑋 ) ∧ 𝑙 = 𝑘 ) → ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) = ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑘 ) ) )
99 simpr ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑘𝑋 ) → 𝑘𝑋 )
100 fvexd ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑘𝑋 ) → ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑘 ) ) ∈ V )
101 95 98 99 100 fvmptd ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑘𝑋 ) → ( ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑘 ) ) )
102 101 adantlr ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑘 ) ) )
103 94 102 eqtrd ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( ( ( 𝐹𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) = ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑘 ) ) )
104 59 fveq1d ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( ( 𝑆𝑖 ) ‘ 𝑛 ) = ( ( 𝑛 ∈ ℕ ↦ ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ) ‘ 𝑛 ) )
105 104 adantr ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑆𝑖 ) ‘ 𝑛 ) = ( ( 𝑛 ∈ ℕ ↦ ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ) ‘ 𝑛 ) )
106 mptexg ( 𝑋 ∈ V → ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ∈ V )
107 34 106 syl ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ∈ V )
108 107 adantr ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ∈ V )
109 eqid ( 𝑛 ∈ ℕ ↦ ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) )
110 109 fvmpt2 ( ( 𝑛 ∈ ℕ ∧ ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ∈ V ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ) ‘ 𝑛 ) = ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) )
111 85 108 110 syl2anc ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ) ‘ 𝑛 ) = ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) )
112 105 111 eqtrd ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑆𝑖 ) ‘ 𝑛 ) = ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) )
113 112 fveq1d ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝑆𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) = ( ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) )
114 113 adantr ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( ( ( 𝑆𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) = ( ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) )
115 eqidd ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑘𝑋 ) → ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) = ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) )
116 2fveq3 ( 𝑙 = 𝑘 → ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) = ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑘 ) ) )
117 116 adantl ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑘𝑋 ) ∧ 𝑙 = 𝑘 ) → ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) = ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑘 ) ) )
118 fvexd ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑘𝑋 ) → ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑘 ) ) ∈ V )
119 115 117 99 118 fvmptd ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑘𝑋 ) → ( ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑘 ) ) )
120 119 adantlr ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑘 ) ) )
121 114 120 eqtrd ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( ( ( 𝑆𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) = ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑘 ) ) )
122 103 121 oveq12d ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( ( ( ( 𝐹𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) [,) ( ( ( 𝑆𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) ) = ( ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑘 ) ) ) )
123 122 ixpeq2dva ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → X 𝑘𝑋 ( ( ( ( 𝐹𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) [,) ( ( ( 𝑆𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) ) = X 𝑘𝑋 ( ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑘 ) ) ) )
124 123 iuneq2dv ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → 𝑛 ∈ ℕ X 𝑘𝑋 ( ( ( ( 𝐹𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) [,) ( ( ( 𝑆𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) ) = 𝑛 ∈ ℕ X 𝑘𝑋 ( ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑘 ) ) ) )
125 72 80 124 3eqtr4d ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) = 𝑛 ∈ ℕ X 𝑘𝑋 ( ( ( ( 𝐹𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) [,) ( ( ( 𝑆𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) ) )
126 125 adantl ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) → 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) = 𝑛 ∈ ℕ X 𝑘𝑋 ( ( ( ( 𝐹𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) [,) ( ( ( 𝑆𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) ) )
127 126 3adant3 ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝐼 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) → 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) = 𝑛 ∈ ℕ X 𝑘𝑋 ( ( ( ( 𝐹𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) [,) ( ( ( 𝑆𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) ) )
128 64 127 sseq12d ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝐼 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) → ( 𝐼 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ↔ X 𝑘𝑋 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑛 ∈ ℕ X 𝑘𝑋 ( ( ( ( 𝐹𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) [,) ( ( ( 𝑆𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) ) ) )
129 63 128 mpbid ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝐼 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) → X 𝑘𝑋 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑛 ∈ ℕ X 𝑘𝑋 ( ( ( ( 𝐹𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) [,) ( ( ( 𝑆𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) ) )
130 129 3adant3r ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝐼 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → X 𝑘𝑋 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑛 ∈ ℕ X 𝑘𝑋 ( ( ( ( 𝐹𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) [,) ( ( ( 𝑆𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) ) )
131 6 16 17 18 48 62 130 hoidmvle ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝐼 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → ( 𝐴 ( 𝐿𝑋 ) 𝐵 ) ≤ ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( ( 𝐹𝑖 ) ‘ 𝑛 ) ( 𝐿𝑋 ) ( ( 𝑆𝑖 ) ‘ 𝑛 ) ) ) ) )
132 simpl ( ( 𝑛 = 𝑗𝑙𝑋 ) → 𝑛 = 𝑗 )
133 132 fveq2d ( ( 𝑛 = 𝑗𝑙𝑋 ) → ( 𝑖𝑛 ) = ( 𝑖𝑗 ) )
134 133 fveq1d ( ( 𝑛 = 𝑗𝑙𝑋 ) → ( ( 𝑖𝑛 ) ‘ 𝑙 ) = ( ( 𝑖𝑗 ) ‘ 𝑙 ) )
135 134 fveq2d ( ( 𝑛 = 𝑗𝑙𝑋 ) → ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) = ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑙 ) ) )
136 135 mpteq2dva ( 𝑛 = 𝑗 → ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) = ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑙 ) ) ) )
137 136 fveq1d ( 𝑛 = 𝑗 → ( ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) )
138 137 adantr ( ( 𝑛 = 𝑗𝑘𝑋 ) → ( ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) )
139 eqidd ( 𝑘𝑋 → ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑙 ) ) ) = ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑙 ) ) ) )
140 2fveq3 ( 𝑙 = 𝑘 → ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑙 ) ) = ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) )
141 140 adantl ( ( 𝑘𝑋𝑙 = 𝑘 ) → ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑙 ) ) = ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) )
142 id ( 𝑘𝑋𝑘𝑋 )
143 fvexd ( 𝑘𝑋 → ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) ∈ V )
144 139 141 142 143 fvmptd ( 𝑘𝑋 → ( ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) )
145 144 adantl ( ( 𝑛 = 𝑗𝑘𝑋 ) → ( ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) )
146 138 145 eqtrd ( ( 𝑛 = 𝑗𝑘𝑋 ) → ( ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) )
147 134 fveq2d ( ( 𝑛 = 𝑗𝑙𝑋 ) → ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) = ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑙 ) ) )
148 147 mpteq2dva ( 𝑛 = 𝑗 → ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) = ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑙 ) ) ) )
149 148 fveq1d ( 𝑛 = 𝑗 → ( ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) )
150 149 adantr ( ( 𝑛 = 𝑗𝑘𝑋 ) → ( ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) )
151 eqidd ( 𝑘𝑋 → ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑙 ) ) ) = ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑙 ) ) ) )
152 2fveq3 ( 𝑙 = 𝑘 → ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑙 ) ) = ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) )
153 152 adantl ( ( 𝑘𝑋𝑙 = 𝑘 ) → ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑙 ) ) = ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) )
154 fvexd ( 𝑘𝑋 → ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) ∈ V )
155 151 153 142 154 fvmptd ( 𝑘𝑋 → ( ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) )
156 155 adantl ( ( 𝑛 = 𝑗𝑘𝑋 ) → ( ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) )
157 150 156 eqtrd ( ( 𝑛 = 𝑗𝑘𝑋 ) → ( ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) )
158 146 157 oveq12d ( ( 𝑛 = 𝑗𝑘𝑋 ) → ( ( ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) = ( ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) ) )
159 158 fveq2d ( ( 𝑛 = 𝑗𝑘𝑋 ) → ( vol ‘ ( ( ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) ) ) )
160 159 prodeq2dv ( 𝑛 = 𝑗 → ∏ 𝑘𝑋 ( vol ‘ ( ( ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) = ∏ 𝑘𝑋 ( vol ‘ ( ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) ) ) )
161 160 cbvmptv ( 𝑛 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) ) ) )
162 161 a1i ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( 𝑛 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) ) ) ) )
163 78 eqcomd ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) ) = ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) )
164 163 fveq2d ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( vol ‘ ( ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) ) ) = ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) )
165 164 prodeq2dv ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑗 ∈ ℕ ) → ∏ 𝑘𝑋 ( vol ‘ ( ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) ) ) = ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) )
166 165 mpteq2dva ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) )
167 162 166 eqtrd ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( 𝑛 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) )
168 167 fveq2d ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) )
169 168 3ad2ant2 ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) )
170 92 adantll ( ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹𝑖 ) ‘ 𝑛 ) = ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) )
171 112 adantll ( ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑆𝑖 ) ‘ 𝑛 ) = ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) )
172 170 171 oveq12d ( ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝐹𝑖 ) ‘ 𝑛 ) ( 𝐿𝑋 ) ( ( 𝑆𝑖 ) ‘ 𝑛 ) ) = ( ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ( 𝐿𝑋 ) ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ) )
173 1 ad2antrr ( ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) ∧ 𝑛 ∈ ℕ ) → 𝑋 ∈ Fin )
174 2 ad2antrr ( ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) ∧ 𝑛 ∈ ℕ ) → 𝑋 ≠ ∅ )
175 23 adantlll ( ( ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑙𝑋 ) → ( ( 𝑖𝑛 ) ‘ 𝑙 ) ∈ ( ℝ × ℝ ) )
176 175 24 syl ( ( ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑙𝑋 ) → ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ∈ ℝ )
177 176 fmpttd ( ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) : 𝑋 ⟶ ℝ )
178 175 49 syl ( ( ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑙𝑋 ) → ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ∈ ℝ )
179 178 fmpttd ( ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) : 𝑋 ⟶ ℝ )
180 6 173 174 177 179 hoidmvn0val ( ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ( 𝐿𝑋 ) ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ) = ∏ 𝑘𝑋 ( vol ‘ ( ( ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) )
181 172 180 eqtrd ( ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝐹𝑖 ) ‘ 𝑛 ) ( 𝐿𝑋 ) ( ( 𝑆𝑖 ) ‘ 𝑛 ) ) = ∏ 𝑘𝑋 ( vol ‘ ( ( ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) )
182 181 mpteq2dva ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) → ( 𝑛 ∈ ℕ ↦ ( ( ( 𝐹𝑖 ) ‘ 𝑛 ) ( 𝐿𝑋 ) ( ( 𝑆𝑖 ) ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) ) )
183 182 fveq2d ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( ( 𝐹𝑖 ) ‘ 𝑛 ) ( 𝐿𝑋 ) ( ( 𝑆𝑖 ) ‘ 𝑛 ) ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) ) ) )
184 183 3adant3 ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( ( 𝐹𝑖 ) ‘ 𝑛 ) ( 𝐿𝑋 ) ( ( 𝑆𝑖 ) ‘ 𝑛 ) ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( ( 𝑙𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) ) ) )
185 simp3 ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) )
186 169 184 185 3eqtr4d ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( ( 𝐹𝑖 ) ‘ 𝑛 ) ( 𝐿𝑋 ) ( ( 𝑆𝑖 ) ‘ 𝑛 ) ) ) ) = 𝑧 )
187 186 3adant3l ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝐼 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( ( 𝐹𝑖 ) ‘ 𝑛 ) ( 𝐿𝑋 ) ( ( 𝑆𝑖 ) ‘ 𝑛 ) ) ) ) = 𝑧 )
188 131 187 breqtrd ( ( 𝜑𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝐼 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → ( 𝐴 ( 𝐿𝑋 ) 𝐵 ) ≤ 𝑧 )
189 188 3exp ( 𝜑 → ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( ( 𝐼 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → ( 𝐴 ( 𝐿𝑋 ) 𝐵 ) ≤ 𝑧 ) ) )
190 189 adantr ( ( 𝜑𝑧𝑀 ) → ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( ( 𝐼 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → ( 𝐴 ( 𝐿𝑋 ) 𝐵 ) ≤ 𝑧 ) ) )
191 190 rexlimdv ( ( 𝜑𝑧𝑀 ) → ( ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → ( 𝐴 ( 𝐿𝑋 ) 𝐵 ) ≤ 𝑧 ) )
192 15 191 mpd ( ( 𝜑𝑧𝑀 ) → ( 𝐴 ( 𝐿𝑋 ) 𝐵 ) ≤ 𝑧 )
193 192 ralrimiva ( 𝜑 → ∀ 𝑧𝑀 ( 𝐴 ( 𝐿𝑋 ) 𝐵 ) ≤ 𝑧 )
194 ssrab2 { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ⊆ ℝ*
195 7 194 eqsstri 𝑀 ⊆ ℝ*
196 195 a1i ( 𝜑𝑀 ⊆ ℝ* )
197 icossxr ( 0 [,) +∞ ) ⊆ ℝ*
198 6 1 3 4 hoidmvcl ( 𝜑 → ( 𝐴 ( 𝐿𝑋 ) 𝐵 ) ∈ ( 0 [,) +∞ ) )
199 197 198 sselid ( 𝜑 → ( 𝐴 ( 𝐿𝑋 ) 𝐵 ) ∈ ℝ* )
200 infxrgelb ( ( 𝑀 ⊆ ℝ* ∧ ( 𝐴 ( 𝐿𝑋 ) 𝐵 ) ∈ ℝ* ) → ( ( 𝐴 ( 𝐿𝑋 ) 𝐵 ) ≤ inf ( 𝑀 , ℝ* , < ) ↔ ∀ 𝑧𝑀 ( 𝐴 ( 𝐿𝑋 ) 𝐵 ) ≤ 𝑧 ) )
201 196 199 200 syl2anc ( 𝜑 → ( ( 𝐴 ( 𝐿𝑋 ) 𝐵 ) ≤ inf ( 𝑀 , ℝ* , < ) ↔ ∀ 𝑧𝑀 ( 𝐴 ( 𝐿𝑋 ) 𝐵 ) ≤ 𝑧 ) )
202 193 201 mpbird ( 𝜑 → ( 𝐴 ( 𝐿𝑋 ) 𝐵 ) ≤ inf ( 𝑀 , ℝ* , < ) )
203 5 a1i ( 𝜑𝐼 = X 𝑘𝑋 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
204 nfv 𝑘 𝜑
205 3 ffvelrnda ( ( 𝜑𝑘𝑋 ) → ( 𝐴𝑘 ) ∈ ℝ )
206 4 ffvelrnda ( ( 𝜑𝑘𝑋 ) → ( 𝐵𝑘 ) ∈ ℝ )
207 206 rexrd ( ( 𝜑𝑘𝑋 ) → ( 𝐵𝑘 ) ∈ ℝ* )
208 204 205 207 hoissrrn2 ( 𝜑X 𝑘𝑋 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ ( ℝ ↑m 𝑋 ) )
209 203 208 eqsstrd ( 𝜑𝐼 ⊆ ( ℝ ↑m 𝑋 ) )
210 1 2 209 7 ovnn0val ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐼 ) = inf ( 𝑀 , ℝ* , < ) )
211 210 eqcomd ( 𝜑 → inf ( 𝑀 , ℝ* , < ) = ( ( voln* ‘ 𝑋 ) ‘ 𝐼 ) )
212 202 211 breqtrd ( 𝜑 → ( 𝐴 ( 𝐿𝑋 ) 𝐵 ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝐼 ) )