Theorem ovncvrrp

Description: The Lebesgue outer measure of a subset of multidimensional real numbers can always be approximated by the total outer measure of a cover of half-open (multidimensional) intervals. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	ovncvrrp.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	ovncvrrp.n0	⊢ ( 𝜑 → 𝑋 ≠ ∅ )
	ovncvrrp.a	⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
	ovncvrrp.e	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
	ovncvrrp.c	⊢ 𝐶 = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } )
	ovncvrrp.l	⊢ 𝐿 = ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) )
	ovncvrrp.d	⊢ 𝐷 = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ ( 𝑒 ∈ ℝ+ ↦ { 𝑖 ∈ ( 𝐶 ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +e 𝑒 ) } ) )
Assertion	ovncvrrp	⊢ ( 𝜑 → ∃ 𝑖 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		ovncvrrp.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		ovncvrrp.n0	⊢ ( 𝜑 → 𝑋 ≠ ∅ )
3		ovncvrrp.a	⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
4		ovncvrrp.e	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
5		ovncvrrp.c	⊢ 𝐶 = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } )
6		ovncvrrp.l	⊢ 𝐿 = ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) )
7		ovncvrrp.d	⊢ 𝐷 = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ ( 𝑒 ∈ ℝ+ ↦ { 𝑖 ∈ ( 𝐶 ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +e 𝑒 ) } ) )
8		eqid	⊢ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } = { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) }
9	1 2 3 4 8	ovnlerp	⊢ ( 𝜑 → ∃ 𝑧 ∈ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } 𝑧 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) )
10		simp1	⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ∧ 𝑧 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) → 𝜑 )
11		simp3	⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ∧ 𝑧 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) → 𝑧 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) )
12		rabid	⊢ ( 𝑧 ∈ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ↔ ( 𝑧 ∈ ℝ* ∧ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
13	12	biimpi	⊢ ( 𝑧 ∈ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } → ( 𝑧 ∈ ℝ* ∧ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
14	13	simprd	⊢ ( 𝑧 ∈ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } → ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
15	14	adantr	⊢ ( ( 𝑧 ∈ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ∧ 𝑧 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) → ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
16	15	3adant1	⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ∧ 𝑧 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) → ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
17		nfv	⊢ Ⅎ 𝑖 ( 𝜑 ∧ 𝑧 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) )
18		nfe1	⊢ Ⅎ 𝑖 ∃ 𝑖 ( 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) )
19		simp1l	⊢ ( ( ( 𝜑 ∧ 𝑧 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → 𝜑 )
20		simp2	⊢ ( ( ( 𝜑 ∧ 𝑧 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) )
21		simp3l	⊢ ( ( ( 𝜑 ∧ 𝑧 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) )
22		id	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) → ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
23		fveq1	⊢ ( 𝑙 = 𝑖 → ( 𝑙 ‘ 𝑗 ) = ( 𝑖 ‘ 𝑗 ) )
24	23	coeq2d	⊢ ( 𝑙 = 𝑖 → ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) = ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) )
25	24	fveq1d	⊢ ( 𝑙 = 𝑖 → ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) )
26	25	ixpeq2dv	⊢ ( 𝑙 = 𝑖 → X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) = X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) )
27	26	iuneq2d	⊢ ( 𝑙 = 𝑖 → ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) = ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) )
28	27	sseq2d	⊢ ( 𝑙 = 𝑖 → ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) ↔ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
29	28	elrab	⊢ ( 𝑖 ∈ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } ↔ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
30	22 29	sylibr	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) → 𝑖 ∈ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } )
31	30	3adant1	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) → 𝑖 ∈ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } )
32		sseq1	⊢ ( 𝑎 = 𝐴 → ( 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) ↔ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
33	32	rabbidv	⊢ ( 𝑎 = 𝐴 → { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } = { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } )
34		ovexd	⊢ ( 𝜑 → ( ℝ ↑m 𝑋 ) ∈ V )
35	34 3	ssexd	⊢ ( 𝜑 → 𝐴 ∈ V )
36		elpwg	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↔ 𝐴 ⊆ ( ℝ ↑m 𝑋 ) ) )
37	35 36	syl	⊢ ( 𝜑 → ( 𝐴 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↔ 𝐴 ⊆ ( ℝ ↑m 𝑋 ) ) )
38	3 37	mpbird	⊢ ( 𝜑 → 𝐴 ∈ 𝒫 ( ℝ ↑m 𝑋 ) )
39		ovex	⊢ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∈ V
40	39	rabex	⊢ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } ∈ V
41	40	a1i	⊢ ( 𝜑 → { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } ∈ V )
42	5 33 38 41	fvmptd3	⊢ ( 𝜑 → ( 𝐶 ‘ 𝐴 ) = { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } )
43	42	eqcomd	⊢ ( 𝜑 → { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } = ( 𝐶 ‘ 𝐴 ) )
44	43	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) → { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } = ( 𝐶 ‘ 𝐴 ) )
45	31 44	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) → 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) )
46	19 20 21 45	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) )
47		coeq2	⊢ ( ℎ = ( 𝑖 ‘ 𝑗 ) → ( [,) ∘ ℎ ) = ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) )
48	47	fveq1d	⊢ ( ℎ = ( 𝑖 ‘ 𝑗 ) → ( ( [,) ∘ ℎ ) ‘ 𝑘 ) = ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) )
49	48	fveq2d	⊢ ( ℎ = ( 𝑖 ‘ 𝑗 ) → ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
50	49	prodeq2ad	⊢ ( ℎ = ( 𝑖 ‘ 𝑗 ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
51		elmapi	⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → 𝑖 : ℕ ⟶ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
52	51	adantr	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑗 ∈ ℕ ) → 𝑖 : ℕ ⟶ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
53		simpr	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ )
54	52 53	ffvelcdmd	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑗 ∈ ℕ ) → ( 𝑖 ‘ 𝑗 ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
55		prodex	⊢ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ∈ V
56	55	a1i	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑗 ∈ ℕ ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ∈ V )
57	6 50 54 56	fvmptd3	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
58	57	mpteq2dva	⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) = ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) )
59	58	fveq2d	⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
60	59	adantr	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
61		id	⊢ ( 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) → 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
62	61	eqcomd	⊢ ( 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) = 𝑧 )
63	62	adantl	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) = 𝑧 )
64	60 63	eqtrd	⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) = 𝑧 )
65	64	3adant1	⊢ ( ( 𝑧 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) = 𝑧 )
66		simp1	⊢ ( ( 𝑧 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → 𝑧 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) )
67	65 66	eqbrtrd	⊢ ( ( 𝑧 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) )
68	67	3adant1l	⊢ ( ( ( 𝜑 ∧ 𝑧 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) )
69	68	3adant3l	⊢ ( ( ( 𝜑 ∧ 𝑧 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) )
70	46 69	jca	⊢ ( ( ( 𝜑 ∧ 𝑧 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → ( 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) )
71	70	19.8ad	⊢ ( ( ( 𝜑 ∧ 𝑧 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → ∃ 𝑖 ( 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) )
72	71	3exp	⊢ ( ( 𝜑 ∧ 𝑧 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) → ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → ∃ 𝑖 ( 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) ) ) )
73	17 18 72	rexlimd	⊢ ( ( 𝜑 ∧ 𝑧 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) → ( ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → ∃ 𝑖 ( 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) ) )
74	73	imp	⊢ ( ( ( 𝜑 ∧ 𝑧 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) ∧ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → ∃ 𝑖 ( 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) )
75	10 11 16 74	syl21anc	⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ∧ 𝑧 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) → ∃ 𝑖 ( 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) )
76	75	3exp	⊢ ( 𝜑 → ( 𝑧 ∈ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } → ( 𝑧 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) → ∃ 𝑖 ( 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) ) ) )
77	76	rexlimdv	⊢ ( 𝜑 → ( ∃ 𝑧 ∈ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } 𝑧 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) → ∃ 𝑖 ( 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) ) )
78	9 77	mpd	⊢ ( 𝜑 → ∃ 𝑖 ( 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) )
79		rabid	⊢ ( 𝑖 ∈ { 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) } ↔ ( 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) )
80	79	bilanri	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) ) → 𝑖 ∈ { 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) } )
81		nfcv	⊢ Ⅎ 𝑏 ( 𝑒 ∈ ℝ+ ↦ { 𝑖 ∈ ( 𝐶 ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +e 𝑒 ) } )
82		nfcv	⊢ Ⅎ 𝑎 ℝ+
83		nfv	⊢ Ⅎ 𝑎 ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +e 𝑒 )
84		nfmpt1	⊢ Ⅎ 𝑎 ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } )
85	5 84	nfcxfr	⊢ Ⅎ 𝑎 𝐶
86		nfcv	⊢ Ⅎ 𝑎 𝑏
87	85 86	nffv	⊢ Ⅎ 𝑎 ( 𝐶 ‘ 𝑏 )
88	83 87	nfrabw	⊢ Ⅎ 𝑎 { 𝑖 ∈ ( 𝐶 ‘ 𝑏 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +e 𝑒 ) }
89	82 88	nfmpt	⊢ Ⅎ 𝑎 ( 𝑒 ∈ ℝ+ ↦ { 𝑖 ∈ ( 𝐶 ‘ 𝑏 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +e 𝑒 ) } )
90		fveq2	⊢ ( 𝑎 = 𝑏 → ( 𝐶 ‘ 𝑎 ) = ( 𝐶 ‘ 𝑏 ) )
91	90	eleq2d	⊢ ( 𝑎 = 𝑏 → ( 𝑖 ∈ ( 𝐶 ‘ 𝑎 ) ↔ 𝑖 ∈ ( 𝐶 ‘ 𝑏 ) ) )
92		fveq2	⊢ ( 𝑎 = 𝑏 → ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) = ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) )
93	92	oveq1d	⊢ ( 𝑎 = 𝑏 → ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +e 𝑒 ) = ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +e 𝑒 ) )
94	93	breq2d	⊢ ( 𝑎 = 𝑏 → ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +e 𝑒 ) ↔ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +e 𝑒 ) ) )
95	91 94	anbi12d	⊢ ( 𝑎 = 𝑏 → ( ( 𝑖 ∈ ( 𝐶 ‘ 𝑎 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +e 𝑒 ) ) ↔ ( 𝑖 ∈ ( 𝐶 ‘ 𝑏 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +e 𝑒 ) ) ) )
96	95	rabbidva2	⊢ ( 𝑎 = 𝑏 → { 𝑖 ∈ ( 𝐶 ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +e 𝑒 ) } = { 𝑖 ∈ ( 𝐶 ‘ 𝑏 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +e 𝑒 ) } )
97	96	mpteq2dv	⊢ ( 𝑎 = 𝑏 → ( 𝑒 ∈ ℝ+ ↦ { 𝑖 ∈ ( 𝐶 ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +e 𝑒 ) } ) = ( 𝑒 ∈ ℝ+ ↦ { 𝑖 ∈ ( 𝐶 ‘ 𝑏 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +e 𝑒 ) } ) )
98	81 89 97	cbvmpt	⊢ ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ ( 𝑒 ∈ ℝ+ ↦ { 𝑖 ∈ ( 𝐶 ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +e 𝑒 ) } ) ) = ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ ( 𝑒 ∈ ℝ+ ↦ { 𝑖 ∈ ( 𝐶 ‘ 𝑏 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +e 𝑒 ) } ) )
99	7 98	eqtri	⊢ 𝐷 = ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ ( 𝑒 ∈ ℝ+ ↦ { 𝑖 ∈ ( 𝐶 ‘ 𝑏 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +e 𝑒 ) } ) )
100		fveq2	⊢ ( 𝑏 = 𝐴 → ( 𝐶 ‘ 𝑏 ) = ( 𝐶 ‘ 𝐴 ) )
101	100	eleq2d	⊢ ( 𝑏 = 𝐴 → ( 𝑖 ∈ ( 𝐶 ‘ 𝑏 ) ↔ 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ) )
102		fveq2	⊢ ( 𝑏 = 𝐴 → ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) = ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) )
103	102	oveq1d	⊢ ( 𝑏 = 𝐴 → ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +e 𝑒 ) = ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝑒 ) )
104	103	breq2d	⊢ ( 𝑏 = 𝐴 → ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +e 𝑒 ) ↔ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝑒 ) ) )
105	101 104	anbi12d	⊢ ( 𝑏 = 𝐴 → ( ( 𝑖 ∈ ( 𝐶 ‘ 𝑏 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +e 𝑒 ) ) ↔ ( 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝑒 ) ) ) )
106	105	rabbidva2	⊢ ( 𝑏 = 𝐴 → { 𝑖 ∈ ( 𝐶 ‘ 𝑏 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +e 𝑒 ) } = { 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝑒 ) } )
107	106	mpteq2dv	⊢ ( 𝑏 = 𝐴 → ( 𝑒 ∈ ℝ+ ↦ { 𝑖 ∈ ( 𝐶 ‘ 𝑏 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +e 𝑒 ) } ) = ( 𝑒 ∈ ℝ+ ↦ { 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝑒 ) } ) )
108	38	adantr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) ) → 𝐴 ∈ 𝒫 ( ℝ ↑m 𝑋 ) )
109		rpex	⊢ ℝ+ ∈ V
110	109	mptex	⊢ ( 𝑒 ∈ ℝ+ ↦ { 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝑒 ) } ) ∈ V
111	110	a1i	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) ) → ( 𝑒 ∈ ℝ+ ↦ { 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝑒 ) } ) ∈ V )
112	99 107 108 111	fvmptd3	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) ) → ( 𝐷 ‘ 𝐴 ) = ( 𝑒 ∈ ℝ+ ↦ { 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝑒 ) } ) )
113		oveq2	⊢ ( 𝑒 = 𝐸 → ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝑒 ) = ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) )
114	113	breq2d	⊢ ( 𝑒 = 𝐸 → ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝑒 ) ↔ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) )
115	114	rabbidv	⊢ ( 𝑒 = 𝐸 → { 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝑒 ) } = { 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) } )
116	115	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) ) ∧ 𝑒 = 𝐸 ) → { 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝑒 ) } = { 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) } )
117	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) ) → 𝐸 ∈ ℝ+ )
118		fvex	⊢ ( 𝐶 ‘ 𝐴 ) ∈ V
119	118	rabex	⊢ { 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) } ∈ V
120	119	a1i	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) ) → { 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) } ∈ V )
121	112 116 117 120	fvmptd	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) ) → ( ( 𝐷 ‘ 𝐴 ) ‘ 𝐸 ) = { 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) } )
122	121	eqcomd	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) ) → { 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) } = ( ( 𝐷 ‘ 𝐴 ) ‘ 𝐸 ) )
123	80 122	eleqtrd	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) ) → 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝐸 ) )
124	123	ex	⊢ ( 𝜑 → ( ( 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) → 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝐸 ) ) )
125	124	eximdv	⊢ ( 𝜑 → ( ∃ 𝑖 ( 𝑖 ∈ ( 𝐶 ‘ 𝐴 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) → ∃ 𝑖 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝐸 ) ) )
126	78 125	mpd	⊢ ( 𝜑 → ∃ 𝑖 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝐸 ) )