Metamath Proof Explorer

Theorem ovnhoilem1

Description: The Lebesgue outer measure of a multidimensional half-open interval is less than or equal to the product of its length in each dimension. First part of the proof of Proposition 115D (b) of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses ovnhoilem1.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
ovnhoilem1.a ⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
ovnhoilem1.b ⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
ovnhoilem1.c ⊢ 𝐼 = X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) )
ovnhoilem1.m ⊢ 𝑀 = { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) }
ovnhoilem1.h ⊢ 𝐻 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ if ( 𝑗 = 1 , ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ , ⟨ 0 , 0 ⟩ ) ) )
Assertion ovnhoilem1 ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐼 ) ≤ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )

Proof

Step Hyp Ref Expression
1 ovnhoilem1.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
2 ovnhoilem1.a ⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
3 ovnhoilem1.b ⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
4 ovnhoilem1.c ⊢ 𝐼 = X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) )
5 ovnhoilem1.m ⊢ 𝑀 = { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) }
6 ovnhoilem1.h ⊢ 𝐻 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ if ( 𝑗 = 1 , ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ , ⟨ 0 , 0 ⟩ ) ) )
7 4 a1i ⊢ ( 𝜑 → 𝐼 = X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) )
8 nfv ⊢ Ⅎ 𝑘 𝜑
9 2 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
10 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
11 10 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ* )
12 8 9 11 hoissrrn2 ⊢ ( 𝜑 → X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ⊆ ( ℝ ↑m 𝑋 ) )
13 7 12 eqsstrd ⊢ ( 𝜑 → 𝐼 ⊆ ( ℝ ↑m 𝑋 ) )
14 1 13 5 ovnval2 ⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐼 ) = if ( 𝑋 = ∅ , 0 , inf ( 𝑀 , ℝ* , < ) ) )
15 iftrue ⊢ ( 𝑋 = ∅ → if ( 𝑋 = ∅ , 0 , inf ( 𝑀 , ℝ* , < ) ) = 0 )
16 15 adantl ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → if ( 𝑋 = ∅ , 0 , inf ( 𝑀 , ℝ* , < ) ) = 0 )
17 0xr ⊢ 0 ∈ ℝ*
18 17 a1i ⊢ ( 𝜑 → 0 ∈ ℝ* )
19 pnfxr ⊢ +∞ ∈ ℝ*
20 19 a1i ⊢ ( 𝜑 → +∞ ∈ ℝ* )
21 8 1 9 10 hoiprodcl3 ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ( 0 [,) +∞ ) )
22 icogelb ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ( 0 [,) +∞ ) ) → 0 ≤ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
23 18 20 21 22 syl3anc ⊢ ( 𝜑 → 0 ≤ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 0 ≤ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
25 16 24 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → if ( 𝑋 = ∅ , 0 , inf ( 𝑀 , ℝ* , < ) ) ≤ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
26 iffalse ⊢ ( ¬ 𝑋 = ∅ → if ( 𝑋 = ∅ , 0 , inf ( 𝑀 , ℝ* , < ) ) = inf ( 𝑀 , ℝ* , < ) )
27 26 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → if ( 𝑋 = ∅ , 0 , inf ( 𝑀 , ℝ* , < ) ) = inf ( 𝑀 , ℝ* , < ) )
28 ssrab2 ⊢ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ⊆ ℝ*
29 5 28 eqsstri ⊢ 𝑀 ⊆ ℝ*
30 29 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → 𝑀 ⊆ ℝ* )
31 icossxr ⊢ ( 0 [,) +∞ ) ⊆ ℝ*
32 31 21 sselid ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℝ* )
33 32 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℝ* )
34 opelxpi ⊢ ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑘 ) ∈ ℝ ) → ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ ∈ ( ℝ × ℝ ) )
35 9 10 34 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ ∈ ( ℝ × ℝ ) )
36 0re ⊢ 0 ∈ ℝ
37 opelxpi ⊢ ( ( 0 ∈ ℝ ∧ 0 ∈ ℝ ) → ⟨ 0 , 0 ⟩ ∈ ( ℝ × ℝ ) )
38 36 36 37 mp2an ⊢ ⟨ 0 , 0 ⟩ ∈ ( ℝ × ℝ )
39 38 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ⟨ 0 , 0 ⟩ ∈ ( ℝ × ℝ ) )
40 35 39 ifcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → if ( 𝑗 = 1 , ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ , ⟨ 0 , 0 ⟩ ) ∈ ( ℝ × ℝ ) )
41 40 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑋 ↦ if ( 𝑗 = 1 , ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ , ⟨ 0 , 0 ⟩ ) ) : 𝑋 ⟶ ( ℝ × ℝ ) )
42 reex ⊢ ℝ ∈ V
43 42 42 xpex ⊢ ( ℝ × ℝ ) ∈ V
44 1 43 jctil ⊢ ( 𝜑 → ( ( ℝ × ℝ ) ∈ V ∧ 𝑋 ∈ Fin ) )
45 elmapg ⊢ ( ( ( ℝ × ℝ ) ∈ V ∧ 𝑋 ∈ Fin ) → ( ( 𝑘 ∈ 𝑋 ↦ if ( 𝑗 = 1 , ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ , ⟨ 0 , 0 ⟩ ) ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↔ ( 𝑘 ∈ 𝑋 ↦ if ( 𝑗 = 1 , ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ , ⟨ 0 , 0 ⟩ ) ) : 𝑋 ⟶ ( ℝ × ℝ ) ) )
46 44 45 syl ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝑋 ↦ if ( 𝑗 = 1 , ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ , ⟨ 0 , 0 ⟩ ) ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↔ ( 𝑘 ∈ 𝑋 ↦ if ( 𝑗 = 1 , ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ , ⟨ 0 , 0 ⟩ ) ) : 𝑋 ⟶ ( ℝ × ℝ ) ) )
47 41 46 mpbird ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑋 ↦ if ( 𝑗 = 1 , ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ , ⟨ 0 , 0 ⟩ ) ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
48 47 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑘 ∈ 𝑋 ↦ if ( 𝑗 = 1 , ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ , ⟨ 0 , 0 ⟩ ) ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
49 48 6 fmptd ⊢ ( 𝜑 → 𝐻 : ℕ ⟶ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
50 ovex ⊢ ( ( ℝ × ℝ ) ↑m 𝑋 ) ∈ V
51 nnex ⊢ ℕ ∈ V
52 50 51 elmap ⊢ ( 𝐻 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ↔ 𝐻 : ℕ ⟶ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
53 49 52 sylibr ⊢ ( 𝜑 → 𝐻 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) )
54 53 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → 𝐻 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) )
55 eqidd ⊢ ( 𝜑 → X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) = X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) )
56 35 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑋 ↦ ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ ) : 𝑋 ⟶ ( ℝ × ℝ ) )
57 iftrue ⊢ ( 𝑗 = 1 → if ( 𝑗 = 1 , ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ , ⟨ 0 , 0 ⟩ ) = ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ )
58 57 mpteq2dv ⊢ ( 𝑗 = 1 → ( 𝑘 ∈ 𝑋 ↦ if ( 𝑗 = 1 , ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ , ⟨ 0 , 0 ⟩ ) ) = ( 𝑘 ∈ 𝑋 ↦ ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ ) )
59 1nn ⊢ 1 ∈ ℕ
60 59 a1i ⊢ ( 𝜑 → 1 ∈ ℕ )
61 mptexg ⊢ ( 𝑋 ∈ Fin → ( 𝑘 ∈ 𝑋 ↦ ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ ) ∈ V )
62 1 61 syl ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑋 ↦ ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ ) ∈ V )
63 6 58 60 62 fvmptd3 ⊢ ( 𝜑 → ( 𝐻 ‘ 1 ) = ( 𝑘 ∈ 𝑋 ↦ ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ ) )
64 63 feq1d ⊢ ( 𝜑 → ( ( 𝐻 ‘ 1 ) : 𝑋 ⟶ ( ℝ × ℝ ) ↔ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ ) : 𝑋 ⟶ ( ℝ × ℝ ) ) )
65 56 64 mpbird ⊢ ( 𝜑 → ( 𝐻 ‘ 1 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
66 65 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐻 ‘ 1 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
67 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝑘 ∈ 𝑋 )
68 66 67 fvovco ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( [,) ∘ ( 𝐻 ‘ 1 ) ) ‘ 𝑘 ) = ( ( 1st ‘ ( ( 𝐻 ‘ 1 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝐻 ‘ 1 ) ‘ 𝑘 ) ) ) )
69 35 elexd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ ∈ V )
70 63 69 fvmpt2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐻 ‘ 1 ) ‘ 𝑘 ) = ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ )
71 70 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 1st ‘ ( ( 𝐻 ‘ 1 ) ‘ 𝑘 ) ) = ( 1st ‘ ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ ) )
72 fvex ⊢ ( 𝐴 ‘ 𝑘 ) ∈ V
73 fvex ⊢ ( 𝐵 ‘ 𝑘 ) ∈ V
74 72 73 op1st ⊢ ( 1st ‘ ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ ) = ( 𝐴 ‘ 𝑘 )
75 74 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 1st ‘ ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ ) = ( 𝐴 ‘ 𝑘 ) )
76 71 75 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 1st ‘ ( ( 𝐻 ‘ 1 ) ‘ 𝑘 ) ) = ( 𝐴 ‘ 𝑘 ) )
77 70 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 2nd ‘ ( ( 𝐻 ‘ 1 ) ‘ 𝑘 ) ) = ( 2nd ‘ ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ ) )
78 72 73 op2nd ⊢ ( 2nd ‘ ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ ) = ( 𝐵 ‘ 𝑘 )
79 78 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 2nd ‘ ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ ) = ( 𝐵 ‘ 𝑘 ) )
80 77 79 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 2nd ‘ ( ( 𝐻 ‘ 1 ) ‘ 𝑘 ) ) = ( 𝐵 ‘ 𝑘 ) )
81 76 80 oveq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( 1st ‘ ( ( 𝐻 ‘ 1 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝐻 ‘ 1 ) ‘ 𝑘 ) ) ) = ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) )
82 68 81 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( [,) ∘ ( 𝐻 ‘ 1 ) ) ‘ 𝑘 ) = ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) )
83 82 ixpeq2dva ⊢ ( 𝜑 → X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐻 ‘ 1 ) ) ‘ 𝑘 ) = X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) )
84 55 7 83 3eqtr4d ⊢ ( 𝜑 → 𝐼 = X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐻 ‘ 1 ) ) ‘ 𝑘 ) )
85 fveq2 ⊢ ( 𝑗 = 1 → ( 𝐻 ‘ 𝑗 ) = ( 𝐻 ‘ 1 ) )
86 85 coeq2d ⊢ ( 𝑗 = 1 → ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) = ( [,) ∘ ( 𝐻 ‘ 1 ) ) )
87 86 fveq1d ⊢ ( 𝑗 = 1 → ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( [,) ∘ ( 𝐻 ‘ 1 ) ) ‘ 𝑘 ) )
88 87 ixpeq2dv ⊢ ( 𝑗 = 1 → X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) = X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐻 ‘ 1 ) ) ‘ 𝑘 ) )
89 88 ssiun2s ⊢ ( 1 ∈ ℕ → X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐻 ‘ 1 ) ) ‘ 𝑘 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) )
90 59 89 ax-mp ⊢ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐻 ‘ 1 ) ) ‘ 𝑘 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 )
91 84 90 eqsstrdi ⊢ ( 𝜑 → 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) )
92 91 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) )
93 82 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 1 ) ) ‘ 𝑘 ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
94 93 eqcomd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 1 ) ) ‘ 𝑘 ) ) )
95 94 prodeq2dv ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 1 ) ) ‘ 𝑘 ) ) )
96 95 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 1 ) ) ‘ 𝑘 ) ) )
97 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
98 icossicc ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
99 8 1 65 hoiprodcl ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 1 ) ) ‘ 𝑘 ) ) ∈ ( 0 [,) +∞ ) )
100 98 99 sselid ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 1 ) ) ‘ 𝑘 ) ) ∈ ( 0 [,] +∞ ) )
101 87 fveq2d ⊢ ( 𝑗 = 1 → ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 1 ) ) ‘ 𝑘 ) ) )
102 101 prodeq2ad ⊢ ( 𝑗 = 1 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 1 ) ) ‘ 𝑘 ) ) )
103 97 100 102 sge0snmpt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ { 1 } ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 1 ) ) ‘ 𝑘 ) ) )
104 103 eqcomd ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 1 ) ) ‘ 𝑘 ) ) = ( Σ^ ‘ ( 𝑗 ∈ { 1 } ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
105 104 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 1 ) ) ‘ 𝑘 ) ) = ( Σ^ ‘ ( 𝑗 ∈ { 1 } ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
106 nfv ⊢ Ⅎ 𝑗 ( 𝜑 ∧ ¬ 𝑋 = ∅ )
107 51 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ℕ ∈ V )
108 snssi ⊢ ( 1 ∈ ℕ → { 1 } ⊆ ℕ )
109 59 108 ax-mp ⊢ { 1 } ⊆ ℕ
110 109 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → { 1 } ⊆ ℕ )
111 nfv ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) ∧ 𝑗 ∈ { 1 } )
112 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) ∧ 𝑗 ∈ { 1 } ) → 𝑋 ∈ Fin )
113 simpl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ { 1 } ) → 𝜑 )
114 elsni ⊢ ( 𝑗 ∈ { 1 } → 𝑗 = 1 )
115 114 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ { 1 } ) → 𝑗 = 1 )
116 65 adantr ⊢ ( ( 𝜑 ∧ 𝑗 = 1 ) → ( 𝐻 ‘ 1 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
117 85 adantl ⊢ ( ( 𝜑 ∧ 𝑗 = 1 ) → ( 𝐻 ‘ 𝑗 ) = ( 𝐻 ‘ 1 ) )
118 117 feq1d ⊢ ( ( 𝜑 ∧ 𝑗 = 1 ) → ( ( 𝐻 ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) ↔ ( 𝐻 ‘ 1 ) : 𝑋 ⟶ ( ℝ × ℝ ) ) )
119 116 118 mpbird ⊢ ( ( 𝜑 ∧ 𝑗 = 1 ) → ( 𝐻 ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
120 113 115 119 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ { 1 } ) → ( 𝐻 ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
121 120 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) ∧ 𝑗 ∈ { 1 } ) → ( 𝐻 ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
122 111 112 121 hoiprodcl ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) ∧ 𝑗 ∈ { 1 } ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ∈ ( 0 [,) +∞ ) )
123 98 122 sselid ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) ∧ 𝑗 ∈ { 1 } ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ∈ ( 0 [,] +∞ ) )
124 39 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑋 ↦ ⟨ 0 , 0 ⟩ ) : 𝑋 ⟶ ( ℝ × ℝ ) )
125 124 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 1 } ) ) → ( 𝑘 ∈ 𝑋 ↦ ⟨ 0 , 0 ⟩ ) : 𝑋 ⟶ ( ℝ × ℝ ) )
126 simpl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 1 } ) ) → 𝜑 )
127 eldifi ⊢ ( 𝑗 ∈ ( ℕ ∖ { 1 } ) → 𝑗 ∈ ℕ )
128 127 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 1 } ) ) → 𝑗 ∈ ℕ )
129 6 a1i ⊢ ( 𝜑 → 𝐻 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ if ( 𝑗 = 1 , ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ , ⟨ 0 , 0 ⟩ ) ) ) )
130 48 elexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑘 ∈ 𝑋 ↦ if ( 𝑗 = 1 , ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ , ⟨ 0 , 0 ⟩ ) ) ∈ V )
131 129 130 fvmpt2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐻 ‘ 𝑗 ) = ( 𝑘 ∈ 𝑋 ↦ if ( 𝑗 = 1 , ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ , ⟨ 0 , 0 ⟩ ) ) )
132 126 128 131 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 1 } ) ) → ( 𝐻 ‘ 𝑗 ) = ( 𝑘 ∈ 𝑋 ↦ if ( 𝑗 = 1 , ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ , ⟨ 0 , 0 ⟩ ) ) )
133 eldifsni ⊢ ( 𝑗 ∈ ( ℕ ∖ { 1 } ) → 𝑗 ≠ 1 )
134 133 neneqd ⊢ ( 𝑗 ∈ ( ℕ ∖ { 1 } ) → ¬ 𝑗 = 1 )
135 134 iffalsed ⊢ ( 𝑗 ∈ ( ℕ ∖ { 1 } ) → if ( 𝑗 = 1 , ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ , ⟨ 0 , 0 ⟩ ) = ⟨ 0 , 0 ⟩ )
136 135 mpteq2dv ⊢ ( 𝑗 ∈ ( ℕ ∖ { 1 } ) → ( 𝑘 ∈ 𝑋 ↦ if ( 𝑗 = 1 , ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ , ⟨ 0 , 0 ⟩ ) ) = ( 𝑘 ∈ 𝑋 ↦ ⟨ 0 , 0 ⟩ ) )
137 136 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 1 } ) ) → ( 𝑘 ∈ 𝑋 ↦ if ( 𝑗 = 1 , ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ , ⟨ 0 , 0 ⟩ ) ) = ( 𝑘 ∈ 𝑋 ↦ ⟨ 0 , 0 ⟩ ) )
138 132 137 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 1 } ) ) → ( 𝐻 ‘ 𝑗 ) = ( 𝑘 ∈ 𝑋 ↦ ⟨ 0 , 0 ⟩ ) )
139 138 feq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 1 } ) ) → ( ( 𝐻 ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) ↔ ( 𝑘 ∈ 𝑋 ↦ ⟨ 0 , 0 ⟩ ) : 𝑋 ⟶ ( ℝ × ℝ ) ) )
140 125 139 mpbird ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 1 } ) ) → ( 𝐻 ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
141 140 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 1 } ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐻 ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
142 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 1 } ) ) ∧ 𝑘 ∈ 𝑋 ) → 𝑘 ∈ 𝑋 )
143 141 142 fvovco ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 1 } ) ) ∧ 𝑘 ∈ 𝑋 ) → ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( 1st ‘ ( ( 𝐻 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝐻 ‘ 𝑗 ) ‘ 𝑘 ) ) ) )
144 38 elexi ⊢ ⟨ 0 , 0 ⟩ ∈ V
145 144 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 1 } ) ) ∧ 𝑘 ∈ 𝑋 ) → ⟨ 0 , 0 ⟩ ∈ V )
146 138 145 fvmpt2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 1 } ) ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐻 ‘ 𝑗 ) ‘ 𝑘 ) = ⟨ 0 , 0 ⟩ )
147 146 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 1 } ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 1st ‘ ( ( 𝐻 ‘ 𝑗 ) ‘ 𝑘 ) ) = ( 1st ‘ ⟨ 0 , 0 ⟩ ) )
148 17 elexi ⊢ 0 ∈ V
149 148 148 op1st ⊢ ( 1st ‘ ⟨ 0 , 0 ⟩ ) = 0
150 149 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 1 } ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 1st ‘ ⟨ 0 , 0 ⟩ ) = 0 )
151 147 150 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 1 } ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 1st ‘ ( ( 𝐻 ‘ 𝑗 ) ‘ 𝑘 ) ) = 0 )
152 146 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 1 } ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 2nd ‘ ( ( 𝐻 ‘ 𝑗 ) ‘ 𝑘 ) ) = ( 2nd ‘ ⟨ 0 , 0 ⟩ ) )
153 148 148 op2nd ⊢ ( 2nd ‘ ⟨ 0 , 0 ⟩ ) = 0
154 153 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 1 } ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 2nd ‘ ⟨ 0 , 0 ⟩ ) = 0 )
155 152 154 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 1 } ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 2nd ‘ ( ( 𝐻 ‘ 𝑗 ) ‘ 𝑘 ) ) = 0 )
156 151 155 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 1 } ) ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 1st ‘ ( ( 𝐻 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝐻 ‘ 𝑗 ) ‘ 𝑘 ) ) ) = ( 0 [,) 0 ) )
157 0le0 ⊢ 0 ≤ 0
158 ico0 ⊢ ( ( 0 ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( ( 0 [,) 0 ) = ∅ ↔ 0 ≤ 0 ) )
159 17 17 158 mp2an ⊢ ( ( 0 [,) 0 ) = ∅ ↔ 0 ≤ 0 )
160 157 159 mpbir ⊢ ( 0 [,) 0 ) = ∅
161 160 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 1 } ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 0 [,) 0 ) = ∅ )
162 143 156 161 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 1 } ) ) ∧ 𝑘 ∈ 𝑋 ) → ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) = ∅ )
163 162 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 1 } ) ) ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( vol ‘ ∅ ) )
164 vol0 ⊢ ( vol ‘ ∅ ) = 0
165 164 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 1 } ) ) ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ∅ ) = 0 )
166 163 165 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 1 } ) ) ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = 0 )
167 166 prodeq2dv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 1 } ) ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ∏ 𝑘 ∈ 𝑋 0 )
168 167 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) ∧ 𝑗 ∈ ( ℕ ∖ { 1 } ) ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ∏ 𝑘 ∈ 𝑋 0 )
169 0cnd ⊢ ( 𝜑 → 0 ∈ ℂ )
170 fprodconst ⊢ ( ( 𝑋 ∈ Fin ∧ 0 ∈ ℂ ) → ∏ 𝑘 ∈ 𝑋 0 = ( 0 ↑ ( ♯ ‘ 𝑋 ) ) )
171 1 169 170 syl2anc ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 0 = ( 0 ↑ ( ♯ ‘ 𝑋 ) ) )
172 171 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) ∧ 𝑗 ∈ ( ℕ ∖ { 1 } ) ) → ∏ 𝑘 ∈ 𝑋 0 = ( 0 ↑ ( ♯ ‘ 𝑋 ) ) )
173 neqne ⊢ ( ¬ 𝑋 = ∅ → 𝑋 ≠ ∅ )
174 173 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → 𝑋 ≠ ∅ )
175 1 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → 𝑋 ∈ Fin )
176 hashnncl ⊢ ( 𝑋 ∈ Fin → ( ( ♯ ‘ 𝑋 ) ∈ ℕ ↔ 𝑋 ≠ ∅ ) )
177 175 176 syl ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ( ( ♯ ‘ 𝑋 ) ∈ ℕ ↔ 𝑋 ≠ ∅ ) )
178 174 177 mpbird ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ( ♯ ‘ 𝑋 ) ∈ ℕ )
179 0exp ⊢ ( ( ♯ ‘ 𝑋 ) ∈ ℕ → ( 0 ↑ ( ♯ ‘ 𝑋 ) ) = 0 )
180 178 179 syl ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ( 0 ↑ ( ♯ ‘ 𝑋 ) ) = 0 )
181 180 adantr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) ∧ 𝑗 ∈ ( ℕ ∖ { 1 } ) ) → ( 0 ↑ ( ♯ ‘ 𝑋 ) ) = 0 )
182 168 172 181 3eqtrd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) ∧ 𝑗 ∈ ( ℕ ∖ { 1 } ) ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = 0 )
183 106 107 110 123 182 sge0ss ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ( Σ^ ‘ ( 𝑗 ∈ { 1 } ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
184 96 105 183 3eqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
185 92 184 jca ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
186 nfcv ⊢ Ⅎ 𝑘 𝑖
187 nfcv ⊢ Ⅎ 𝑘 ℕ
188 nfmpt1 ⊢ Ⅎ 𝑘 ( 𝑘 ∈ 𝑋 ↦ if ( 𝑗 = 1 , ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ , ⟨ 0 , 0 ⟩ ) )
189 187 188 nfmpt ⊢ Ⅎ 𝑘 ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ if ( 𝑗 = 1 , ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ , ⟨ 0 , 0 ⟩ ) ) )
190 6 189 nfcxfr ⊢ Ⅎ 𝑘 𝐻
191 186 190 nfeq ⊢ Ⅎ 𝑘 𝑖 = 𝐻
192 fveq1 ⊢ ( 𝑖 = 𝐻 → ( 𝑖 ‘ 𝑗 ) = ( 𝐻 ‘ 𝑗 ) )
193 192 coeq2d ⊢ ( 𝑖 = 𝐻 → ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) = ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) )
194 193 fveq1d ⊢ ( 𝑖 = 𝐻 → ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) )
195 194 adantr ⊢ ( ( 𝑖 = 𝐻 ∧ 𝑘 ∈ 𝑋 ) → ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) )
196 191 195 ixpeq2d ⊢ ( 𝑖 = 𝐻 → X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) )
197 196 iuneq2d ⊢ ( 𝑖 = 𝐻 → ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) )
198 197 sseq2d ⊢ ( 𝑖 = 𝐻 → ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ↔ 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
199 194 fveq2d ⊢ ( 𝑖 = 𝐻 → ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
200 199 a1d ⊢ ( 𝑖 = 𝐻 → ( 𝑘 ∈ 𝑋 → ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) )
201 191 200 ralrimi ⊢ ( 𝑖 = 𝐻 → ∀ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
202 201 prodeq2d ⊢ ( 𝑖 = 𝐻 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
203 202 mpteq2dv ⊢ ( 𝑖 = 𝐻 → ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) = ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) )
204 203 fveq2d ⊢ ( 𝑖 = 𝐻 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
205 204 eqeq2d ⊢ ( 𝑖 = 𝐻 → ( ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ↔ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
206 198 205 anbi12d ⊢ ( 𝑖 = 𝐻 → ( ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ↔ ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
207 206 rspcev ⊢ ( ( 𝐻 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐻 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
208 54 185 207 syl2anc ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
209 33 208 jca ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ( ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℝ* ∧ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
210 eqeq1 ⊢ ( 𝑧 = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) → ( 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ↔ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
211 210 anbi2d ⊢ ( 𝑧 = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) → ( ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ↔ ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
212 211 rexbidv ⊢ ( 𝑧 = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) → ( ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ↔ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
213 212 elrab ⊢ ( ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ↔ ( ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℝ* ∧ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
214 209 213 sylibr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } )
215 5 eqcomi ⊢ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } = 𝑀
216 215 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } = 𝑀 )
217 214 216 eleqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ 𝑀 )
218 infxrlb ⊢ ( ( 𝑀 ⊆ ℝ* ∧ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ 𝑀 ) → inf ( 𝑀 , ℝ* , < ) ≤ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
219 30 217 218 syl2anc ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → inf ( 𝑀 , ℝ* , < ) ≤ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
220 27 219 eqbrtrd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → if ( 𝑋 = ∅ , 0 , inf ( 𝑀 , ℝ* , < ) ) ≤ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
221 25 220 pm2.61dan ⊢ ( 𝜑 → if ( 𝑋 = ∅ , 0 , inf ( 𝑀 , ℝ* , < ) ) ≤ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
222 14 221 eqbrtrd ⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐼 ) ≤ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )