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 sselid ( 𝜑 → 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 )