Metamath Proof Explorer

Theorem ovnsubadd

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

Ref Expression
Hypotheses ovnsubadd.1 ⊢ ( 𝜑 → 𝑋 ∈ Fin )
ovnsubadd.2 ⊢ ( 𝜑 → 𝐴 : ℕ ⟶ 𝒫 ( ℝ ↑m 𝑋 ) )
Assertion ovnsubadd ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ovnsubadd.1 ⊢ ( 𝜑 → 𝑋 ∈ Fin )
2 ovnsubadd.2 ⊢ ( 𝜑 → 𝐴 : ℕ ⟶ 𝒫 ( ℝ ↑m 𝑋 ) )
3 fveq2 ⊢ ( 𝑋 = ∅ → ( voln* ‘ 𝑋 ) = ( voln* ‘ ∅ ) )
4 3 fveq1d ⊢ ( 𝑋 = ∅ → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) = ( ( voln* ‘ ∅ ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) )
5 4 adantl ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) = ( ( voln* ‘ ∅ ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) )
6 2 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 : ℕ ⟶ 𝒫 ( ℝ ↑m 𝑋 ) )
7 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
8 6 7 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ‘ 𝑛 ) ∈ 𝒫 ( ℝ ↑m 𝑋 ) )
9 elpwi ⊢ ( ( 𝐴 ‘ 𝑛 ) ∈ 𝒫 ( ℝ ↑m 𝑋 ) → ( 𝐴 ‘ 𝑛 ) ⊆ ( ℝ ↑m 𝑋 ) )
10 8 9 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ‘ 𝑛 ) ⊆ ( ℝ ↑m 𝑋 ) )
11 10 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ⊆ ( ℝ ↑m 𝑋 ) )
12 iunss ⊢ ( ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ⊆ ( ℝ ↑m 𝑋 ) ↔ ∀ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ⊆ ( ℝ ↑m 𝑋 ) )
13 11 12 sylibr ⊢ ( 𝜑 → ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ⊆ ( ℝ ↑m 𝑋 ) )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ⊆ ( ℝ ↑m 𝑋 ) )
15 oveq2 ⊢ ( 𝑋 = ∅ → ( ℝ ↑m 𝑋 ) = ( ℝ ↑m ∅ ) )
16 15 adantl ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ℝ ↑m 𝑋 ) = ( ℝ ↑m ∅ ) )
17 14 16 sseqtrd ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ⊆ ( ℝ ↑m ∅ ) )
18 17 ovn0val ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( voln* ‘ ∅ ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) = 0 )
19 5 18 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) = 0 )
20 nnex ⊢ ℕ ∈ V
21 20 a1i ⊢ ( 𝜑 → ℕ ∈ V )
22 1 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑋 ∈ Fin )
23 22 10 ovncl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ ( 0 [,] +∞ ) )
24 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) )
25 23 24 fmptd ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) : ℕ ⟶ ( 0 [,] +∞ ) )
26 21 25 sge0ge0 ⊢ ( 𝜑 → 0 ≤ ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 0 ≤ ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) )
28 19 27 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) )
29 1 13 ovnxrcl ⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ∈ ℝ* )
30 29 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ∈ ℝ* )
31 21 25 sge0xrcl ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) ∈ ℝ* )
32 31 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) ∈ ℝ* )
33 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) ∧ 𝑦 ∈ ℝ+ ) → 𝑋 ∈ Fin )
34 neqne ⊢ ( ¬ 𝑋 = ∅ → 𝑋 ≠ ∅ )
35 34 ad2antlr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) ∧ 𝑦 ∈ ℝ+ ) → 𝑋 ≠ ∅ )
36 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) ∧ 𝑦 ∈ ℝ+ ) → 𝐴 : ℕ ⟶ 𝒫 ( ℝ ↑m 𝑋 ) )
37 simpr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ+ )
38 eqid ⊢ ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ) = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } )
39 sseq1 ⊢ ( 𝑏 = 𝑎 → ( 𝑏 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) ↔ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
40 39 rabbidv ⊢ ( 𝑏 = 𝑎 → { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } = { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } )
41 40 cbvmptv ⊢ ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } ) = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } )
42 eqid ⊢ ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) ) = ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) )
43 fveq2 ⊢ ( 𝑜 = 𝑗 → ( 𝑙 ‘ 𝑜 ) = ( 𝑙 ‘ 𝑗 ) )
44 43 coeq2d ⊢ ( 𝑜 = 𝑗 → ( [,) ∘ ( 𝑙 ‘ 𝑜 ) ) = ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) )
45 44 fveq1d ⊢ ( 𝑜 = 𝑗 → ( ( [,) ∘ ( 𝑙 ‘ 𝑜 ) ) ‘ 𝑑 ) = ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑑 ) )
46 45 ixpeq2dv ⊢ ( 𝑜 = 𝑗 → X 𝑑 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑜 ) ) ‘ 𝑑 ) = X 𝑑 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑑 ) )
47 fveq2 ⊢ ( 𝑑 = 𝑘 → ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑑 ) = ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) )
48 47 cbvixpv ⊢ X 𝑑 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑑 ) = X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 )
49 46 48 eqtrdi ⊢ ( 𝑜 = 𝑗 → X 𝑑 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑜 ) ) ‘ 𝑑 ) = X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) )
50 49 cbviunv ⊢ ∪ 𝑜 ∈ ℕ X 𝑑 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑜 ) ) ‘ 𝑑 ) = ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 )
51 50 sseq2i ⊢ ( 𝑏 ⊆ ∪ 𝑜 ∈ ℕ X 𝑑 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑜 ) ) ‘ 𝑑 ) ↔ 𝑏 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) )
52 51 rabbii ⊢ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑜 ∈ ℕ X 𝑑 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑜 ) ) ‘ 𝑑 ) } = { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) }
53 52 mpteq2i ⊢ ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑜 ∈ ℕ X 𝑑 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑜 ) ) ‘ 𝑑 ) } ) = ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } )
54 53 fveq1i ⊢ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑜 ∈ ℕ X 𝑑 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑜 ) ) ‘ 𝑑 ) } ) ‘ 𝑑 ) = ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑑 )
55 fveq2 ⊢ ( 𝑑 = 𝑎 → ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑑 ) = ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑎 ) )
56 54 55 eqtrid ⊢ ( 𝑑 = 𝑎 → ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑜 ∈ ℕ X 𝑑 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑜 ) ) ‘ 𝑑 ) } ) ‘ 𝑑 ) = ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑎 ) )
57 56 eleq2d ⊢ ( 𝑑 = 𝑎 → ( 𝑚 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑜 ∈ ℕ X 𝑑 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑜 ) ) ‘ 𝑑 ) } ) ‘ 𝑑 ) ↔ 𝑚 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑎 ) ) )
58 2fveq3 ⊢ ( 𝑑 = 𝑘 → ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑑 ) ) = ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) )
59 58 cbvprodv ⊢ ∏ 𝑑 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑑 ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) )
60 59 mpteq2i ⊢ ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑑 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑑 ) ) ) = ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) )
61 60 a1i ⊢ ( 𝑜 = 𝑗 → ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑑 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑑 ) ) ) = ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) ) )
62 fveq2 ⊢ ( 𝑜 = 𝑗 → ( 𝑚 ‘ 𝑜 ) = ( 𝑚 ‘ 𝑗 ) )
63 61 62 fveq12d ⊢ ( 𝑜 = 𝑗 → ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑑 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑑 ) ) ) ‘ ( 𝑚 ‘ 𝑜 ) ) = ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) ) ‘ ( 𝑚 ‘ 𝑗 ) ) )
64 63 cbvmptv ⊢ ( 𝑜 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑑 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑑 ) ) ) ‘ ( 𝑚 ‘ 𝑜 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) ) ‘ ( 𝑚 ‘ 𝑗 ) ) )
65 64 fveq2i ⊢ ( Σ^ ‘ ( 𝑜 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑑 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑑 ) ) ) ‘ ( 𝑚 ‘ 𝑜 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) ) ‘ ( 𝑚 ‘ 𝑗 ) ) ) )
66 65 a1i ⊢ ( 𝑑 = 𝑎 → ( Σ^ ‘ ( 𝑜 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑑 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑑 ) ) ) ‘ ( 𝑚 ‘ 𝑜 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) ) ‘ ( 𝑚 ‘ 𝑗 ) ) ) ) )
67 fveq2 ⊢ ( 𝑑 = 𝑎 → ( ( voln* ‘ 𝑋 ) ‘ 𝑑 ) = ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) )
68 67 oveq1d ⊢ ( 𝑑 = 𝑎 → ( ( ( voln* ‘ 𝑋 ) ‘ 𝑑 ) +𝑒 𝑓 ) = ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑓 ) )
69 66 68 breq12d ⊢ ( 𝑑 = 𝑎 → ( ( Σ^ ‘ ( 𝑜 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑑 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑑 ) ) ) ‘ ( 𝑚 ‘ 𝑜 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑑 ) +𝑒 𝑓 ) ↔ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) ) ‘ ( 𝑚 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑓 ) ) )
70 57 69 anbi12d ⊢ ( 𝑑 = 𝑎 → ( ( 𝑚 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑜 ∈ ℕ X 𝑑 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑜 ) ) ‘ 𝑑 ) } ) ‘ 𝑑 ) ∧ ( Σ^ ‘ ( 𝑜 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑑 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑑 ) ) ) ‘ ( 𝑚 ‘ 𝑜 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑑 ) +𝑒 𝑓 ) ) ↔ ( 𝑚 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑎 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) ) ‘ ( 𝑚 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑓 ) ) ) )
71 70 rabbidva2 ⊢ ( 𝑑 = 𝑎 → { 𝑚 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑜 ∈ ℕ X 𝑑 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑜 ) ) ‘ 𝑑 ) } ) ‘ 𝑑 ) ∣ ( Σ^ ‘ ( 𝑜 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑑 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑑 ) ) ) ‘ ( 𝑚 ‘ 𝑜 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑑 ) +𝑒 𝑓 ) } = { 𝑚 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) ) ‘ ( 𝑚 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑓 ) } )
72 fveq1 ⊢ ( 𝑚 = 𝑖 → ( 𝑚 ‘ 𝑗 ) = ( 𝑖 ‘ 𝑗 ) )
73 72 fveq2d ⊢ ( 𝑚 = 𝑖 → ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) ) ‘ ( 𝑚 ‘ 𝑗 ) ) = ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) ) ‘ ( 𝑖 ‘ 𝑗 ) ) )
74 73 mpteq2dv ⊢ ( 𝑚 = 𝑖 → ( 𝑗 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) ) ‘ ( 𝑚 ‘ 𝑗 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) ) ‘ ( 𝑖 ‘ 𝑗 ) ) ) )
75 74 fveq2d ⊢ ( 𝑚 = 𝑖 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) ) ‘ ( 𝑚 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) ) ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) )
76 75 breq1d ⊢ ( 𝑚 = 𝑖 → ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) ) ‘ ( 𝑚 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑓 ) ↔ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) ) ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑓 ) ) )
77 76 cbvrabv ⊢ { 𝑚 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) ) ‘ ( 𝑚 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑓 ) } = { 𝑖 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) ) ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑓 ) }
78 71 77 eqtrdi ⊢ ( 𝑑 = 𝑎 → { 𝑚 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑜 ∈ ℕ X 𝑑 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑜 ) ) ‘ 𝑑 ) } ) ‘ 𝑑 ) ∣ ( Σ^ ‘ ( 𝑜 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑑 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑑 ) ) ) ‘ ( 𝑚 ‘ 𝑜 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑑 ) +𝑒 𝑓 ) } = { 𝑖 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) ) ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑓 ) } )
79 78 mpteq2dv ⊢ ( 𝑑 = 𝑎 → ( 𝑓 ∈ ℝ+ ↦ { 𝑚 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑜 ∈ ℕ X 𝑑 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑜 ) ) ‘ 𝑑 ) } ) ‘ 𝑑 ) ∣ ( Σ^ ‘ ( 𝑜 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑑 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑑 ) ) ) ‘ ( 𝑚 ‘ 𝑜 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑑 ) +𝑒 𝑓 ) } ) = ( 𝑓 ∈ ℝ+ ↦ { 𝑖 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) ) ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑓 ) } ) )
80 oveq2 ⊢ ( 𝑓 = 𝑒 → ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑓 ) = ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑒 ) )
81 80 breq2d ⊢ ( 𝑓 = 𝑒 → ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) ) ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑓 ) ↔ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) ) ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑒 ) ) )
82 81 rabbidv ⊢ ( 𝑓 = 𝑒 → { 𝑖 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) ) ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑓 ) } = { 𝑖 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) ) ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑒 ) } )
83 82 cbvmptv ⊢ ( 𝑓 ∈ ℝ+ ↦ { 𝑖 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) ) ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑓 ) } ) = ( 𝑒 ∈ ℝ+ ↦ { 𝑖 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) ) ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑒 ) } )
84 79 83 eqtrdi ⊢ ( 𝑑 = 𝑎 → ( 𝑓 ∈ ℝ+ ↦ { 𝑚 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑜 ∈ ℕ X 𝑑 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑜 ) ) ‘ 𝑑 ) } ) ‘ 𝑑 ) ∣ ( Σ^ ‘ ( 𝑜 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑑 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑑 ) ) ) ‘ ( 𝑚 ‘ 𝑜 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑑 ) +𝑒 𝑓 ) } ) = ( 𝑒 ∈ ℝ+ ↦ { 𝑖 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) ) ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑒 ) } ) )
85 84 cbvmptv ⊢ ( 𝑑 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ ( 𝑓 ∈ ℝ+ ↦ { 𝑚 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑜 ∈ ℕ X 𝑑 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑜 ) ) ‘ 𝑑 ) } ) ‘ 𝑑 ) ∣ ( Σ^ ‘ ( 𝑜 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑑 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑑 ) ) ) ‘ ( 𝑚 ‘ 𝑜 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑑 ) +𝑒 𝑓 ) } ) ) = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ ( 𝑒 ∈ ℝ+ ↦ { 𝑖 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) ) ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑒 ) } ) )
86 33 35 36 37 38 41 42 85 ovnsubaddlem2 ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) ∧ 𝑦 ∈ ℝ+ ) → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ≤ ( ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) +𝑒 𝑦 ) )
87 30 32 86 xrlexaddrp ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) )
88 28 87 pm2.61dan ⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) )