Metamath Proof Explorer

Theorem ovn0lem

Description: For any finite dimension, the Lebesgue outer measure of the empty set is zero. This is step (a)(ii) of the proof of Proposition 115D (a) of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses ovn0lem.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
ovn0lem.n0 ⊢ ( 𝜑 → 𝑋 ≠ ∅ )
ovn0lem.m ⊢ 𝑀 = { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) }
ovn0lem.infm ⊢ ( 𝜑 → inf ( 𝑀 , ℝ* , < ) ∈ ( 0 [,] +∞ ) )
ovn0lem.i ⊢ 𝐼 = ( 𝑗 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ⟨ 1 , 0 ⟩ ) )
Assertion ovn0lem ( 𝜑 → inf ( 𝑀 , ℝ* , < ) = 0 )

Proof

Step Hyp Ref Expression
1 ovn0lem.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
2 ovn0lem.n0 ⊢ ( 𝜑 → 𝑋 ≠ ∅ )
3 ovn0lem.m ⊢ 𝑀 = { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) }
4 ovn0lem.infm ⊢ ( 𝜑 → inf ( 𝑀 , ℝ* , < ) ∈ ( 0 [,] +∞ ) )
5 ovn0lem.i ⊢ 𝐼 = ( 𝑗 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ⟨ 1 , 0 ⟩ ) )
6 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
7 6 4 sseldi ⊢ ( 𝜑 → inf ( 𝑀 , ℝ* , < ) ∈ ℝ* )
8 0xr ⊢ 0 ∈ ℝ*
9 8 a1i ⊢ ( 𝜑 → 0 ∈ ℝ* )
10 ssrab2 ⊢ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) } ⊆ ℝ*
11 3 10 eqsstri ⊢ 𝑀 ⊆ ℝ*
12 11 a1i ⊢ ( 𝜑 → 𝑀 ⊆ ℝ* )
13 1re ⊢ 1 ∈ ℝ
14 0re ⊢ 0 ∈ ℝ
15 13 14 pm3.2i ⊢ ( 1 ∈ ℝ ∧ 0 ∈ ℝ )
16 opelxp ⊢ ( ⟨ 1 , 0 ⟩ ∈ ( ℝ × ℝ ) ↔ ( 1 ∈ ℝ ∧ 0 ∈ ℝ ) )
17 15 16 mpbir ⊢ ⟨ 1 , 0 ⟩ ∈ ( ℝ × ℝ )
18 17 a1i ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝑋 ) → ⟨ 1 , 0 ⟩ ∈ ( ℝ × ℝ ) )
19 eqid ⊢ ( 𝑙 ∈ 𝑋 ↦ ⟨ 1 , 0 ⟩ ) = ( 𝑙 ∈ 𝑋 ↦ ⟨ 1 , 0 ⟩ )
20 18 19 fmptd ⊢ ( 𝜑 → ( 𝑙 ∈ 𝑋 ↦ ⟨ 1 , 0 ⟩ ) : 𝑋 ⟶ ( ℝ × ℝ ) )
21 reex ⊢ ℝ ∈ V
22 21 21 xpex ⊢ ( ℝ × ℝ ) ∈ V
23 22 a1i ⊢ ( 𝜑 → ( ℝ × ℝ ) ∈ V )
24 elmapg ⊢ ( ( ( ℝ × ℝ ) ∈ V ∧ 𝑋 ∈ Fin ) → ( ( 𝑙 ∈ 𝑋 ↦ ⟨ 1 , 0 ⟩ ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↔ ( 𝑙 ∈ 𝑋 ↦ ⟨ 1 , 0 ⟩ ) : 𝑋 ⟶ ( ℝ × ℝ ) ) )
25 23 1 24 syl2anc ⊢ ( 𝜑 → ( ( 𝑙 ∈ 𝑋 ↦ ⟨ 1 , 0 ⟩ ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↔ ( 𝑙 ∈ 𝑋 ↦ ⟨ 1 , 0 ⟩ ) : 𝑋 ⟶ ( ℝ × ℝ ) ) )
26 20 25 mpbird ⊢ ( 𝜑 → ( 𝑙 ∈ 𝑋 ↦ ⟨ 1 , 0 ⟩ ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑙 ∈ 𝑋 ↦ ⟨ 1 , 0 ⟩ ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
28 27 5 fmptd ⊢ ( 𝜑 → 𝐼 : ℕ ⟶ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
29 ovexd ⊢ ( 𝜑 → ( ( ℝ × ℝ ) ↑m 𝑋 ) ∈ V )
30 nnex ⊢ ℕ ∈ V
31 30 a1i ⊢ ( 𝜑 → ℕ ∈ V )
32 elmapg ⊢ ( ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ∈ V ∧ ℕ ∈ V ) → ( 𝐼 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ↔ 𝐼 : ℕ ⟶ ( ( ℝ × ℝ ) ↑m 𝑋 ) ) )
33 29 31 32 syl2anc ⊢ ( 𝜑 → ( 𝐼 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ↔ 𝐼 : ℕ ⟶ ( ( ℝ × ℝ ) ↑m 𝑋 ) ) )
34 28 33 mpbird ⊢ ( 𝜑 → 𝐼 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) )
35 n0 ⊢ ( 𝑋 ≠ ∅ ↔ ∃ 𝑙 𝑙 ∈ 𝑋 )
36 2 35 sylib ⊢ ( 𝜑 → ∃ 𝑙 𝑙 ∈ 𝑋 )
37 36 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ∃ 𝑙 𝑙 ∈ 𝑋 )
38 nfv ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑙 ∈ 𝑋 )
39 nfcv ⊢ Ⅎ 𝑘 ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑙 ) )
40 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑙 ∈ 𝑋 ) → 𝑋 ∈ Fin )
41 28 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐼 ‘ 𝑗 ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
42 elmapi ⊢ ( ( 𝐼 ‘ 𝑗 ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) → ( 𝐼 ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
43 41 42 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐼 ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
44 43 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐼 ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
45 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → 𝑘 ∈ 𝑋 )
46 44 45 fvovco ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( 1st ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑘 ) ) ) )
47 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ )
48 27 elexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑙 ∈ 𝑋 ↦ ⟨ 1 , 0 ⟩ ) ∈ V )
49 5 fvmpt2 ⊢ ( ( 𝑗 ∈ ℕ ∧ ( 𝑙 ∈ 𝑋 ↦ ⟨ 1 , 0 ⟩ ) ∈ V ) → ( 𝐼 ‘ 𝑗 ) = ( 𝑙 ∈ 𝑋 ↦ ⟨ 1 , 0 ⟩ ) )
50 47 48 49 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐼 ‘ 𝑗 ) = ( 𝑙 ∈ 𝑋 ↦ ⟨ 1 , 0 ⟩ ) )
51 50 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐼 ‘ 𝑗 ) = ( 𝑙 ∈ 𝑋 ↦ ⟨ 1 , 0 ⟩ ) )
52 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑙 = 𝑘 ) → ⟨ 1 , 0 ⟩ = ⟨ 1 , 0 ⟩ )
53 17 elexi ⊢ ⟨ 1 , 0 ⟩ ∈ V
54 53 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ⟨ 1 , 0 ⟩ ∈ V )
55 51 52 45 54 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑘 ) = ⟨ 1 , 0 ⟩ )
56 55 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 1st ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑘 ) ) = ( 1st ‘ ⟨ 1 , 0 ⟩ ) )
57 13 elexi ⊢ 1 ∈ V
58 8 elexi ⊢ 0 ∈ V
59 57 58 op1st ⊢ ( 1st ‘ ⟨ 1 , 0 ⟩ ) = 1
60 59 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 1st ‘ ⟨ 1 , 0 ⟩ ) = 1 )
61 56 60 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 1st ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑘 ) ) = 1 )
62 55 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 2nd ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑘 ) ) = ( 2nd ‘ ⟨ 1 , 0 ⟩ ) )
63 57 58 op2nd ⊢ ( 2nd ‘ ⟨ 1 , 0 ⟩ ) = 0
64 63 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 2nd ‘ ⟨ 1 , 0 ⟩ ) = 0 )
65 62 64 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 2nd ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑘 ) ) = 0 )
66 61 65 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 1st ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑘 ) ) ) = ( 1 [,) 0 ) )
67 0le1 ⊢ 0 ≤ 1
68 1xr ⊢ 1 ∈ ℝ*
69 ico0 ⊢ ( ( 1 ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( ( 1 [,) 0 ) = ∅ ↔ 0 ≤ 1 ) )
70 68 8 69 mp2an ⊢ ( ( 1 [,) 0 ) = ∅ ↔ 0 ≤ 1 )
71 67 70 mpbir ⊢ ( 1 [,) 0 ) = ∅
72 71 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 1 [,) 0 ) = ∅ )
73 46 66 72 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) = ∅ )
74 73 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( vol ‘ ∅ ) )
75 vol0 ⊢ ( vol ‘ ∅ ) = 0
76 75 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ∅ ) = 0 )
77 74 76 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = 0 )
78 0cn ⊢ 0 ∈ ℂ
79 78 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → 0 ∈ ℂ )
80 77 79 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ∈ ℂ )
81 80 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑙 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ∈ ℂ )
82 2fveq3 ⊢ ( 𝑘 = 𝑙 → ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑙 ) ) )
83 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑙 ∈ 𝑋 ) → 𝑙 ∈ 𝑋 )
84 eleq1w ⊢ ( 𝑘 = 𝑙 → ( 𝑘 ∈ 𝑋 ↔ 𝑙 ∈ 𝑋 ) )
85 84 anbi2d ⊢ ( 𝑘 = 𝑙 → ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑙 ∈ 𝑋 ) ) )
86 82 eqeq1d ⊢ ( 𝑘 = 𝑙 → ( ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = 0 ↔ ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑙 ) ) = 0 ) )
87 85 86 imbi12d ⊢ ( 𝑘 = 𝑙 → ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = 0 ) ↔ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑙 ∈ 𝑋 ) → ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑙 ) ) = 0 ) ) )
88 87 77 chvarvv ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑙 ∈ 𝑋 ) → ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑙 ) ) = 0 )
89 38 39 40 81 82 83 88 fprod0 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑙 ∈ 𝑋 ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = 0 )
90 89 ex ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑙 ∈ 𝑋 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = 0 ) )
91 90 exlimdv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ∃ 𝑙 𝑙 ∈ 𝑋 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = 0 ) )
92 37 91 mpd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = 0 )
93 92 mpteq2dva ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) = ( 𝑗 ∈ ℕ ↦ 0 ) )
94 93 fveq2d ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ 0 ) ) )
95 nfv ⊢ Ⅎ 𝑗 𝜑
96 95 31 sge0z ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ 0 ) ) = 0 )
97 eqidd ⊢ ( 𝜑 → 0 = 0 )
98 94 96 97 3eqtrrd ⊢ ( 𝜑 → 0 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
99 fveq1 ⊢ ( 𝑖 = 𝐼 → ( 𝑖 ‘ 𝑗 ) = ( 𝐼 ‘ 𝑗 ) )
100 99 coeq2d ⊢ ( 𝑖 = 𝐼 → ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) = ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) )
101 100 fveq1d ⊢ ( 𝑖 = 𝐼 → ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) )
102 101 fveq2d ⊢ ( 𝑖 = 𝐼 → ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
103 102 ralrimivw ⊢ ( 𝑖 = 𝐼 → ∀ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
104 103 prodeq2d ⊢ ( 𝑖 = 𝐼 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
105 104 mpteq2dv ⊢ ( 𝑖 = 𝐼 → ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) = ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) )
106 105 fveq2d ⊢ ( 𝑖 = 𝐼 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
107 106 rspceeqv ⊢ ( ( 𝐼 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 0 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) 0 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
108 34 98 107 syl2anc ⊢ ( 𝜑 → ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) 0 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
109 9 108 jca ⊢ ( 𝜑 → ( 0 ∈ ℝ* ∧ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) 0 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
110 eqeq1 ⊢ ( 𝑧 = 0 → ( 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ↔ 0 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
111 110 rexbidv ⊢ ( 𝑧 = 0 → ( ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ↔ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) 0 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
112 111 3 elrab2 ⊢ ( 0 ∈ 𝑀 ↔ ( 0 ∈ ℝ* ∧ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) 0 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
113 109 112 sylibr ⊢ ( 𝜑 → 0 ∈ 𝑀 )
114 infxrlb ⊢ ( ( 𝑀 ⊆ ℝ* ∧ 0 ∈ 𝑀 ) → inf ( 𝑀 , ℝ* , < ) ≤ 0 )
115 12 113 114 syl2anc ⊢ ( 𝜑 → inf ( 𝑀 , ℝ* , < ) ≤ 0 )
116 pnfxr ⊢ +∞ ∈ ℝ*
117 116 a1i ⊢ ( 𝜑 → +∞ ∈ ℝ* )
118 iccgelb ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ inf ( 𝑀 , ℝ* , < ) ∈ ( 0 [,] +∞ ) ) → 0 ≤ inf ( 𝑀 , ℝ* , < ) )
119 9 117 4 118 syl3anc ⊢ ( 𝜑 → 0 ≤ inf ( 𝑀 , ℝ* , < ) )
120 7 9 115 119 xrletrid ⊢ ( 𝜑 → inf ( 𝑀 , ℝ* , < ) = 0 )