ovnsubaddlem1

Description: The Lebesgue outer measure is subadditive. Proposition 115D (a)(iv) of Fremlin1 p. 31 . (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	ovnsubaddlem1.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	ovnsubaddlem1.n0	⊢ ( 𝜑 → 𝑋 ≠ ∅ )
	ovnsubaddlem1.a	⊢ ( 𝜑 → 𝐴 : ℕ ⟶ 𝒫 ( ℝ ↑_m 𝑋 ) )
	ovnsubaddlem1.e	⊢ ( 𝜑 → 𝐸 ∈ ℝ⁺ )
	ovnsubaddlem1.z	⊢ 𝑍 = ( 𝑎 ∈ 𝒫 ( ℝ ↑_m 𝑋 ) ↦ { 𝑧 ∈ ℝ^* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } )
	ovnsubaddlem1.c	⊢ 𝐶 = ( 𝑎 ∈ 𝒫 ( ℝ ↑_m 𝑋 ) ↦ { ℎ ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) } )
	ovnsubaddlem1.l	⊢ 𝐿 = ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑘 ) ) )
	ovnsubaddlem1.d	⊢ 𝐷 = ( 𝑎 ∈ 𝒫 ( ℝ ↑_m 𝑋 ) ↦ ( 𝑒 ∈ ℝ⁺ ↦ { 𝑖 ∈ ( 𝐶 ‘ 𝑎 ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +_𝑒 𝑒 ) } ) )
	ovnsubaddlem1.i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐼 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) )
	ovnsubaddlem1.f	⊢ ( 𝜑 → 𝐹 : ℕ –1-1-onto→ ( ℕ × ℕ ) )
	ovnsubaddlem1.g	⊢ 𝐺 = ( 𝑚 ∈ ℕ ↦ ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) )
Assertion	ovnsubaddlem1	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ≤ ( ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) +_𝑒 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		ovnsubaddlem1.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		ovnsubaddlem1.n0	⊢ ( 𝜑 → 𝑋 ≠ ∅ )
3		ovnsubaddlem1.a	⊢ ( 𝜑 → 𝐴 : ℕ ⟶ 𝒫 ( ℝ ↑_m 𝑋 ) )
4		ovnsubaddlem1.e	⊢ ( 𝜑 → 𝐸 ∈ ℝ⁺ )
5		ovnsubaddlem1.z	⊢ 𝑍 = ( 𝑎 ∈ 𝒫 ( ℝ ↑_m 𝑋 ) ↦ { 𝑧 ∈ ℝ^* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } )
6		ovnsubaddlem1.c	⊢ 𝐶 = ( 𝑎 ∈ 𝒫 ( ℝ ↑_m 𝑋 ) ↦ { ℎ ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) } )
7		ovnsubaddlem1.l	⊢ 𝐿 = ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑘 ) ) )
8		ovnsubaddlem1.d	⊢ 𝐷 = ( 𝑎 ∈ 𝒫 ( ℝ ↑_m 𝑋 ) ↦ ( 𝑒 ∈ ℝ⁺ ↦ { 𝑖 ∈ ( 𝐶 ‘ 𝑎 ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +_𝑒 𝑒 ) } ) )
9		ovnsubaddlem1.i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐼 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) )
10		ovnsubaddlem1.f	⊢ ( 𝜑 → 𝐹 : ℕ –1-1-onto→ ( ℕ × ℕ ) )
11		ovnsubaddlem1.g	⊢ 𝐺 = ( 𝑚 ∈ ℕ ↦ ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) )
12	3	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 : ℕ ⟶ 𝒫 ( ℝ ↑_m 𝑋 ) )
13		simpr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
14	12 13	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ‘ 𝑛 ) ∈ 𝒫 ( ℝ ↑_m 𝑋 ) )
15		elpwi	⊢ ( ( 𝐴 ‘ 𝑛 ) ∈ 𝒫 ( ℝ ↑_m 𝑋 ) → ( 𝐴 ‘ 𝑛 ) ⊆ ( ℝ ↑_m 𝑋 ) )
16	14 15	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ‘ 𝑛 ) ⊆ ( ℝ ↑_m 𝑋 ) )
17	16	ralrimiva	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ⊆ ( ℝ ↑_m 𝑋 ) )
18		iunss	⊢ ( ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ⊆ ( ℝ ↑_m 𝑋 ) ↔ ∀ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ⊆ ( ℝ ↑_m 𝑋 ) )
19	17 18	sylibr	⊢ ( 𝜑 → ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ⊆ ( ℝ ↑_m 𝑋 ) )
20	1 19	ovnxrcl	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ∈ ℝ^* )
21		nfv	⊢ Ⅎ 𝑚 𝜑
22		nnex	⊢ ℕ ∈ V
23	22	a1i	⊢ ( 𝜑 → ℕ ∈ V )
24		icossicc	⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
25		nfv	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑚 ∈ ℕ )
26		simpl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝜑 )
27	26 1	syl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑋 ∈ Fin )
28		f1of	⊢ ( 𝐹 : ℕ –1-1-onto→ ( ℕ × ℕ ) → 𝐹 : ℕ ⟶ ( ℕ × ℕ ) )
29	10 28	syl	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ℕ × ℕ ) )
30	29	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝐹 : ℕ ⟶ ( ℕ × ℕ ) )
31		simpr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℕ )
32	30 31	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐹 ‘ 𝑚 ) ∈ ( ℕ × ℕ ) )
33		xp1st	⊢ ( ( 𝐹 ‘ 𝑚 ) ∈ ( ℕ × ℕ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℕ )
34	32 33	syl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℕ )
35		xp2nd	⊢ ( ( 𝐹 ‘ 𝑚 ) ∈ ( ℕ × ℕ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℕ )
36	32 35	syl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℕ )
37		fvex	⊢ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ V
38		eleq1	⊢ ( 𝑗 = ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) → ( 𝑗 ∈ ℕ ↔ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℕ ) )
39	38	3anbi3d	⊢ ( 𝑗 = ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) → ( ( 𝜑 ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℕ ∧ 𝑗 ∈ ℕ ) ↔ ( 𝜑 ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℕ ) ) )
40		fveq2	⊢ ( 𝑗 = ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) → ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑗 ) = ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) )
41	40	feq1d	⊢ ( 𝑗 = ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) → ( ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) ↔ ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) : 𝑋 ⟶ ( ℝ × ℝ ) ) )
42	39 41	imbi12d	⊢ ( 𝑗 = ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) → ( ( ( 𝜑 ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) ) ↔ ( ( 𝜑 ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℕ ) → ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) : 𝑋 ⟶ ( ℝ × ℝ ) ) ) )
43		fvex	⊢ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ V
44		eleq1	⊢ ( 𝑛 = ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) → ( 𝑛 ∈ ℕ ↔ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℕ ) )
45	44	3anbi2d	⊢ ( 𝑛 = ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) → ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ↔ ( 𝜑 ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) )
46		fveq2	⊢ ( 𝑛 = ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) → ( 𝐼 ‘ 𝑛 ) = ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) )
47	46	fveq1d	⊢ ( 𝑛 = ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) → ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) = ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑗 ) )
48	47	feq1d	⊢ ( 𝑛 = ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) → ( ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) ↔ ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) ) )
49	45 48	imbi12d	⊢ ( 𝑛 = ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) → ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) ) ↔ ( ( 𝜑 ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) ) ) )
50		sseq1	⊢ ( 𝑎 = ( 𝐴 ‘ 𝑛 ) → ( 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) ↔ ( 𝐴 ‘ 𝑛 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
51	50	rabbidv	⊢ ( 𝑎 = ( 𝐴 ‘ 𝑛 ) → { ℎ ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) } = { ℎ ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∣ ( 𝐴 ‘ 𝑛 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) } )
52		ovex	⊢ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∈ V
53	52	rabex	⊢ { ℎ ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∣ ( 𝐴 ‘ 𝑛 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) } ∈ V
54	53	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → { ℎ ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∣ ( 𝐴 ‘ 𝑛 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) } ∈ V )
55	6 51 14 54	fvmptd3	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) = { ℎ ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∣ ( 𝐴 ‘ 𝑛 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) } )
56		ssrab2	⊢ { ℎ ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∣ ( 𝐴 ‘ 𝑛 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) } ⊆ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ )
57	56	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → { ℎ ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∣ ( 𝐴 ‘ 𝑛 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) } ⊆ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) )
58	55 57	eqsstrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) ⊆ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) )
59		fveq2	⊢ ( 𝑎 = ( 𝐴 ‘ 𝑛 ) → ( 𝐶 ‘ 𝑎 ) = ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) )
60	59	eleq2d	⊢ ( 𝑎 = ( 𝐴 ‘ 𝑛 ) → ( 𝑖 ∈ ( 𝐶 ‘ 𝑎 ) ↔ 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) ) )
61		fveq2	⊢ ( 𝑎 = ( 𝐴 ‘ 𝑛 ) → ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) = ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) )
62	61	oveq1d	⊢ ( 𝑎 = ( 𝐴 ‘ 𝑛 ) → ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +_𝑒 𝑒 ) = ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 𝑒 ) )
63	62	breq2d	⊢ ( 𝑎 = ( 𝐴 ‘ 𝑛 ) → ( ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +_𝑒 𝑒 ) ↔ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 𝑒 ) ) )
64	60 63	anbi12d	⊢ ( 𝑎 = ( 𝐴 ‘ 𝑛 ) → ( ( 𝑖 ∈ ( 𝐶 ‘ 𝑎 ) ∧ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +_𝑒 𝑒 ) ) ↔ ( 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) ∧ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 𝑒 ) ) ) )
65	64	rabbidva2	⊢ ( 𝑎 = ( 𝐴 ‘ 𝑛 ) → { 𝑖 ∈ ( 𝐶 ‘ 𝑎 ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +_𝑒 𝑒 ) } = { 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 𝑒 ) } )
66	65	mpteq2dv	⊢ ( 𝑎 = ( 𝐴 ‘ 𝑛 ) → ( 𝑒 ∈ ℝ⁺ ↦ { 𝑖 ∈ ( 𝐶 ‘ 𝑎 ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +_𝑒 𝑒 ) } ) = ( 𝑒 ∈ ℝ⁺ ↦ { 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 𝑒 ) } ) )
67		rpex	⊢ ℝ⁺ ∈ V
68	67	mptex	⊢ ( 𝑒 ∈ ℝ⁺ ↦ { 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 𝑒 ) } ) ∈ V
69	68	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑒 ∈ ℝ⁺ ↦ { 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 𝑒 ) } ) ∈ V )
70	8 66 14 69	fvmptd3	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) = ( 𝑒 ∈ ℝ⁺ ↦ { 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 𝑒 ) } ) )
71		oveq2	⊢ ( 𝑒 = ( 𝐸 / ( 2 ↑ 𝑛 ) ) → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 𝑒 ) = ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) )
72	71	breq2d	⊢ ( 𝑒 = ( 𝐸 / ( 2 ↑ 𝑛 ) ) → ( ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 𝑒 ) ↔ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) )
73	72	rabbidv	⊢ ( 𝑒 = ( 𝐸 / ( 2 ↑ 𝑛 ) ) → { 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 𝑒 ) } = { 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) } )
74	73	adantl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑒 = ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) → { 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 𝑒 ) } = { 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) } )
75	4	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐸 ∈ ℝ⁺ )
76		2nn	⊢ 2 ∈ ℕ
77	76	a1i	⊢ ( 𝑛 ∈ ℕ → 2 ∈ ℕ )
78		nnnn0	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ₀ )
79	77 78	nnexpcld	⊢ ( 𝑛 ∈ ℕ → ( 2 ↑ 𝑛 ) ∈ ℕ )
80	79	nnrpd	⊢ ( 𝑛 ∈ ℕ → ( 2 ↑ 𝑛 ) ∈ ℝ⁺ )
81	80	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2 ↑ 𝑛 ) ∈ ℝ⁺ )
82	75 81	rpdivcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐸 / ( 2 ↑ 𝑛 ) ) ∈ ℝ⁺ )
83		fvex	⊢ ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ V
84	83	rabex	⊢ { 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) } ∈ V
85	84	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → { 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) } ∈ V )
86	70 74 82 85	fvmptd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) = { 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) } )
87		ssrab2	⊢ { 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) } ⊆ ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) )
88	87	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → { 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) } ⊆ ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) )
89	86 88	eqsstrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ⊆ ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) )
90	89 9	sseldd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐼 ‘ 𝑛 ) ∈ ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) )
91	58 90	sseldd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐼 ‘ 𝑛 ) ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) )
92		elmapfn	⊢ ( ( 𝐼 ‘ 𝑛 ) ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) → ( 𝐼 ‘ 𝑛 ) Fn ℕ )
93	91 92	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐼 ‘ 𝑛 ) Fn ℕ )
94		elmapi	⊢ ( ( 𝐼 ‘ 𝑛 ) ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) → ( 𝐼 ‘ 𝑛 ) : ℕ ⟶ ( ( ℝ × ℝ ) ↑_m 𝑋 ) )
95	91 94	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐼 ‘ 𝑛 ) : ℕ ⟶ ( ( ℝ × ℝ ) ↑_m 𝑋 ) )
96	95	ffvelrnda	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ∈ ( ( ℝ × ℝ ) ↑_m 𝑋 ) )
97	96	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∀ 𝑗 ∈ ℕ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ∈ ( ( ℝ × ℝ ) ↑_m 𝑋 ) )
98	93 97	jca	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐼 ‘ 𝑛 ) Fn ℕ ∧ ∀ 𝑗 ∈ ℕ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ∈ ( ( ℝ × ℝ ) ↑_m 𝑋 ) ) )
99	98	3adant3	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( ( 𝐼 ‘ 𝑛 ) Fn ℕ ∧ ∀ 𝑗 ∈ ℕ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ∈ ( ( ℝ × ℝ ) ↑_m 𝑋 ) ) )
100		ffnfv	⊢ ( ( 𝐼 ‘ 𝑛 ) : ℕ ⟶ ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↔ ( ( 𝐼 ‘ 𝑛 ) Fn ℕ ∧ ∀ 𝑗 ∈ ℕ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ∈ ( ( ℝ × ℝ ) ↑_m 𝑋 ) ) )
101	99 100	sylibr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( 𝐼 ‘ 𝑛 ) : ℕ ⟶ ( ( ℝ × ℝ ) ↑_m 𝑋 ) )
102		simp3	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ )
103	101 102	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ∈ ( ( ℝ × ℝ ) ↑_m 𝑋 ) )
104		elmapi	⊢ ( ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ∈ ( ( ℝ × ℝ ) ↑_m 𝑋 ) → ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
105	103 104	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
106	43 49 105	vtocl	⊢ ( ( 𝜑 ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
107	37 42 106	vtocl	⊢ ( ( 𝜑 ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℕ ) → ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) : 𝑋 ⟶ ( ℝ × ℝ ) )
108	26 34 36 107	syl3anc	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) : 𝑋 ⟶ ( ℝ × ℝ ) )
109		id	⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℕ )
110		fvex	⊢ ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) ∈ V
111	110	a1i	⊢ ( 𝑚 ∈ ℕ → ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) ∈ V )
112	11	fvmpt2	⊢ ( ( 𝑚 ∈ ℕ ∧ ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) ∈ V ) → ( 𝐺 ‘ 𝑚 ) = ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) )
113	109 111 112	syl2anc	⊢ ( 𝑚 ∈ ℕ → ( 𝐺 ‘ 𝑚 ) = ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) )
114	113	adantl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐺 ‘ 𝑚 ) = ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) )
115	114	feq1d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝐺 ‘ 𝑚 ) : 𝑋 ⟶ ( ℝ × ℝ ) ↔ ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) : 𝑋 ⟶ ( ℝ × ℝ ) ) )
116	108 115	mpbird	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐺 ‘ 𝑚 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
117	25 27 7 116	hoiprodcl2	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐿 ‘ ( 𝐺 ‘ 𝑚 ) ) ∈ ( 0 [,) +∞ ) )
118	24 117	sselid	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐿 ‘ ( 𝐺 ‘ 𝑚 ) ) ∈ ( 0 [,] +∞ ) )
119	21 23 118	sge0xrclmpt	⊢ ( 𝜑 → ( Σ^{^} ‘ ( 𝑚 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ∈ ℝ^* )
120		nfv	⊢ Ⅎ 𝑛 𝜑
121		0xr	⊢ 0 ∈ ℝ^*
122	121	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 ∈ ℝ^* )
123		pnfxr	⊢ +∞ ∈ ℝ^*
124	123	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → +∞ ∈ ℝ^* )
125	1	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑋 ∈ Fin )
126	125 16 5	ovnval2b	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) = if ( 𝑋 = ∅ , 0 , inf ( ( 𝑍 ‘ ( 𝐴 ‘ 𝑛 ) ) , ℝ^* , < ) ) )
127	2	neneqd	⊢ ( 𝜑 → ¬ 𝑋 = ∅ )
128	127	iffalsed	⊢ ( 𝜑 → if ( 𝑋 = ∅ , 0 , inf ( ( 𝑍 ‘ ( 𝐴 ‘ 𝑛 ) ) , ℝ^* , < ) ) = inf ( ( 𝑍 ‘ ( 𝐴 ‘ 𝑛 ) ) , ℝ^* , < ) )
129	128	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → if ( 𝑋 = ∅ , 0 , inf ( ( 𝑍 ‘ ( 𝐴 ‘ 𝑛 ) ) , ℝ^* , < ) ) = inf ( ( 𝑍 ‘ ( 𝐴 ‘ 𝑛 ) ) , ℝ^* , < ) )
130	126 129	eqtrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) = inf ( ( 𝑍 ‘ ( 𝐴 ‘ 𝑛 ) ) , ℝ^* , < ) )
131		sseq1	⊢ ( 𝑎 = ( 𝐴 ‘ 𝑛 ) → ( 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ↔ ( 𝐴 ‘ 𝑛 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
132	131	anbi1d	⊢ ( 𝑎 = ( 𝐴 ‘ 𝑛 ) → ( ( 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ↔ ( ( 𝐴 ‘ 𝑛 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
133	132	rexbidv	⊢ ( 𝑎 = ( 𝐴 ‘ 𝑛 ) → ( ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ↔ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( ( 𝐴 ‘ 𝑛 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
134	133	rabbidv	⊢ ( 𝑎 = ( 𝐴 ‘ 𝑛 ) → { 𝑧 ∈ ℝ^* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } = { 𝑧 ∈ ℝ^* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( ( 𝐴 ‘ 𝑛 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } )
135		xrex	⊢ ℝ^* ∈ V
136	135	rabex	⊢ { 𝑧 ∈ ℝ^* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( ( 𝐴 ‘ 𝑛 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ∈ V
137	136	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → { 𝑧 ∈ ℝ^* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( ( 𝐴 ‘ 𝑛 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ∈ V )
138	5 134 14 137	fvmptd3	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑍 ‘ ( 𝐴 ‘ 𝑛 ) ) = { 𝑧 ∈ ℝ^* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( ( 𝐴 ‘ 𝑛 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } )
139		ssrab2	⊢ { 𝑧 ∈ ℝ^* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( ( 𝐴 ‘ 𝑛 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ⊆ ℝ^*
140	139	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → { 𝑧 ∈ ℝ^* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( ( 𝐴 ‘ 𝑛 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ⊆ ℝ^* )
141	138 140	eqsstrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑍 ‘ ( 𝐴 ‘ 𝑛 ) ) ⊆ ℝ^* )
142		infxrcl	⊢ ( ( 𝑍 ‘ ( 𝐴 ‘ 𝑛 ) ) ⊆ ℝ^* → inf ( ( 𝑍 ‘ ( 𝐴 ‘ 𝑛 ) ) , ℝ^* , < ) ∈ ℝ^* )
143	141 142	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → inf ( ( 𝑍 ‘ ( 𝐴 ‘ 𝑛 ) ) , ℝ^* , < ) ∈ ℝ^* )
144	130 143	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ ℝ^* )
145	4	rpred	⊢ ( 𝜑 → 𝐸 ∈ ℝ )
146	145	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐸 ∈ ℝ )
147		2re	⊢ 2 ∈ ℝ
148	147	a1i	⊢ ( 𝑛 ∈ ℕ → 2 ∈ ℝ )
149	148 78	reexpcld	⊢ ( 𝑛 ∈ ℕ → ( 2 ↑ 𝑛 ) ∈ ℝ )
150	149	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2 ↑ 𝑛 ) ∈ ℝ )
151	148	recnd	⊢ ( 𝑛 ∈ ℕ → 2 ∈ ℂ )
152		2ne0	⊢ 2 ≠ 0
153	152	a1i	⊢ ( 𝑛 ∈ ℕ → 2 ≠ 0 )
154		nnz	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℤ )
155	151 153 154	expne0d	⊢ ( 𝑛 ∈ ℕ → ( 2 ↑ 𝑛 ) ≠ 0 )
156	155	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2 ↑ 𝑛 ) ≠ 0 )
157	146 150 156	redivcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐸 / ( 2 ↑ 𝑛 ) ) ∈ ℝ )
158	157	rexrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐸 / ( 2 ↑ 𝑛 ) ) ∈ ℝ^* )
159	144 158	xaddcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ∈ ℝ^* )
160	125 16	ovncl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ ( 0 [,] +∞ ) )
161		xrge0ge0	⊢ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ ( 0 [,] +∞ ) → 0 ≤ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) )
162	160 161	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 ≤ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) )
163		0red	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 ∈ ℝ )
164	82	rpgt0d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 < ( 𝐸 / ( 2 ↑ 𝑛 ) ) )
165	163 157 164	ltled	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 ≤ ( 𝐸 / ( 2 ↑ 𝑛 ) ) )
166	157	ltpnfd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐸 / ( 2 ↑ 𝑛 ) ) < +∞ )
167	158 124 166	xrltled	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐸 / ( 2 ↑ 𝑛 ) ) ≤ +∞ )
168	122 124 158 165 167	eliccxrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐸 / ( 2 ↑ 𝑛 ) ) ∈ ( 0 [,] +∞ ) )
169	144 168	xadd0ge	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) )
170	122 144 159 162 169	xrletrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) )
171		pnfge	⊢ ( ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ∈ ℝ^* → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≤ +∞ )
172	159 171	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≤ +∞ )
173	122 124 159 170 172	eliccxrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ∈ ( 0 [,] +∞ ) )
174	120 23 173	sge0xrclmpt	⊢ ( 𝜑 → ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) ∈ ℝ^* )
175		sseq1	⊢ ( 𝑎 = ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) → ( 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) ↔ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
176	175	rabbidv	⊢ ( 𝑎 = ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) → { ℎ ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) } = { ℎ ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∣ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) } )
177	3	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝐴 : ℕ ⟶ 𝒫 ( ℝ ↑_m 𝑋 ) )
178	177 34	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ∈ 𝒫 ( ℝ ↑_m 𝑋 ) )
179	52	rabex	⊢ { ℎ ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∣ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) } ∈ V
180	179	a1i	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → { ℎ ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∣ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) } ∈ V )
181	6 176 178 180	fvmptd3	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐶 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) = { ℎ ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∣ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) } )
182		ssrab2	⊢ { ℎ ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∣ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) } ⊆ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ )
183	182	a1i	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → { ℎ ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∣ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) } ⊆ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) )
184	181 183	eqsstrd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐶 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ⊆ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) )
185		fveq2	⊢ ( 𝑎 = ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) → ( 𝐶 ‘ 𝑎 ) = ( 𝐶 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) )
186	185	eleq2d	⊢ ( 𝑎 = ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) → ( 𝑖 ∈ ( 𝐶 ‘ 𝑎 ) ↔ 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ) )
187		fveq2	⊢ ( 𝑎 = ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) → ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) = ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) )
188	187	oveq1d	⊢ ( 𝑎 = ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) → ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +_𝑒 𝑒 ) = ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) +_𝑒 𝑒 ) )
189	188	breq2d	⊢ ( 𝑎 = ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) → ( ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +_𝑒 𝑒 ) ↔ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) +_𝑒 𝑒 ) ) )
190	186 189	anbi12d	⊢ ( 𝑎 = ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) → ( ( 𝑖 ∈ ( 𝐶 ‘ 𝑎 ) ∧ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +_𝑒 𝑒 ) ) ↔ ( 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ∧ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) +_𝑒 𝑒 ) ) ) )
191	190	rabbidva2	⊢ ( 𝑎 = ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) → { 𝑖 ∈ ( 𝐶 ‘ 𝑎 ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +_𝑒 𝑒 ) } = { 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) +_𝑒 𝑒 ) } )
192	191	mpteq2dv	⊢ ( 𝑎 = ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) → ( 𝑒 ∈ ℝ⁺ ↦ { 𝑖 ∈ ( 𝐶 ‘ 𝑎 ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +_𝑒 𝑒 ) } ) = ( 𝑒 ∈ ℝ⁺ ↦ { 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) +_𝑒 𝑒 ) } ) )
193	67	mptex	⊢ ( 𝑒 ∈ ℝ⁺ ↦ { 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) +_𝑒 𝑒 ) } ) ∈ V
194	193	a1i	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑒 ∈ ℝ⁺ ↦ { 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) +_𝑒 𝑒 ) } ) ∈ V )
195	8 192 178 194	fvmptd3	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐷 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) = ( 𝑒 ∈ ℝ⁺ ↦ { 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) +_𝑒 𝑒 ) } ) )
196		oveq2	⊢ ( 𝑒 = ( 𝐸 / ( 2 ↑ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) +_𝑒 𝑒 ) = ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) +_𝑒 ( 𝐸 / ( 2 ↑ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ) )
197	196	breq2d	⊢ ( 𝑒 = ( 𝐸 / ( 2 ↑ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) → ( ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) +_𝑒 𝑒 ) ↔ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) +_𝑒 ( 𝐸 / ( 2 ↑ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ) ) )
198	197	rabbidv	⊢ ( 𝑒 = ( 𝐸 / ( 2 ↑ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) → { 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) +_𝑒 𝑒 ) } = { 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) +_𝑒 ( 𝐸 / ( 2 ↑ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ) } )
199	198	adantl	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑒 = ( 𝐸 / ( 2 ↑ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ) → { 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) +_𝑒 𝑒 ) } = { 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) +_𝑒 ( 𝐸 / ( 2 ↑ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ) } )
200	26 4	syl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝐸 ∈ ℝ⁺ )
201		2rp	⊢ 2 ∈ ℝ⁺
202	201	a1i	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 2 ∈ ℝ⁺ )
203	34	nnzd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℤ )
204	202 203	rpexpcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 2 ↑ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ∈ ℝ⁺ )
205	200 204	rpdivcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐸 / ( 2 ↑ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ∈ ℝ⁺ )
206		fvex	⊢ ( 𝐶 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ∈ V
207	206	rabex	⊢ { 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) +_𝑒 ( 𝐸 / ( 2 ↑ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ) } ∈ V
208	207	a1i	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → { 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) +_𝑒 ( 𝐸 / ( 2 ↑ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ) } ∈ V )
209	195 199 205 208	fvmptd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝐷 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ ( 𝐸 / ( 2 ↑ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ) = { 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) +_𝑒 ( 𝐸 / ( 2 ↑ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ) } )
210		ssrab2	⊢ { 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) +_𝑒 ( 𝐸 / ( 2 ↑ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ) } ⊆ ( 𝐶 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) )
211	210	a1i	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → { 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) +_𝑒 ( 𝐸 / ( 2 ↑ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ) } ⊆ ( 𝐶 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) )
212	209 211	eqsstrd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝐷 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ ( 𝐸 / ( 2 ↑ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ) ⊆ ( 𝐶 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) )
213	44	anbi2d	⊢ ( 𝑛 = ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) → ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ↔ ( 𝜑 ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℕ ) ) )
214		2fveq3	⊢ ( 𝑛 = ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) → ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) = ( 𝐷 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) )
215		oveq2	⊢ ( 𝑛 = ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) → ( 2 ↑ 𝑛 ) = ( 2 ↑ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) )
216	215	oveq2d	⊢ ( 𝑛 = ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) → ( 𝐸 / ( 2 ↑ 𝑛 ) ) = ( 𝐸 / ( 2 ↑ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) )
217	214 216	fveq12d	⊢ ( 𝑛 = ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) → ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) = ( ( 𝐷 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ ( 𝐸 / ( 2 ↑ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ) )
218	46 217	eleq12d	⊢ ( 𝑛 = ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) → ( ( 𝐼 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ↔ ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ ( 𝐸 / ( 2 ↑ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ) ) )
219	213 218	imbi12d	⊢ ( 𝑛 = ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) → ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐼 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ↔ ( ( 𝜑 ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℕ ) → ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ ( 𝐸 / ( 2 ↑ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ) ) ) )
220	43 219 9	vtocl	⊢ ( ( 𝜑 ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℕ ) → ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ ( 𝐸 / ( 2 ↑ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ) )
221	26 34 220	syl2anc	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ‘ ( 𝐸 / ( 2 ↑ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ) )
222	212 221	sseldd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ∈ ( 𝐶 ‘ ( 𝐴 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) )
223	184 222	sseldd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) )
224		elmapfn	⊢ ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) → ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) Fn ℕ )
225	223 224	syl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) Fn ℕ )
226		elmapi	⊢ ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) → ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) : ℕ ⟶ ( ( ℝ × ℝ ) ↑_m 𝑋 ) )
227	223 226	syl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) : ℕ ⟶ ( ( ℝ × ℝ ) ↑_m 𝑋 ) )
228	227	ffvelrnda	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑗 ) ∈ ( ( ℝ × ℝ ) ↑_m 𝑋 ) )
229	228	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ∀ 𝑗 ∈ ℕ ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑗 ) ∈ ( ( ℝ × ℝ ) ↑_m 𝑋 ) )
230	225 229	jca	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) Fn ℕ ∧ ∀ 𝑗 ∈ ℕ ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑗 ) ∈ ( ( ℝ × ℝ ) ↑_m 𝑋 ) ) )
231		ffnfv	⊢ ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) : ℕ ⟶ ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↔ ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) Fn ℕ ∧ ∀ 𝑗 ∈ ℕ ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑗 ) ∈ ( ( ℝ × ℝ ) ↑_m 𝑋 ) ) )
232	230 231	sylibr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) : ℕ ⟶ ( ( ℝ × ℝ ) ↑_m 𝑋 ) )
233	232 36	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) ∈ ( ( ℝ × ℝ ) ↑_m 𝑋 ) )
234	233 11	fmptd	⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ( ℝ × ℝ ) ↑_m 𝑋 ) )
235		simpl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝜑 )
236	9 86	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐼 ‘ 𝑛 ) ∈ { 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) } )
237	87 236	sselid	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐼 ‘ 𝑛 ) ∈ ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) )
238		simp3	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ ( 𝐼 ‘ 𝑛 ) ∈ ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) ) → ( 𝐼 ‘ 𝑛 ) ∈ ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) )
239	55	3adant3	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ ( 𝐼 ‘ 𝑛 ) ∈ ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) ) → ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) = { ℎ ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∣ ( 𝐴 ‘ 𝑛 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) } )
240	238 239	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ ( 𝐼 ‘ 𝑛 ) ∈ ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) ) → ( 𝐼 ‘ 𝑛 ) ∈ { ℎ ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∣ ( 𝐴 ‘ 𝑛 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) } )
241		fveq1	⊢ ( ℎ = ( 𝐼 ‘ 𝑛 ) → ( ℎ ‘ 𝑗 ) = ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) )
242	241	coeq2d	⊢ ( ℎ = ( 𝐼 ‘ 𝑛 ) → ( [,) ∘ ( ℎ ‘ 𝑗 ) ) = ( [,) ∘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) )
243	242	fveq1d	⊢ ( ℎ = ( 𝐼 ‘ 𝑛 ) → ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( [,) ∘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ‘ 𝑘 ) )
244	243	ixpeq2dv	⊢ ( ℎ = ( 𝐼 ‘ 𝑛 ) → X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) = X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ‘ 𝑘 ) )
245	244	iuneq2d	⊢ ( ℎ = ( 𝐼 ‘ 𝑛 ) → ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) = ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ‘ 𝑘 ) )
246	245	sseq2d	⊢ ( ℎ = ( 𝐼 ‘ 𝑛 ) → ( ( 𝐴 ‘ 𝑛 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) ↔ ( 𝐴 ‘ 𝑛 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
247	246	elrab	⊢ ( ( 𝐼 ‘ 𝑛 ) ∈ { ℎ ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∣ ( 𝐴 ‘ 𝑛 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) } ↔ ( ( 𝐼 ‘ 𝑛 ) ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ ( 𝐴 ‘ 𝑛 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
248	240 247	sylib	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ ( 𝐼 ‘ 𝑛 ) ∈ ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) ) → ( ( 𝐼 ‘ 𝑛 ) ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∧ ( 𝐴 ‘ 𝑛 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
249	248	simprd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ ( 𝐼 ‘ 𝑛 ) ∈ ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) ) → ( 𝐴 ‘ 𝑛 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ‘ 𝑘 ) )
250	235 13 237 249	syl3anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ‘ 𝑛 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ‘ 𝑘 ) )
251		f1ofo	⊢ ( 𝐹 : ℕ –1-1-onto→ ( ℕ × ℕ ) → 𝐹 : ℕ –onto→ ( ℕ × ℕ ) )
252	10 251	syl	⊢ ( 𝜑 → 𝐹 : ℕ –onto→ ( ℕ × ℕ ) )
253	252	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → 𝐹 : ℕ –onto→ ( ℕ × ℕ ) )
254		opelxpi	⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ⟨ 𝑛 , 𝑗 ⟩ ∈ ( ℕ × ℕ ) )
255	13 254	sylan	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → ⟨ 𝑛 , 𝑗 ⟩ ∈ ( ℕ × ℕ ) )
256		foelrni	⊢ ( ( 𝐹 : ℕ –onto→ ( ℕ × ℕ ) ∧ ⟨ 𝑛 , 𝑗 ⟩ ∈ ( ℕ × ℕ ) ) → ∃ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) = ⟨ 𝑛 , 𝑗 ⟩ )
257	253 255 256	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → ∃ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) = ⟨ 𝑛 , 𝑗 ⟩ )
258		nfv	⊢ Ⅎ 𝑚 ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ℕ )
259		nfre1	⊢ Ⅎ 𝑚 ∃ 𝑚 ∈ { 𝑖 ∈ ℕ ∣ ( 1^st ‘ ( 𝐹 ‘ 𝑖 ) ) = 𝑛 } X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ‘ 𝑘 ) ⊆ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐺 ‘ 𝑚 ) ) ‘ 𝑘 )
260		simpl	⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝐹 ‘ 𝑚 ) = ⟨ 𝑛 , 𝑗 ⟩ ) → 𝑚 ∈ ℕ )
261		fveq2	⊢ ( ( 𝐹 ‘ 𝑚 ) = ⟨ 𝑛 , 𝑗 ⟩ → ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) = ( 1^st ‘ ⟨ 𝑛 , 𝑗 ⟩ ) )
262		op1stg	⊢ ( ( 𝑛 ∈ V ∧ 𝑗 ∈ V ) → ( 1^st ‘ ⟨ 𝑛 , 𝑗 ⟩ ) = 𝑛 )
263	262	el2v	⊢ ( 1^st ‘ ⟨ 𝑛 , 𝑗 ⟩ ) = 𝑛
264	263	a1i	⊢ ( ( 𝐹 ‘ 𝑚 ) = ⟨ 𝑛 , 𝑗 ⟩ → ( 1^st ‘ ⟨ 𝑛 , 𝑗 ⟩ ) = 𝑛 )
265	261 264	eqtrd	⊢ ( ( 𝐹 ‘ 𝑚 ) = ⟨ 𝑛 , 𝑗 ⟩ → ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) = 𝑛 )
266	265	adantl	⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝐹 ‘ 𝑚 ) = ⟨ 𝑛 , 𝑗 ⟩ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) = 𝑛 )
267	260 266	jca	⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝐹 ‘ 𝑚 ) = ⟨ 𝑛 , 𝑗 ⟩ ) → ( 𝑚 ∈ ℕ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) = 𝑛 ) )
268		2fveq3	⊢ ( 𝑖 = 𝑚 → ( 1^st ‘ ( 𝐹 ‘ 𝑖 ) ) = ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) )
269	268	eqeq1d	⊢ ( 𝑖 = 𝑚 → ( ( 1^st ‘ ( 𝐹 ‘ 𝑖 ) ) = 𝑛 ↔ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) = 𝑛 ) )
270	269	elrab	⊢ ( 𝑚 ∈ { 𝑖 ∈ ℕ ∣ ( 1^st ‘ ( 𝐹 ‘ 𝑖 ) ) = 𝑛 } ↔ ( 𝑚 ∈ ℕ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) = 𝑛 ) )
271	267 270	sylibr	⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝐹 ‘ 𝑚 ) = ⟨ 𝑛 , 𝑗 ⟩ ) → 𝑚 ∈ { 𝑖 ∈ ℕ ∣ ( 1^st ‘ ( 𝐹 ‘ 𝑖 ) ) = 𝑛 } )
272	271	3adant1	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑚 ∈ ℕ ∧ ( 𝐹 ‘ 𝑚 ) = ⟨ 𝑛 , 𝑗 ⟩ ) → 𝑚 ∈ { 𝑖 ∈ ℕ ∣ ( 1^st ‘ ( 𝐹 ‘ 𝑖 ) ) = 𝑛 } )
273	260 113	syl	⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝐹 ‘ 𝑚 ) = ⟨ 𝑛 , 𝑗 ⟩ ) → ( 𝐺 ‘ 𝑚 ) = ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) )
274	265	fveq2d	⊢ ( ( 𝐹 ‘ 𝑚 ) = ⟨ 𝑛 , 𝑗 ⟩ → ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) = ( 𝐼 ‘ 𝑛 ) )
275		vex	⊢ 𝑛 ∈ V
276		vex	⊢ 𝑗 ∈ V
277	275 276	op2ndd	⊢ ( ( 𝐹 ‘ 𝑚 ) = ⟨ 𝑛 , 𝑗 ⟩ → ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) = 𝑗 )
278	274 277	fveq12d	⊢ ( ( 𝐹 ‘ 𝑚 ) = ⟨ 𝑛 , 𝑗 ⟩ → ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) = ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) )
279	278	adantl	⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝐹 ‘ 𝑚 ) = ⟨ 𝑛 , 𝑗 ⟩ ) → ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) = ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) )
280	273 279	eqtr2d	⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝐹 ‘ 𝑚 ) = ⟨ 𝑛 , 𝑗 ⟩ ) → ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) = ( 𝐺 ‘ 𝑚 ) )
281	280	coeq2d	⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝐹 ‘ 𝑚 ) = ⟨ 𝑛 , 𝑗 ⟩ ) → ( [,) ∘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) = ( [,) ∘ ( 𝐺 ‘ 𝑚 ) ) )
282	281	fveq1d	⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝐹 ‘ 𝑚 ) = ⟨ 𝑛 , 𝑗 ⟩ ) → ( ( [,) ∘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( [,) ∘ ( 𝐺 ‘ 𝑚 ) ) ‘ 𝑘 ) )
283	282	ixpeq2dv	⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝐹 ‘ 𝑚 ) = ⟨ 𝑛 , 𝑗 ⟩ ) → X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ‘ 𝑘 ) = X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐺 ‘ 𝑚 ) ) ‘ 𝑘 ) )
284		eqimss	⊢ ( X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ‘ 𝑘 ) = X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐺 ‘ 𝑚 ) ) ‘ 𝑘 ) → X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ‘ 𝑘 ) ⊆ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐺 ‘ 𝑚 ) ) ‘ 𝑘 ) )
285	283 284	syl	⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝐹 ‘ 𝑚 ) = ⟨ 𝑛 , 𝑗 ⟩ ) → X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ‘ 𝑘 ) ⊆ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐺 ‘ 𝑚 ) ) ‘ 𝑘 ) )
286	285	3adant1	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑚 ∈ ℕ ∧ ( 𝐹 ‘ 𝑚 ) = ⟨ 𝑛 , 𝑗 ⟩ ) → X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ‘ 𝑘 ) ⊆ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐺 ‘ 𝑚 ) ) ‘ 𝑘 ) )
287		rspe	⊢ ( ( 𝑚 ∈ { 𝑖 ∈ ℕ ∣ ( 1^st ‘ ( 𝐹 ‘ 𝑖 ) ) = 𝑛 } ∧ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ‘ 𝑘 ) ⊆ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐺 ‘ 𝑚 ) ) ‘ 𝑘 ) ) → ∃ 𝑚 ∈ { 𝑖 ∈ ℕ ∣ ( 1^st ‘ ( 𝐹 ‘ 𝑖 ) ) = 𝑛 } X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ‘ 𝑘 ) ⊆ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐺 ‘ 𝑚 ) ) ‘ 𝑘 ) )
288	272 286 287	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑚 ∈ ℕ ∧ ( 𝐹 ‘ 𝑚 ) = ⟨ 𝑛 , 𝑗 ⟩ ) → ∃ 𝑚 ∈ { 𝑖 ∈ ℕ ∣ ( 1^st ‘ ( 𝐹 ‘ 𝑖 ) ) = 𝑛 } X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ‘ 𝑘 ) ⊆ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐺 ‘ 𝑚 ) ) ‘ 𝑘 ) )
289	288	3exp	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → ( 𝑚 ∈ ℕ → ( ( 𝐹 ‘ 𝑚 ) = ⟨ 𝑛 , 𝑗 ⟩ → ∃ 𝑚 ∈ { 𝑖 ∈ ℕ ∣ ( 1^st ‘ ( 𝐹 ‘ 𝑖 ) ) = 𝑛 } X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ‘ 𝑘 ) ⊆ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐺 ‘ 𝑚 ) ) ‘ 𝑘 ) ) ) )
290	258 259 289	rexlimd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → ( ∃ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) = ⟨ 𝑛 , 𝑗 ⟩ → ∃ 𝑚 ∈ { 𝑖 ∈ ℕ ∣ ( 1^st ‘ ( 𝐹 ‘ 𝑖 ) ) = 𝑛 } X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ‘ 𝑘 ) ⊆ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐺 ‘ 𝑚 ) ) ‘ 𝑘 ) ) )
291	257 290	mpd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → ∃ 𝑚 ∈ { 𝑖 ∈ ℕ ∣ ( 1^st ‘ ( 𝐹 ‘ 𝑖 ) ) = 𝑛 } X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ‘ 𝑘 ) ⊆ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐺 ‘ 𝑚 ) ) ‘ 𝑘 ) )
292	291	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∀ 𝑗 ∈ ℕ ∃ 𝑚 ∈ { 𝑖 ∈ ℕ ∣ ( 1^st ‘ ( 𝐹 ‘ 𝑖 ) ) = 𝑛 } X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ‘ 𝑘 ) ⊆ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐺 ‘ 𝑚 ) ) ‘ 𝑘 ) )
293		iunss2	⊢ ( ∀ 𝑗 ∈ ℕ ∃ 𝑚 ∈ { 𝑖 ∈ ℕ ∣ ( 1^st ‘ ( 𝐹 ‘ 𝑖 ) ) = 𝑛 } X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ‘ 𝑘 ) ⊆ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐺 ‘ 𝑚 ) ) ‘ 𝑘 ) → ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ‘ 𝑘 ) ⊆ ∪ 𝑚 ∈ { 𝑖 ∈ ℕ ∣ ( 1^st ‘ ( 𝐹 ‘ 𝑖 ) ) = 𝑛 } X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐺 ‘ 𝑚 ) ) ‘ 𝑘 ) )
294	292 293	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ‘ 𝑘 ) ⊆ ∪ 𝑚 ∈ { 𝑖 ∈ ℕ ∣ ( 1^st ‘ ( 𝐹 ‘ 𝑖 ) ) = 𝑛 } X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐺 ‘ 𝑚 ) ) ‘ 𝑘 ) )
295	250 294	sstrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ‘ 𝑛 ) ⊆ ∪ 𝑚 ∈ { 𝑖 ∈ ℕ ∣ ( 1^st ‘ ( 𝐹 ‘ 𝑖 ) ) = 𝑛 } X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐺 ‘ 𝑚 ) ) ‘ 𝑘 ) )
296		ssrab2	⊢ { 𝑖 ∈ ℕ ∣ ( 1^st ‘ ( 𝐹 ‘ 𝑖 ) ) = 𝑛 } ⊆ ℕ
297		iunss1	⊢ ( { 𝑖 ∈ ℕ ∣ ( 1^st ‘ ( 𝐹 ‘ 𝑖 ) ) = 𝑛 } ⊆ ℕ → ∪ 𝑚 ∈ { 𝑖 ∈ ℕ ∣ ( 1^st ‘ ( 𝐹 ‘ 𝑖 ) ) = 𝑛 } X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐺 ‘ 𝑚 ) ) ‘ 𝑘 ) ⊆ ∪ 𝑚 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐺 ‘ 𝑚 ) ) ‘ 𝑘 ) )
298	296 297	ax-mp	⊢ ∪ 𝑚 ∈ { 𝑖 ∈ ℕ ∣ ( 1^st ‘ ( 𝐹 ‘ 𝑖 ) ) = 𝑛 } X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐺 ‘ 𝑚 ) ) ‘ 𝑘 ) ⊆ ∪ 𝑚 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐺 ‘ 𝑚 ) ) ‘ 𝑘 )
299	298	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∪ 𝑚 ∈ { 𝑖 ∈ ℕ ∣ ( 1^st ‘ ( 𝐹 ‘ 𝑖 ) ) = 𝑛 } X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐺 ‘ 𝑚 ) ) ‘ 𝑘 ) ⊆ ∪ 𝑚 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐺 ‘ 𝑚 ) ) ‘ 𝑘 ) )
300	295 299	sstrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ‘ 𝑛 ) ⊆ ∪ 𝑚 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐺 ‘ 𝑚 ) ) ‘ 𝑘 ) )
301	300	ralrimiva	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ⊆ ∪ 𝑚 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐺 ‘ 𝑚 ) ) ‘ 𝑘 ) )
302		iunss	⊢ ( ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ⊆ ∪ 𝑚 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐺 ‘ 𝑚 ) ) ‘ 𝑘 ) ↔ ∀ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ⊆ ∪ 𝑚 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐺 ‘ 𝑚 ) ) ‘ 𝑘 ) )
303	301 302	sylibr	⊢ ( 𝜑 → ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ⊆ ∪ 𝑚 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐺 ‘ 𝑚 ) ) ‘ 𝑘 ) )
304	1 2 7 234 303	ovnlecvr	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ≤ ( Σ^{^} ‘ ( 𝑚 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) )
305	114	fveq2d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐿 ‘ ( 𝐺 ‘ 𝑚 ) ) = ( 𝐿 ‘ ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) )
306	305	mpteq2dva	⊢ ( 𝜑 → ( 𝑚 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐺 ‘ 𝑚 ) ) ) = ( 𝑚 ∈ ℕ ↦ ( 𝐿 ‘ ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ) )
307	306	fveq2d	⊢ ( 𝜑 → ( Σ^{^} ‘ ( 𝑚 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) = ( Σ^{^} ‘ ( 𝑚 ∈ ℕ ↦ ( 𝐿 ‘ ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ) ) )
308		nfv	⊢ Ⅎ 𝑝 𝜑
309		2fveq3	⊢ ( 𝑝 = ( 𝐹 ‘ 𝑚 ) → ( 𝐼 ‘ ( 1^st ‘ 𝑝 ) ) = ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) )
310		fveq2	⊢ ( 𝑝 = ( 𝐹 ‘ 𝑚 ) → ( 2^nd ‘ 𝑝 ) = ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) )
311	309 310	fveq12d	⊢ ( 𝑝 = ( 𝐹 ‘ 𝑚 ) → ( ( 𝐼 ‘ ( 1^st ‘ 𝑝 ) ) ‘ ( 2^nd ‘ 𝑝 ) ) = ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) )
312	311	fveq2d	⊢ ( 𝑝 = ( 𝐹 ‘ 𝑚 ) → ( 𝐿 ‘ ( ( 𝐼 ‘ ( 1^st ‘ 𝑝 ) ) ‘ ( 2^nd ‘ 𝑝 ) ) ) = ( 𝐿 ‘ ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) )
313		eqidd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑚 ) )
314		nfv	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑝 ∈ ( ℕ × ℕ ) )
315	1	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ℕ × ℕ ) ) → 𝑋 ∈ Fin )
316		simpl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ℕ × ℕ ) ) → 𝜑 )
317		xp1st	⊢ ( 𝑝 ∈ ( ℕ × ℕ ) → ( 1^st ‘ 𝑝 ) ∈ ℕ )
318	317	adantl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ℕ × ℕ ) ) → ( 1^st ‘ 𝑝 ) ∈ ℕ )
319		xp2nd	⊢ ( 𝑝 ∈ ( ℕ × ℕ ) → ( 2^nd ‘ 𝑝 ) ∈ ℕ )
320	319	adantl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ℕ × ℕ ) ) → ( 2^nd ‘ 𝑝 ) ∈ ℕ )
321		fvex	⊢ ( 2^nd ‘ 𝑝 ) ∈ V
322		eleq1	⊢ ( 𝑗 = ( 2^nd ‘ 𝑝 ) → ( 𝑗 ∈ ℕ ↔ ( 2^nd ‘ 𝑝 ) ∈ ℕ ) )
323	322	3anbi3d	⊢ ( 𝑗 = ( 2^nd ‘ 𝑝 ) → ( ( 𝜑 ∧ ( 1^st ‘ 𝑝 ) ∈ ℕ ∧ 𝑗 ∈ ℕ ) ↔ ( 𝜑 ∧ ( 1^st ‘ 𝑝 ) ∈ ℕ ∧ ( 2^nd ‘ 𝑝 ) ∈ ℕ ) ) )
324		fveq2	⊢ ( 𝑗 = ( 2^nd ‘ 𝑝 ) → ( ( 𝐼 ‘ ( 1^st ‘ 𝑝 ) ) ‘ 𝑗 ) = ( ( 𝐼 ‘ ( 1^st ‘ 𝑝 ) ) ‘ ( 2^nd ‘ 𝑝 ) ) )
325	324	feq1d	⊢ ( 𝑗 = ( 2^nd ‘ 𝑝 ) → ( ( ( 𝐼 ‘ ( 1^st ‘ 𝑝 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) ↔ ( ( 𝐼 ‘ ( 1^st ‘ 𝑝 ) ) ‘ ( 2^nd ‘ 𝑝 ) ) : 𝑋 ⟶ ( ℝ × ℝ ) ) )
326	323 325	imbi12d	⊢ ( 𝑗 = ( 2^nd ‘ 𝑝 ) → ( ( ( 𝜑 ∧ ( 1^st ‘ 𝑝 ) ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( ( 𝐼 ‘ ( 1^st ‘ 𝑝 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) ) ↔ ( ( 𝜑 ∧ ( 1^st ‘ 𝑝 ) ∈ ℕ ∧ ( 2^nd ‘ 𝑝 ) ∈ ℕ ) → ( ( 𝐼 ‘ ( 1^st ‘ 𝑝 ) ) ‘ ( 2^nd ‘ 𝑝 ) ) : 𝑋 ⟶ ( ℝ × ℝ ) ) ) )
327		fvex	⊢ ( 1^st ‘ 𝑝 ) ∈ V
328		eleq1	⊢ ( 𝑛 = ( 1^st ‘ 𝑝 ) → ( 𝑛 ∈ ℕ ↔ ( 1^st ‘ 𝑝 ) ∈ ℕ ) )
329	328	3anbi2d	⊢ ( 𝑛 = ( 1^st ‘ 𝑝 ) → ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ↔ ( 𝜑 ∧ ( 1^st ‘ 𝑝 ) ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) )
330		fveq2	⊢ ( 𝑛 = ( 1^st ‘ 𝑝 ) → ( 𝐼 ‘ 𝑛 ) = ( 𝐼 ‘ ( 1^st ‘ 𝑝 ) ) )
331	330	fveq1d	⊢ ( 𝑛 = ( 1^st ‘ 𝑝 ) → ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) = ( ( 𝐼 ‘ ( 1^st ‘ 𝑝 ) ) ‘ 𝑗 ) )
332	331	feq1d	⊢ ( 𝑛 = ( 1^st ‘ 𝑝 ) → ( ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) ↔ ( ( 𝐼 ‘ ( 1^st ‘ 𝑝 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) ) )
333	329 332	imbi12d	⊢ ( 𝑛 = ( 1^st ‘ 𝑝 ) → ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) ) ↔ ( ( 𝜑 ∧ ( 1^st ‘ 𝑝 ) ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( ( 𝐼 ‘ ( 1^st ‘ 𝑝 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) ) ) )
334	327 333 105	vtocl	⊢ ( ( 𝜑 ∧ ( 1^st ‘ 𝑝 ) ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( ( 𝐼 ‘ ( 1^st ‘ 𝑝 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
335	321 326 334	vtocl	⊢ ( ( 𝜑 ∧ ( 1^st ‘ 𝑝 ) ∈ ℕ ∧ ( 2^nd ‘ 𝑝 ) ∈ ℕ ) → ( ( 𝐼 ‘ ( 1^st ‘ 𝑝 ) ) ‘ ( 2^nd ‘ 𝑝 ) ) : 𝑋 ⟶ ( ℝ × ℝ ) )
336	316 318 320 335	syl3anc	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ℕ × ℕ ) ) → ( ( 𝐼 ‘ ( 1^st ‘ 𝑝 ) ) ‘ ( 2^nd ‘ 𝑝 ) ) : 𝑋 ⟶ ( ℝ × ℝ ) )
337	314 315 7 336	hoiprodcl2	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ℕ × ℕ ) ) → ( 𝐿 ‘ ( ( 𝐼 ‘ ( 1^st ‘ 𝑝 ) ) ‘ ( 2^nd ‘ 𝑝 ) ) ) ∈ ( 0 [,) +∞ ) )
338	24 337	sselid	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ℕ × ℕ ) ) → ( 𝐿 ‘ ( ( 𝐼 ‘ ( 1^st ‘ 𝑝 ) ) ‘ ( 2^nd ‘ 𝑝 ) ) ) ∈ ( 0 [,] +∞ ) )
339	308 21 312 23 10 313 338	sge0f1o	⊢ ( 𝜑 → ( Σ^{^} ‘ ( 𝑝 ∈ ( ℕ × ℕ ) ↦ ( 𝐿 ‘ ( ( 𝐼 ‘ ( 1^st ‘ 𝑝 ) ) ‘ ( 2^nd ‘ 𝑝 ) ) ) ) ) = ( Σ^{^} ‘ ( 𝑚 ∈ ℕ ↦ ( 𝐿 ‘ ( ( 𝐼 ‘ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ‘ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) ) ) )
340	307 339	eqtr4d	⊢ ( 𝜑 → ( Σ^{^} ‘ ( 𝑚 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) = ( Σ^{^} ‘ ( 𝑝 ∈ ( ℕ × ℕ ) ↦ ( 𝐿 ‘ ( ( 𝐼 ‘ ( 1^st ‘ 𝑝 ) ) ‘ ( 2^nd ‘ 𝑝 ) ) ) ) ) )
341		nfv	⊢ Ⅎ 𝑗 𝜑
342	275 276	op1std	⊢ ( 𝑝 = ⟨ 𝑛 , 𝑗 ⟩ → ( 1^st ‘ 𝑝 ) = 𝑛 )
343	342	fveq2d	⊢ ( 𝑝 = ⟨ 𝑛 , 𝑗 ⟩ → ( 𝐼 ‘ ( 1^st ‘ 𝑝 ) ) = ( 𝐼 ‘ 𝑛 ) )
344	275 276	op2ndd	⊢ ( 𝑝 = ⟨ 𝑛 , 𝑗 ⟩ → ( 2^nd ‘ 𝑝 ) = 𝑗 )
345	343 344	fveq12d	⊢ ( 𝑝 = ⟨ 𝑛 , 𝑗 ⟩ → ( ( 𝐼 ‘ ( 1^st ‘ 𝑝 ) ) ‘ ( 2^nd ‘ 𝑝 ) ) = ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) )
346	345	fveq2d	⊢ ( 𝑝 = ⟨ 𝑛 , 𝑗 ⟩ → ( 𝐿 ‘ ( ( 𝐼 ‘ ( 1^st ‘ 𝑝 ) ) ‘ ( 2^nd ‘ 𝑝 ) ) ) = ( 𝐿 ‘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) )
347		nfv	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ℕ )
348	125	adantr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → 𝑋 ∈ Fin )
349	96 104	syl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
350	347 348 7 349	hoiprodcl2	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐿 ‘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ∈ ( 0 [,) +∞ ) )
351	24 350	sselid	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐿 ‘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ∈ ( 0 [,] +∞ ) )
352	351	3impa	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( 𝐿 ‘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ∈ ( 0 [,] +∞ ) )
353	341 346 23 23 352	sge0xp	⊢ ( 𝜑 → ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ) ) ) ) = ( Σ^{^} ‘ ( 𝑝 ∈ ( ℕ × ℕ ) ↦ ( 𝐿 ‘ ( ( 𝐼 ‘ ( 1^st ‘ 𝑝 ) ) ‘ ( 2^nd ‘ 𝑝 ) ) ) ) ) )
354	353	eqcomd	⊢ ( 𝜑 → ( Σ^{^} ‘ ( 𝑝 ∈ ( ℕ × ℕ ) ↦ ( 𝐿 ‘ ( ( 𝐼 ‘ ( 1^st ‘ 𝑝 ) ) ‘ ( 2^nd ‘ 𝑝 ) ) ) ) ) = ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ) ) ) ) )
355	22	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ℕ ∈ V )
356		eqid	⊢ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) )
357	351 356	fmptd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ) : ℕ ⟶ ( 0 [,] +∞ ) )
358	355 357	sge0cl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ) ) ∈ ( 0 [,] +∞ ) )
359		fveq1	⊢ ( 𝑖 = ( 𝐼 ‘ 𝑛 ) → ( 𝑖 ‘ 𝑗 ) = ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) )
360	359	fveq2d	⊢ ( 𝑖 = ( 𝐼 ‘ 𝑛 ) → ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) = ( 𝐿 ‘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) )
361	360	mpteq2dv	⊢ ( 𝑖 = ( 𝐼 ‘ 𝑛 ) → ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ) )
362	361	fveq2d	⊢ ( 𝑖 = ( 𝐼 ‘ 𝑛 ) → ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ) ) )
363	362	breq1d	⊢ ( 𝑖 = ( 𝐼 ‘ 𝑛 ) → ( ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ↔ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) )
364	363	elrab	⊢ ( ( 𝐼 ‘ 𝑛 ) ∈ { 𝑖 ∈ ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) } ↔ ( ( 𝐼 ‘ 𝑛 ) ∈ ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) ∧ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) )
365	236 364	sylib	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐼 ‘ 𝑛 ) ∈ ( 𝐶 ‘ ( 𝐴 ‘ 𝑛 ) ) ∧ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) )
366	365	simprd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) )
367	120 23 358 173 366	sge0lempt	⊢ ( 𝜑 → ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( ( 𝐼 ‘ 𝑛 ) ‘ 𝑗 ) ) ) ) ) ) ≤ ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) )
368	354 367	eqbrtrd	⊢ ( 𝜑 → ( Σ^{^} ‘ ( 𝑝 ∈ ( ℕ × ℕ ) ↦ ( 𝐿 ‘ ( ( 𝐼 ‘ ( 1^st ‘ 𝑝 ) ) ‘ ( 2^nd ‘ 𝑝 ) ) ) ) ) ≤ ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) )
369	340 368	eqbrtrd	⊢ ( 𝜑 → ( Σ^{^} ‘ ( 𝑚 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ≤ ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) )
370	20 119 174 304 369	xrletrd	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ≤ ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) )
371	120 23 160 168	sge0xadd	⊢ ( 𝜑 → ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) = ( ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) +_𝑒 ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) )
372	121	a1i	⊢ ( 𝜑 → 0 ∈ ℝ^* )
373	123	a1i	⊢ ( 𝜑 → +∞ ∈ ℝ^* )
374	145	rexrd	⊢ ( 𝜑 → 𝐸 ∈ ℝ^* )
375	4	rpge0d	⊢ ( 𝜑 → 0 ≤ 𝐸 )
376	145	ltpnfd	⊢ ( 𝜑 → 𝐸 < +∞ )
377	372 373 374 375 376	elicod	⊢ ( 𝜑 → 𝐸 ∈ ( 0 [,) +∞ ) )
378	377	sge0ad2en	⊢ ( 𝜑 → ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) = 𝐸 )
379	378	oveq2d	⊢ ( 𝜑 → ( ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) +_𝑒 ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) = ( ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) +_𝑒 𝐸 ) )
380	371 379	eqtrd	⊢ ( 𝜑 → ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) +_𝑒 ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) = ( ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) +_𝑒 𝐸 ) )
381	370 380	breqtrd	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ≤ ( ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) +_𝑒 𝐸 ) )

Metamath Proof Explorer

Theorem ovnsubaddlem1

Proof