Metamath Proof Explorer

Theorem ovnsubaddlem2

Description: ( voln*X ) is subadditive. Proposition 115D (a)(iv) of Fremlin1 p. 31 . (Contributed by Glauco Siliprandi, 11-Oct-2020)

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

Proof

Step Hyp Ref Expression
1 ovnsubaddlem2.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
2 ovnsubaddlem2.n0 ⊢ ( 𝜑 → 𝑋 ≠ ∅ )
3 ovnsubaddlem2.a ⊢ ( 𝜑 → 𝐴 : ℕ ⟶ 𝒫 ( ℝ ↑m 𝑋 ) )
4 ovnsubaddlem2.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
5 ovnsubaddlem2.z ⊢ 𝑍 = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } )
6 ovnsubaddlem2.c ⊢ 𝐶 = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } )
7 ovnsubaddlem2.l ⊢ 𝐿 = ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) )
8 ovnsubaddlem2.d ⊢ 𝐷 = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ ( 𝑒 ∈ ℝ+ ↦ { 𝑖 ∈ ( 𝐶 ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +e 𝑒 ) } ) )
9 fvex ⊢ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ∈ V
10 nnenom ⊢ ℕ ≈ ω
11 9 10 axcc3 ⊢ ∃ 𝑔 ( 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) )
12 simprl ⊢ ( ( 𝜑 ∧ ( 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) ) → 𝑔 Fn ℕ )
13 nfv ⊢ Ⅎ 𝑛 𝜑
14 nfra1 ⊢ Ⅎ 𝑛 ∀ 𝑛 ∈ ℕ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) )
15 13 14 nfan ⊢ Ⅎ 𝑛 ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) )
16 rspa ⊢ ( ( ∀ 𝑛 ∈ ℕ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) )
17 16 adantll ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) )
18 1 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑋 ∈ Fin )
19 2 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑋 ≠ ∅ )
20 3 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 : ℕ ⟶ 𝒫 ( ℝ ↑m 𝑋 ) )
21 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
22 20 21 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ‘ 𝑛 ) ∈ 𝒫 ( ℝ ↑m 𝑋 ) )
23 elpwi ⊢ ( ( 𝐴 ‘ 𝑛 ) ∈ 𝒫 ( ℝ ↑m 𝑋 ) → ( 𝐴 ‘ 𝑛 ) ⊆ ( ℝ ↑m 𝑋 ) )
24 22 23 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ‘ 𝑛 ) ⊆ ( ℝ ↑m 𝑋 ) )
25 4 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐸 ∈ ℝ+ )
26 nnnn0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
27 2nn ⊢ 2 ∈ ℕ
28 27 a1i ⊢ ( 𝑛 ∈ ℕ0 → 2 ∈ ℕ )
29 id ⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℕ0 )
30 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( 2 ↑ 𝑛 ) ∈ ℕ )
31 28 29 30 syl2anc ⊢ ( 𝑛 ∈ ℕ0 → ( 2 ↑ 𝑛 ) ∈ ℕ )
32 nnrp ⊢ ( ( 2 ↑ 𝑛 ) ∈ ℕ → ( 2 ↑ 𝑛 ) ∈ ℝ+ )
33 31 32 syl ⊢ ( 𝑛 ∈ ℕ0 → ( 2 ↑ 𝑛 ) ∈ ℝ+ )
34 26 33 syl ⊢ ( 𝑛 ∈ ℕ → ( 2 ↑ 𝑛 ) ∈ ℝ+ )
35 34 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2 ↑ 𝑛 ) ∈ ℝ+ )
36 25 35 rpdivcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐸 / ( 2 ↑ 𝑛 ) ) ∈ ℝ+ )
37 18 19 24 36 6 7 8 ovncvrrp ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∃ 𝑖 𝑖 ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) )
38 n0 ⊢ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ ↔ ∃ 𝑖 𝑖 ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) )
39 37 38 sylibr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ )
40 39 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) → ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ )
41 simpr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) → ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) )
42 40 41 mpd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) )
43 42 ex ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) )
44 43 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) )
45 17 44 mpd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) )
46 45 ex ⊢ ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) → ( 𝑛 ∈ ℕ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) )
47 15 46 ralrimi ⊢ ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) → ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) )
48 47 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) ) → ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) )
49 12 48 jca ⊢ ( ( 𝜑 ∧ ( 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) ) → ( 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) )
50 49 ex ⊢ ( 𝜑 → ( ( 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) → ( 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) )
51 50 eximdv ⊢ ( 𝜑 → ( ∃ 𝑔 ( 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) → ∃ 𝑔 ( 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) )
52 11 51 mpi ⊢ ( 𝜑 → ∃ 𝑔 ( 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) )
53 simpl ⊢ ( ( 𝜑 ∧ ( 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) → 𝜑 )
54 simprl ⊢ ( ( 𝜑 ∧ ( 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) → 𝑔 Fn ℕ )
55 simprr ⊢ ( ( 𝜑 ∧ ( 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) → ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) )
56 nnf1oxpnn ⊢ ∃ 𝑓 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ )
57 simpl1 ⊢ ( ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) → 𝜑 )
58 simpl2 ⊢ ( ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) → 𝑔 Fn ℕ )
59 fveq2 ⊢ ( 𝑞 = 𝑛 → ( 𝑔 ‘ 𝑞 ) = ( 𝑔 ‘ 𝑛 ) )
60 2fveq3 ⊢ ( 𝑞 = 𝑛 → ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) = ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) )
61 oveq2 ⊢ ( 𝑞 = 𝑛 → ( 2 ↑ 𝑞 ) = ( 2 ↑ 𝑛 ) )
62 61 oveq2d ⊢ ( 𝑞 = 𝑛 → ( 𝐸 / ( 2 ↑ 𝑞 ) ) = ( 𝐸 / ( 2 ↑ 𝑛 ) ) )
63 60 62 fveq12d ⊢ ( 𝑞 = 𝑛 → ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) = ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) )
64 59 63 eleq12d ⊢ ( 𝑞 = 𝑛 → ( ( 𝑔 ‘ 𝑞 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) ↔ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) )
65 64 cbvralvw ⊢ ( ∀ 𝑞 ∈ ℕ ( 𝑔 ‘ 𝑞 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) ↔ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) )
66 65 biimpri ⊢ ( ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) → ∀ 𝑞 ∈ ℕ ( 𝑔 ‘ 𝑞 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) )
67 66 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) → ∀ 𝑞 ∈ ℕ ( 𝑔 ‘ 𝑞 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) )
68 67 adantr ⊢ ( ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) → ∀ 𝑞 ∈ ℕ ( 𝑔 ‘ 𝑞 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) )
69 simpr ⊢ ( ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) → 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) )
70 1 adantr ⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) → 𝑋 ∈ Fin )
71 70 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑞 ∈ ℕ ( 𝑔 ‘ 𝑞 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) ) ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) → 𝑋 ∈ Fin )
72 2 adantr ⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) → 𝑋 ≠ ∅ )
73 72 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑞 ∈ ℕ ( 𝑔 ‘ 𝑞 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) ) ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) → 𝑋 ≠ ∅ )
74 3 adantr ⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) → 𝐴 : ℕ ⟶ 𝒫 ( ℝ ↑m 𝑋 ) )
75 74 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑞 ∈ ℕ ( 𝑔 ‘ 𝑞 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) ) ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) → 𝐴 : ℕ ⟶ 𝒫 ( ℝ ↑m 𝑋 ) )
76 4 adantr ⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) → 𝐸 ∈ ℝ+ )
77 76 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑞 ∈ ℕ ( 𝑔 ‘ 𝑞 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) ) ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) → 𝐸 ∈ ℝ+ )
78 coeq2 ⊢ ( ℎ = 𝑖 → ( [,) ∘ ℎ ) = ( [,) ∘ 𝑖 ) )
79 78 fveq1d ⊢ ( ℎ = 𝑖 → ( ( [,) ∘ ℎ ) ‘ 𝑘 ) = ( ( [,) ∘ 𝑖 ) ‘ 𝑘 ) )
80 79 fveq2d ⊢ ( ℎ = 𝑖 → ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑘 ) ) )
81 80 prodeq2ad ⊢ ( ℎ = 𝑖 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑘 ) ) )
82 81 cbvmptv ⊢ ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) ) = ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑘 ) ) )
83 7 82 eqtri ⊢ 𝐿 = ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑘 ) ) )
84 65 biimpi ⊢ ( ∀ 𝑞 ∈ ℕ ( 𝑔 ‘ 𝑞 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) → ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) )
85 84 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑞 ∈ ℕ ( 𝑔 ‘ 𝑞 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) ) → ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) )
86 85 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑞 ∈ ℕ ( 𝑔 ‘ 𝑞 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) ) ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) ∧ 𝑛 ∈ ℕ ) → ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) )
87 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑞 ∈ ℕ ( 𝑔 ‘ 𝑞 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) ) ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
88 rspa ⊢ ( ( ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) )
89 86 87 88 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑞 ∈ ℕ ( 𝑔 ‘ 𝑞 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) ) ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) )
90 simpr ⊢ ( ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑞 ∈ ℕ ( 𝑔 ‘ 𝑞 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) ) ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) → 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) )
91 2fveq3 ⊢ ( 𝑞 = 𝑚 → ( 1st ‘ ( 𝑓 ‘ 𝑞 ) ) = ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) )
92 91 fveq2d ⊢ ( 𝑞 = 𝑚 → ( 𝑔 ‘ ( 1st ‘ ( 𝑓 ‘ 𝑞 ) ) ) = ( 𝑔 ‘ ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ) )
93 2fveq3 ⊢ ( 𝑞 = 𝑚 → ( 2nd ‘ ( 𝑓 ‘ 𝑞 ) ) = ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) )
94 92 93 fveq12d ⊢ ( 𝑞 = 𝑚 → ( ( 𝑔 ‘ ( 1st ‘ ( 𝑓 ‘ 𝑞 ) ) ) ‘ ( 2nd ‘ ( 𝑓 ‘ 𝑞 ) ) ) = ( ( 𝑔 ‘ ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ) ‘ ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) ) )
95 94 cbvmptv ⊢ ( 𝑞 ∈ ℕ ↦ ( ( 𝑔 ‘ ( 1st ‘ ( 𝑓 ‘ 𝑞 ) ) ) ‘ ( 2nd ‘ ( 𝑓 ‘ 𝑞 ) ) ) ) = ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ) ‘ ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) ) )
96 71 73 75 77 5 6 83 8 89 90 95 ovnsubaddlem1 ⊢ ( ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑞 ∈ ℕ ( 𝑔 ‘ 𝑞 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) ) ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ≤ ( ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) +e 𝐸 ) )
97 57 58 68 69 96 syl31anc ⊢ ( ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ≤ ( ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) +e 𝐸 ) )
98 97 ex ⊢ ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) → ( 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ≤ ( ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) +e 𝐸 ) ) )
99 98 exlimdv ⊢ ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) → ( ∃ 𝑓 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ≤ ( ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) +e 𝐸 ) ) )
100 56 99 mpi ⊢ ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ≤ ( ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) +e 𝐸 ) )
101 53 54 55 100 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ≤ ( ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) +e 𝐸 ) )
102 101 ex ⊢ ( 𝜑 → ( ( 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ≤ ( ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) +e 𝐸 ) ) )
103 102 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑔 ( 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ≤ ( ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) +e 𝐸 ) ) )
104 52 103 mpd ⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ≤ ( ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) +e 𝐸 ) )