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 ℕ ) ↦ ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) )
	ovnhoilem2.s	⊢ 𝑆 = ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ↦ ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) )
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 ℕ ) ↦ ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) )
9		ovnhoilem2.s	⊢ 𝑆 = ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ↦ ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) )
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	ffvelcdmda	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑖 ‘ 𝑛 ) ∈ ( ( ℝ × ℝ ) ↑_m 𝑋 ) )
21		elmapi	⊢ ( ( 𝑖 ‘ 𝑛 ) ∈ ( ( ℝ × ℝ ) ↑_m 𝑋 ) → ( 𝑖 ‘ 𝑛 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
22	20 21	syl	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑖 ‘ 𝑛 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
23	22	ffvelcdmda	⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑙 ∈ 𝑋 ) → ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ∈ ( ℝ × ℝ ) )
24		xp1st	⊢ ( ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ∈ ( ℝ × ℝ ) → ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ∈ ℝ )
25	23 24	syl	⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑙 ∈ 𝑋 ) → ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ∈ ℝ )
26	25	fmpttd	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) : 𝑋 ⟶ ℝ )
27		reex	⊢ ℝ ∈ V
28	27	a1i	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ℝ ∈ V )
29		1nn	⊢ 1 ∈ ℕ
30	29	a1i	⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) → 1 ∈ ℕ )
31	19 30	ffvelcdmd	⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_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 ) → ( ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ∈ ( ℝ ↑_m 𝑋 ) ↔ ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) : 𝑋 ⟶ ℝ ) )
37	28 35 36	syl2anc	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ∈ ( ℝ ↑_m 𝑋 ) ↔ ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) : 𝑋 ⟶ ℝ ) )
38	26 37	mpbird	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ∈ ( ℝ ↑_m 𝑋 ) )
39	38	fmpttd	⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) → ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) : ℕ ⟶ ( ℝ ↑_m 𝑋 ) )
40		id	⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) → 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) )
41		nnex	⊢ ℕ ∈ V
42	41	mptex	⊢ ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ∈ V
43	42	a1i	⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) → ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ∈ V )
44	8	fvmpt2	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ∈ V ) → ( 𝐹 ‘ 𝑖 ) = ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) )
45	40 43 44	syl2anc	⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) → ( 𝐹 ‘ 𝑖 ) = ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) )
46	45	feq1d	⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) → ( ( 𝐹 ‘ 𝑖 ) : ℕ ⟶ ( ℝ ↑_m 𝑋 ) ↔ ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) : ℕ ⟶ ( ℝ ↑_m 𝑋 ) ) )
47	39 46	mpbird	⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) → ( 𝐹 ‘ 𝑖 ) : ℕ ⟶ ( ℝ ↑_m 𝑋 ) )
48	47	3ad2ant2	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → ( 𝐹 ‘ 𝑖 ) : ℕ ⟶ ( ℝ ↑_m 𝑋 ) )
49		xp2nd	⊢ ( ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ∈ ( ℝ × ℝ ) → ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ∈ ℝ )
50	23 49	syl	⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑙 ∈ 𝑋 ) → ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ∈ ℝ )
51	50	fmpttd	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) : 𝑋 ⟶ ℝ )
52		elmapg	⊢ ( ( ℝ ∈ V ∧ 𝑋 ∈ V ) → ( ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ∈ ( ℝ ↑_m 𝑋 ) ↔ ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) : 𝑋 ⟶ ℝ ) )
53	28 35 52	syl2anc	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ∈ ( ℝ ↑_m 𝑋 ) ↔ ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) : 𝑋 ⟶ ℝ ) )
54	51 53	mpbird	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ∈ ( ℝ ↑_m 𝑋 ) )
55	54	fmpttd	⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) → ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) : ℕ ⟶ ( ℝ ↑_m 𝑋 ) )
56	41	mptex	⊢ ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ∈ V
57	56	a1i	⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) → ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ∈ V )
58	9	fvmpt2	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ∈ V ) → ( 𝑆 ‘ 𝑖 ) = ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) )
59	40 57 58	syl2anc	⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) → ( 𝑆 ‘ 𝑖 ) = ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) )
60	59	feq1d	⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) → ( ( 𝑆 ‘ 𝑖 ) : ℕ ⟶ ( ℝ ↑_m 𝑋 ) ↔ ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) : ℕ ⟶ ( ℝ ↑_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	⊢ ( 𝑗 = 𝑛 → ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) = ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) )
68	66	fveq2d	⊢ ( 𝑗 = 𝑛 → ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) = ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) )
69	67 68	oveq12d	⊢ ( 𝑗 = 𝑛 → ( ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) = ( ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) ) )
70	69	ixpeq2dv	⊢ ( 𝑗 = 𝑛 → X 𝑘 ∈ 𝑋 ( ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) = X 𝑘 ∈ 𝑋 ( ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) ) )
71	70	cbviunv	⊢ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) = ∪ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) )
72	71	a1i	⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) → ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) = ∪ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) ) )
73	19	ffvelcdmda	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_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 ℕ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) )
79	78	ixpeq2dva	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑗 ∈ ℕ ) → X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = X 𝑘 ∈ 𝑋 ( ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) )
80	79	iuneq2dv	⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) → ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) )
81		simpl	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) )
82	42	a1i	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ∈ V )
83	81 82 44	syl2anc	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑖 ) = ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) )
84	83	fveq1d	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ‘ 𝑛 ) )
85		simpr	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
86		mptexg	⊢ ( 𝑋 ∈ V → ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ∈ V )
87	34 86	syl	⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) → ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ∈ V )
88	87	adantr	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ∈ V )
89		eqid	⊢ ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) )
90	89	fvmpt2	⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ∈ V ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ‘ 𝑛 ) = ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) )
91	85 88 90	syl2anc	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ‘ 𝑛 ) = ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) )
92	84 91	eqtrd	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) = ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) )
93	92	fveq1d	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) = ( ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) )
94	93	adantr	⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) = ( ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) )
95		eqidd	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) = ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) )
96		simpr	⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑙 = 𝑘 ) → 𝑙 = 𝑘 )
97	96	fveq2d	⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑙 = 𝑘 ) → ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) = ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) )
98	97	fveq2d	⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑙 = 𝑘 ) → ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) = ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) )
99		simpr	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑘 ∈ 𝑋 ) → 𝑘 ∈ 𝑋 )
100		fvexd	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) ∈ V )
101	95 98 99 100	fvmptd	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) )
102	101	adantlr	⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) )
103	94 102	eqtrd	⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) = ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) )
104	59	fveq1d	⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) → ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ‘ 𝑛 ) )
105	104	adantr	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ‘ 𝑛 ) )
106		mptexg	⊢ ( 𝑋 ∈ V → ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ∈ V )
107	34 106	syl	⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) → ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ∈ V )
108	107	adantr	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ∈ V )
109		eqid	⊢ ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) )
110	109	fvmpt2	⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ∈ V ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ‘ 𝑛 ) = ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) )
111	85 108 110	syl2anc	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ‘ 𝑛 ) = ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) )
112	105 111	eqtrd	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) = ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) )
113	112	fveq1d	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) = ( ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) )
114	113	adantr	⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) = ( ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) )
115		eqidd	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) = ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) )
116		2fveq3	⊢ ( 𝑙 = 𝑘 → ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) = ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) )
117	116	adantl	⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑙 = 𝑘 ) → ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) = ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) )
118		fvexd	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) ∈ V )
119	115 117 99 118	fvmptd	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) )
120	119	adantlr	⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) )
121	114 120	eqtrd	⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) = ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) )
122	103 121	oveq12d	⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) [,) ( ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) ) = ( ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) ) )
123	122	ixpeq2dva	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → X 𝑘 ∈ 𝑋 ( ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) [,) ( ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) ) = X 𝑘 ∈ 𝑋 ( ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) ) )
124	123	iuneq2dv	⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) → ∪ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) [,) ( ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) ) = ∪ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) ) )
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	⊢ ( ( 𝑛 = 𝑗 ∧ 𝑙 ∈ 𝑋 ) → ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) = ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) )
136	135	mpteq2dva	⊢ ( 𝑛 = 𝑗 → ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) = ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) )
137	136	fveq1d	⊢ ( 𝑛 = 𝑗 → ( ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) )
138	137	adantr	⊢ ( ( 𝑛 = 𝑗 ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) )
139		eqidd	⊢ ( 𝑘 ∈ 𝑋 → ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) = ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) )
140		2fveq3	⊢ ( 𝑙 = 𝑘 → ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) = ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) )
141	140	adantl	⊢ ( ( 𝑘 ∈ 𝑋 ∧ 𝑙 = 𝑘 ) → ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) = ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) )
142		id	⊢ ( 𝑘 ∈ 𝑋 → 𝑘 ∈ 𝑋 )
143		fvexd	⊢ ( 𝑘 ∈ 𝑋 → ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ∈ V )
144	139 141 142 143	fvmptd	⊢ ( 𝑘 ∈ 𝑋 → ( ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) )
145	144	adantl	⊢ ( ( 𝑛 = 𝑗 ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) )
146	138 145	eqtrd	⊢ ( ( 𝑛 = 𝑗 ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) )
147	134	fveq2d	⊢ ( ( 𝑛 = 𝑗 ∧ 𝑙 ∈ 𝑋 ) → ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) = ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) )
148	147	mpteq2dva	⊢ ( 𝑛 = 𝑗 → ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) = ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) )
149	148	fveq1d	⊢ ( 𝑛 = 𝑗 → ( ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) )
150	149	adantr	⊢ ( ( 𝑛 = 𝑗 ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) )
151		eqidd	⊢ ( 𝑘 ∈ 𝑋 → ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) = ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) )
152		2fveq3	⊢ ( 𝑙 = 𝑘 → ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) = ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) )
153	152	adantl	⊢ ( ( 𝑘 ∈ 𝑋 ∧ 𝑙 = 𝑘 ) → ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) = ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) )
154		fvexd	⊢ ( 𝑘 ∈ 𝑋 → ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ∈ V )
155	151 153 142 154	fvmptd	⊢ ( 𝑘 ∈ 𝑋 → ( ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) )
156	155	adantl	⊢ ( ( 𝑛 = 𝑗 ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) )
157	150 156	eqtrd	⊢ ( ( 𝑛 = 𝑗 ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) )
158	146 157	oveq12d	⊢ ( ( 𝑛 = 𝑗 ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) = ( ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) )
159	158	fveq2d	⊢ ( ( 𝑛 = 𝑗 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) )
160	159	prodeq2dv	⊢ ( 𝑛 = 𝑗 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) )
161	160	cbvmptv	⊢ ( 𝑛 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) )
162	161	a1i	⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) → ( 𝑛 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) ) )
163	78	eqcomd	⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) = ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) )
164	163	fveq2d	⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) = ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
165	164	prodeq2dv	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑗 ∈ ℕ ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
166	165	mpteq2dva	⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) → ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) )
167	162 166	eqtrd	⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) → ( 𝑛 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) )
168	167	fveq2d	⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) → ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) ) ) = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
169	168	3ad2ant2	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) ) ) = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
170	92	adantll	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) = ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) )
171	112	adantll	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) = ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) )
172	170 171	oveq12d	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) ) = ( ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ( 𝐿 ‘ 𝑋 ) ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) )
173	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ) ∧ 𝑛 ∈ ℕ ) → 𝑋 ∈ Fin )
174	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ) ∧ 𝑛 ∈ ℕ ) → 𝑋 ≠ ∅ )
175	23	adantlll	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑙 ∈ 𝑋 ) → ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ∈ ( ℝ × ℝ ) )
176	175 24	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑙 ∈ 𝑋 ) → ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ∈ ℝ )
177	176	fmpttd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) : 𝑋 ⟶ ℝ )
178	175 49	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑙 ∈ 𝑋 ) → ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ∈ ℝ )
179	178	fmpttd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) : 𝑋 ⟶ ℝ )
180	6 173 174 177 179	hoidmvn0val	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ( 𝐿 ‘ 𝑋 ) ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) )
181	172 180	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) )
182	181	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ) → ( 𝑛 ∈ ℕ ↦ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) ) )
183	182	fveq2d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ) → ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) = ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) ) ) )
184	183	3adant3	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) = ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝑙 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) ) ) )
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	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
206	4	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
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* ‘ 𝑋 ) ‘ 𝐼 ) )

Metamath Proof Explorer

Theorem ovnhoilem2

Proof