Metamath Proof Explorer

Theorem ovnlecvr

Description: Given a subset of multidimensional reals and a set of half-open intervals that covers it, the Lebesgue outer measure of the set is bounded by the generalized sum of the pre-measure of the half-open intervals. The statement would also be true with X the empty set, but covers are not used for the zero-dimensional case. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses ovnlecvr.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
ovnlecvr.n0 ⊢ ( 𝜑 → 𝑋 ≠ ∅ )
ovnlecvr.l ⊢ 𝐿 = ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑘 ) ) )
ovnlecvr.i ⊢ ( 𝜑 → 𝐼 : ℕ ⟶ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
ovnlecvr.ss ⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) )
Assertion ovnlecvr ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ovnlecvr.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
2 ovnlecvr.n0 ⊢ ( 𝜑 → 𝑋 ≠ ∅ )
3 ovnlecvr.l ⊢ 𝐿 = ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑘 ) ) )
4 ovnlecvr.i ⊢ ( 𝜑 → 𝐼 : ℕ ⟶ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
5 ovnlecvr.ss ⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) )
6 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐼 ‘ 𝑗 ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
7 elmapi ⊢ ( ( 𝐼 ‘ 𝑗 ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) → ( 𝐼 ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
8 6 7 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐼 ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
9 8 hoissrrn ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ⊆ ( ℝ ↑m 𝑋 ) )
10 9 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ⊆ ( ℝ ↑m 𝑋 ) )
11 iunss ⊢ ( ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ⊆ ( ℝ ↑m 𝑋 ) ↔ ∀ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ⊆ ( ℝ ↑m 𝑋 ) )
12 10 11 sylibr ⊢ ( 𝜑 → ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ⊆ ( ℝ ↑m 𝑋 ) )
13 5 12 sstrd ⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
14 eqid ⊢ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } = { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) }
15 1 2 13 14 ovnn0val ⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) = inf ( { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } , ℝ* , < ) )
16 ssrab2 ⊢ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ⊆ ℝ*
17 16 a1i ⊢ ( 𝜑 → { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ⊆ ℝ* )
18 nnex ⊢ ℕ ∈ V
19 18 a1i ⊢ ( 𝜑 → ℕ ∈ V )
20 icossicc ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
21 nfv ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ ℕ )
22 1 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑋 ∈ Fin )
23 21 22 3 8 hoiprodcl2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) ∈ ( 0 [,) +∞ ) )
24 20 23 sselid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) ∈ ( 0 [,] +∞ ) )
25 eqid ⊢ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) )
26 24 25 fmptd ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) ) : ℕ ⟶ ( 0 [,] +∞ ) )
27 19 26 sge0xrcl ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) ) ) ∈ ℝ* )
28 ovex ⊢ ( ( ℝ × ℝ ) ↑m 𝑋 ) ∈ V
29 28 18 pm3.2i ⊢ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ∈ V ∧ ℕ ∈ V )
30 elmapg ⊢ ( ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ∈ V ∧ ℕ ∈ V ) → ( 𝐼 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ↔ 𝐼 : ℕ ⟶ ( ( ℝ × ℝ ) ↑m 𝑋 ) ) )
31 29 30 ax-mp ⊢ ( 𝐼 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ↔ 𝐼 : ℕ ⟶ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
32 4 31 sylibr ⊢ ( 𝜑 → 𝐼 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) )
33 coeq2 ⊢ ( 𝑖 = ( 𝐼 ‘ 𝑗 ) → ( [,) ∘ 𝑖 ) = ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) )
34 33 fveq1d ⊢ ( 𝑖 = ( 𝐼 ‘ 𝑗 ) → ( ( [,) ∘ 𝑖 ) ‘ 𝑘 ) = ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) )
35 34 fveq2d ⊢ ( 𝑖 = ( 𝐼 ‘ 𝑗 ) → ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
36 35 prodeq2ad ⊢ ( 𝑖 = ( 𝐼 ‘ 𝑗 ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑘 ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
37 prodex ⊢ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ∈ V
38 37 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ∈ V )
39 3 36 6 38 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
40 39 mpteq2dva ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) ) = ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) )
41 40 fveq2d ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
42 5 41 jca ⊢ ( 𝜑 → ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
43 nfv ⊢ Ⅎ 𝑘 𝑖 = 𝐼
44 fveq1 ⊢ ( 𝑖 = 𝐼 → ( 𝑖 ‘ 𝑗 ) = ( 𝐼 ‘ 𝑗 ) )
45 44 coeq2d ⊢ ( 𝑖 = 𝐼 → ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) = ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) )
46 45 fveq1d ⊢ ( 𝑖 = 𝐼 → ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) )
47 46 adantr ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑘 ∈ 𝑋 ) → ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) )
48 43 47 ixpeq2d ⊢ ( 𝑖 = 𝐼 → X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) )
49 48 iuneq2d ⊢ ( 𝑖 = 𝐼 → ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) )
50 49 sseq2d ⊢ ( 𝑖 = 𝐼 → ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ↔ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
51 46 fveq2d ⊢ ( 𝑖 = 𝐼 → ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
52 51 prodeq2ad ⊢ ( 𝑖 = 𝐼 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
53 52 mpteq2dv ⊢ ( 𝑖 = 𝐼 → ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) = ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) )
54 53 fveq2d ⊢ ( 𝑖 = 𝐼 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
55 54 eqeq2d ⊢ ( 𝑖 = 𝐼 → ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ↔ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
56 50 55 anbi12d ⊢ ( 𝑖 = 𝐼 → ( ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ↔ ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
57 56 rspcev ⊢ ( ( 𝐼 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
58 32 42 57 syl2anc ⊢ ( 𝜑 → ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
59 27 58 jca ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) ) ) ∈ ℝ* ∧ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
60 eqeq1 ⊢ ( 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) ) ) → ( 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ↔ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
61 60 anbi2d ⊢ ( 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) ) ) → ( ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ↔ ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
62 61 rexbidv ⊢ ( 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) ) ) → ( ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ↔ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
63 62 elrab ⊢ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) ) ) ∈ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ↔ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) ) ) ∈ ℝ* ∧ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
64 59 63 sylibr ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) ) ) ∈ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } )
65 infxrlb ⊢ ( ( { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ⊆ ℝ* ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) ) ) ∈ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ) → inf ( { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } , ℝ* , < ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) ) ) )
66 17 64 65 syl2anc ⊢ ( 𝜑 → inf ( { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } , ℝ* , < ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) ) ) )
67 15 66 eqbrtrd ⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝐼 ‘ 𝑗 ) ) ) ) )