Metamath Proof Explorer


Theorem hoidmv1le

Description: The dimensional volume of a 1-dimensional half-open interval is less than or equal to the generalized sum of the dimensional volumes of countable half-open intervals that cover it. This is one of the two base cases of the induction of Lemma 115B of Fremlin1 p. 29 (the other base case is the 0-dimensional case). This proof of the 1-dimensional case is given in Lemma 114B of Fremlin1 p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses hoidmv1le.l 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘𝑥 ( vol ‘ ( ( 𝑎𝑘 ) [,) ( 𝑏𝑘 ) ) ) ) ) )
hoidmv1le.z ( 𝜑𝑍𝑉 )
hoidmv1le.x 𝑋 = { 𝑍 }
hoidmv1le.a ( 𝜑𝐴 : 𝑋 ⟶ ℝ )
hoidmv1le.b ( 𝜑𝐵 : 𝑋 ⟶ ℝ )
hoidmv1le.c ( 𝜑𝐶 : ℕ ⟶ ( ℝ ↑m 𝑋 ) )
hoidmv1le.d ( 𝜑𝐷 : ℕ ⟶ ( ℝ ↑m 𝑋 ) )
hoidmv1le.s ( 𝜑X 𝑘𝑋 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
Assertion hoidmv1le ( 𝜑 → ( 𝐴 ( 𝐿𝑋 ) 𝐵 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑋 ) ( 𝐷𝑗 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 hoidmv1le.l 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘𝑥 ( vol ‘ ( ( 𝑎𝑘 ) [,) ( 𝑏𝑘 ) ) ) ) ) )
2 hoidmv1le.z ( 𝜑𝑍𝑉 )
3 hoidmv1le.x 𝑋 = { 𝑍 }
4 hoidmv1le.a ( 𝜑𝐴 : 𝑋 ⟶ ℝ )
5 hoidmv1le.b ( 𝜑𝐵 : 𝑋 ⟶ ℝ )
6 hoidmv1le.c ( 𝜑𝐶 : ℕ ⟶ ( ℝ ↑m 𝑋 ) )
7 hoidmv1le.d ( 𝜑𝐷 : ℕ ⟶ ( ℝ ↑m 𝑋 ) )
8 hoidmv1le.s ( 𝜑X 𝑘𝑋 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
9 snidg ( 𝑍𝑉𝑍 ∈ { 𝑍 } )
10 2 9 syl ( 𝜑𝑍 ∈ { 𝑍 } )
11 10 3 eleqtrrdi ( 𝜑𝑍𝑋 )
12 5 11 ffvelrnd ( 𝜑 → ( 𝐵𝑍 ) ∈ ℝ )
13 4 11 ffvelrnd ( 𝜑 → ( 𝐴𝑍 ) ∈ ℝ )
14 12 13 resubcld ( 𝜑 → ( ( 𝐵𝑍 ) − ( 𝐴𝑍 ) ) ∈ ℝ )
15 14 rexrd ( 𝜑 → ( ( 𝐵𝑍 ) − ( 𝐴𝑍 ) ) ∈ ℝ* )
16 pnfxr +∞ ∈ ℝ*
17 16 a1i ( 𝜑 → +∞ ∈ ℝ* )
18 14 ltpnfd ( 𝜑 → ( ( 𝐵𝑍 ) − ( 𝐴𝑍 ) ) < +∞ )
19 15 17 18 xrltled ( 𝜑 → ( ( 𝐵𝑍 ) − ( 𝐴𝑍 ) ) ≤ +∞ )
20 19 ad2antrr ( ( ( 𝜑 ∧ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) = +∞ ) → ( ( 𝐵𝑍 ) − ( 𝐴𝑍 ) ) ≤ +∞ )
21 id ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) = +∞ → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) = +∞ )
22 21 eqcomd ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) = +∞ → +∞ = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) )
23 22 adantl ( ( ( 𝜑 ∧ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) = +∞ ) → +∞ = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) )
24 20 23 breqtrd ( ( ( 𝜑 ∧ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) = +∞ ) → ( ( 𝐵𝑍 ) − ( 𝐴𝑍 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) )
25 simpl ( ( ( 𝜑 ∧ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) ∧ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) = +∞ ) → ( 𝜑 ∧ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) )
26 simpr ( ( ( 𝜑 ∧ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) ∧ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) = +∞ ) → ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) = +∞ )
27 nnex ℕ ∈ V
28 27 a1i ( ( ( 𝜑 ∧ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) ∧ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) = +∞ ) → ℕ ∈ V )
29 3 a1i ( 𝜑𝑋 = { 𝑍 } )
30 snfi { 𝑍 } ∈ Fin
31 30 a1i ( 𝜑 → { 𝑍 } ∈ Fin )
32 29 31 eqeltrd ( 𝜑𝑋 ∈ Fin )
33 32 adantr ( ( 𝜑𝑗 ∈ ℕ ) → 𝑋 ∈ Fin )
34 11 ne0d ( 𝜑𝑋 ≠ ∅ )
35 34 adantr ( ( 𝜑𝑗 ∈ ℕ ) → 𝑋 ≠ ∅ )
36 6 ffvelrnda ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐶𝑗 ) ∈ ( ℝ ↑m 𝑋 ) )
37 elmapi ( ( 𝐶𝑗 ) ∈ ( ℝ ↑m 𝑋 ) → ( 𝐶𝑗 ) : 𝑋 ⟶ ℝ )
38 36 37 syl ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐶𝑗 ) : 𝑋 ⟶ ℝ )
39 7 ffvelrnda ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐷𝑗 ) ∈ ( ℝ ↑m 𝑋 ) )
40 elmapi ( ( 𝐷𝑗 ) ∈ ( ℝ ↑m 𝑋 ) → ( 𝐷𝑗 ) : 𝑋 ⟶ ℝ )
41 39 40 syl ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐷𝑗 ) : 𝑋 ⟶ ℝ )
42 1 33 35 38 41 hoidmvn0val ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐶𝑗 ) ( 𝐿𝑋 ) ( 𝐷𝑗 ) ) = ∏ 𝑘𝑋 ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) )
43 3 prodeq1i 𝑘𝑋 ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ { 𝑍 } ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
44 43 a1i ( ( 𝜑𝑗 ∈ ℕ ) → ∏ 𝑘𝑋 ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ { 𝑍 } ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) )
45 2 adantr ( ( 𝜑𝑗 ∈ ℕ ) → 𝑍𝑉 )
46 11 adantr ( ( 𝜑𝑗 ∈ ℕ ) → 𝑍𝑋 )
47 38 46 ffvelrnd ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐶𝑗 ) ‘ 𝑍 ) ∈ ℝ )
48 41 46 ffvelrnd ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐷𝑗 ) ‘ 𝑍 ) ∈ ℝ )
49 volicore ( ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) ∈ ℝ ∧ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ∈ ℝ ) → ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ∈ ℝ )
50 47 48 49 syl2anc ( ( 𝜑𝑗 ∈ ℕ ) → ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ∈ ℝ )
51 50 recnd ( ( 𝜑𝑗 ∈ ℕ ) → ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ∈ ℂ )
52 fveq2 ( 𝑘 = 𝑍 → ( ( 𝐶𝑗 ) ‘ 𝑘 ) = ( ( 𝐶𝑗 ) ‘ 𝑍 ) )
53 fveq2 ( 𝑘 = 𝑍 → ( ( 𝐷𝑗 ) ‘ 𝑘 ) = ( ( 𝐷𝑗 ) ‘ 𝑍 ) )
54 52 53 oveq12d ( 𝑘 = 𝑍 → ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) = ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
55 54 fveq2d ( 𝑘 = 𝑍 → ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) = ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) )
56 55 prodsn ( ( 𝑍𝑉 ∧ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ∈ ℂ ) → ∏ 𝑘 ∈ { 𝑍 } ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) = ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) )
57 45 51 56 syl2anc ( ( 𝜑𝑗 ∈ ℕ ) → ∏ 𝑘 ∈ { 𝑍 } ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) = ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) )
58 42 44 57 3eqtrd ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐶𝑗 ) ( 𝐿𝑋 ) ( 𝐷𝑗 ) ) = ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) )
59 58 mpteq2dva ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑋 ) ( 𝐷𝑗 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) )
60 fveq2 ( 𝑘 = 𝑙 → ( 𝑎𝑘 ) = ( 𝑎𝑙 ) )
61 fveq2 ( 𝑘 = 𝑙 → ( 𝑏𝑘 ) = ( 𝑏𝑙 ) )
62 60 61 oveq12d ( 𝑘 = 𝑙 → ( ( 𝑎𝑘 ) [,) ( 𝑏𝑘 ) ) = ( ( 𝑎𝑙 ) [,) ( 𝑏𝑙 ) ) )
63 62 fveq2d ( 𝑘 = 𝑙 → ( vol ‘ ( ( 𝑎𝑘 ) [,) ( 𝑏𝑘 ) ) ) = ( vol ‘ ( ( 𝑎𝑙 ) [,) ( 𝑏𝑙 ) ) ) )
64 63 cbvprodv 𝑘𝑥 ( vol ‘ ( ( 𝑎𝑘 ) [,) ( 𝑏𝑘 ) ) ) = ∏ 𝑙𝑥 ( vol ‘ ( ( 𝑎𝑙 ) [,) ( 𝑏𝑙 ) ) )
65 ifeq2 ( ∏ 𝑘𝑥 ( vol ‘ ( ( 𝑎𝑘 ) [,) ( 𝑏𝑘 ) ) ) = ∏ 𝑙𝑥 ( vol ‘ ( ( 𝑎𝑙 ) [,) ( 𝑏𝑙 ) ) ) → if ( 𝑥 = ∅ , 0 , ∏ 𝑘𝑥 ( vol ‘ ( ( 𝑎𝑘 ) [,) ( 𝑏𝑘 ) ) ) ) = if ( 𝑥 = ∅ , 0 , ∏ 𝑙𝑥 ( vol ‘ ( ( 𝑎𝑙 ) [,) ( 𝑏𝑙 ) ) ) ) )
66 64 65 ax-mp if ( 𝑥 = ∅ , 0 , ∏ 𝑘𝑥 ( vol ‘ ( ( 𝑎𝑘 ) [,) ( 𝑏𝑘 ) ) ) ) = if ( 𝑥 = ∅ , 0 , ∏ 𝑙𝑥 ( vol ‘ ( ( 𝑎𝑙 ) [,) ( 𝑏𝑙 ) ) ) )
67 66 a1i ( ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) ∧ 𝑏 ∈ ( ℝ ↑m 𝑥 ) ) → if ( 𝑥 = ∅ , 0 , ∏ 𝑘𝑥 ( vol ‘ ( ( 𝑎𝑘 ) [,) ( 𝑏𝑘 ) ) ) ) = if ( 𝑥 = ∅ , 0 , ∏ 𝑙𝑥 ( vol ‘ ( ( 𝑎𝑙 ) [,) ( 𝑏𝑙 ) ) ) ) )
68 67 mpoeq3ia ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘𝑥 ( vol ‘ ( ( 𝑎𝑘 ) [,) ( 𝑏𝑘 ) ) ) ) ) = ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑙𝑥 ( vol ‘ ( ( 𝑎𝑙 ) [,) ( 𝑏𝑙 ) ) ) ) )
69 68 mpteq2i ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘𝑥 ( vol ‘ ( ( 𝑎𝑘 ) [,) ( 𝑏𝑘 ) ) ) ) ) ) = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑙𝑥 ( vol ‘ ( ( 𝑎𝑙 ) [,) ( 𝑏𝑙 ) ) ) ) ) )
70 1 69 eqtri 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑙𝑥 ( vol ‘ ( ( 𝑎𝑙 ) [,) ( 𝑏𝑙 ) ) ) ) ) )
71 70 33 38 41 hoidmvcl ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐶𝑗 ) ( 𝐿𝑋 ) ( 𝐷𝑗 ) ) ∈ ( 0 [,) +∞ ) )
72 eqid ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑋 ) ( 𝐷𝑗 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑋 ) ( 𝐷𝑗 ) ) )
73 71 72 fmptd ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑋 ) ( 𝐷𝑗 ) ) ) : ℕ ⟶ ( 0 [,) +∞ ) )
74 icossicc ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
75 74 a1i ( 𝜑 → ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) )
76 73 75 fssd ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑋 ) ( 𝐷𝑗 ) ) ) : ℕ ⟶ ( 0 [,] +∞ ) )
77 59 76 feq1dd ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) : ℕ ⟶ ( 0 [,] +∞ ) )
78 77 ad2antrr ( ( ( 𝜑 ∧ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) ∧ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) = +∞ ) → ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) : ℕ ⟶ ( 0 [,] +∞ ) )
79 28 78 sge0repnf ( ( ( 𝜑 ∧ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) ∧ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) = +∞ ) → ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) ∈ ℝ ↔ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) = +∞ ) )
80 26 79 mpbird ( ( ( 𝜑 ∧ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) ∧ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) = +∞ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) ∈ ℝ )
81 13 ad2antrr ( ( ( 𝜑 ∧ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) ∈ ℝ ) → ( 𝐴𝑍 ) ∈ ℝ )
82 12 ad2antrr ( ( ( 𝜑 ∧ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) ∈ ℝ ) → ( 𝐵𝑍 ) ∈ ℝ )
83 simplr ( ( ( 𝜑 ∧ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) ∈ ℝ ) → ( 𝐴𝑍 ) < ( 𝐵𝑍 ) )
84 eqid ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ‘ 𝑍 ) )
85 47 84 fmptd ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) : ℕ ⟶ ℝ )
86 85 ad2antrr ( ( ( 𝜑 ∧ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) ∈ ℝ ) → ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) : ℕ ⟶ ℝ )
87 eqid ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) )
88 48 87 fmptd ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) : ℕ ⟶ ℝ )
89 88 ad2antrr ( ( ( 𝜑 ∧ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) ∈ ℝ ) → ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) : ℕ ⟶ ℝ )
90 3 eleq2i ( 𝑘𝑋𝑘 ∈ { 𝑍 } )
91 90 biimpi ( 𝑘𝑋𝑘 ∈ { 𝑍 } )
92 elsni ( 𝑘 ∈ { 𝑍 } → 𝑘 = 𝑍 )
93 91 92 syl ( 𝑘𝑋𝑘 = 𝑍 )
94 93 54 syl ( 𝑘𝑋 → ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) = ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
95 94 rgen 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) = ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) )
96 ixpeq2 ( ∀ 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) = ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) → X 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) = X 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
97 95 96 ax-mp X 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) = X 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) )
98 97 a1i ( 𝑗 ∈ ℕ → X 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) = X 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
99 98 iuneq2i 𝑗 ∈ ℕ X 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) = 𝑗 ∈ ℕ X 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) )
100 99 a1i ( 𝜑 𝑗 ∈ ℕ X 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) = 𝑗 ∈ ℕ X 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
101 8 100 sseqtrd ( 𝜑X 𝑘𝑋 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
102 101 adantr ( ( 𝜑𝑥 ∈ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ) → X 𝑘𝑋 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
103 id ( 𝑥 ∈ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) → 𝑥 ∈ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) )
104 eqidd ( 𝑥 ∈ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) → { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑥 ⟩ } )
105 opeq2 ( 𝑦 = 𝑥 → ⟨ 𝑍 , 𝑦 ⟩ = ⟨ 𝑍 , 𝑥 ⟩ )
106 105 sneqd ( 𝑦 = 𝑥 → { ⟨ 𝑍 , 𝑦 ⟩ } = { ⟨ 𝑍 , 𝑥 ⟩ } )
107 106 rspceeqv ( ( 𝑥 ∈ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ∧ { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑥 ⟩ } ) → ∃ 𝑦 ∈ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } )
108 103 104 107 syl2anc ( 𝑥 ∈ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) → ∃ 𝑦 ∈ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } )
109 108 adantl ( ( 𝜑𝑥 ∈ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ) → ∃ 𝑦 ∈ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } )
110 elixpsn ( 𝑍𝑉 → ( { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘 ∈ { 𝑍 } ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ↔ ∃ 𝑦 ∈ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } ) )
111 2 110 syl ( 𝜑 → ( { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘 ∈ { 𝑍 } ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ↔ ∃ 𝑦 ∈ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } ) )
112 111 adantr ( ( 𝜑𝑥 ∈ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ) → ( { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘 ∈ { 𝑍 } ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ↔ ∃ 𝑦 ∈ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } ) )
113 109 112 mpbird ( ( 𝜑𝑥 ∈ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ) → { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘 ∈ { 𝑍 } ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) )
114 3 eqcomi { 𝑍 } = 𝑋
115 ixpeq1 ( { 𝑍 } = 𝑋X 𝑘 ∈ { 𝑍 } ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) = X 𝑘𝑋 ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) )
116 114 115 ax-mp X 𝑘 ∈ { 𝑍 } ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) = X 𝑘𝑋 ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) )
117 fveq2 ( 𝑘 = 𝑍 → ( 𝐴𝑘 ) = ( 𝐴𝑍 ) )
118 93 117 syl ( 𝑘𝑋 → ( 𝐴𝑘 ) = ( 𝐴𝑍 ) )
119 fveq2 ( 𝑘 = 𝑍 → ( 𝐵𝑘 ) = ( 𝐵𝑍 ) )
120 93 119 syl ( 𝑘𝑋 → ( 𝐵𝑘 ) = ( 𝐵𝑍 ) )
121 118 120 oveq12d ( 𝑘𝑋 → ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) = ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) )
122 121 eqcomd ( 𝑘𝑋 → ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) = ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
123 122 rgen 𝑘𝑋 ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) = ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) )
124 ixpeq2 ( ∀ 𝑘𝑋 ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) = ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) → X 𝑘𝑋 ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) = X 𝑘𝑋 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
125 123 124 ax-mp X 𝑘𝑋 ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) = X 𝑘𝑋 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) )
126 116 125 eqtri X 𝑘 ∈ { 𝑍 } ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) = X 𝑘𝑋 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) )
127 126 a1i ( 𝜑X 𝑘 ∈ { 𝑍 } ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) = X 𝑘𝑋 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
128 127 adantr ( ( 𝜑𝑥 ∈ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ) → X 𝑘 ∈ { 𝑍 } ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) = X 𝑘𝑋 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
129 113 128 eleqtrd ( ( 𝜑𝑥 ∈ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ) → { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘𝑋 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
130 102 129 sseldd ( ( 𝜑𝑥 ∈ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ) → { ⟨ 𝑍 , 𝑥 ⟩ } ∈ 𝑗 ∈ ℕ X 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
131 eliun ( { ⟨ 𝑍 , 𝑥 ⟩ } ∈ 𝑗 ∈ ℕ X 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ↔ ∃ 𝑗 ∈ ℕ { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
132 130 131 sylib ( ( 𝜑𝑥 ∈ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ) → ∃ 𝑗 ∈ ℕ { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
133 ixpeq1 ( 𝑋 = { 𝑍 } → X 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) = X 𝑘 ∈ { 𝑍 } ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
134 3 133 ax-mp X 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) = X 𝑘 ∈ { 𝑍 } ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) )
135 134 eleq2i ( { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ↔ { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘 ∈ { 𝑍 } ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
136 135 biimpi ( { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) → { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘 ∈ { 𝑍 } ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
137 136 adantl ( ( 𝜑 ∧ { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘 ∈ { 𝑍 } ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
138 elixpsn ( 𝑍𝑉 → ( { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘 ∈ { 𝑍 } ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ↔ ∃ 𝑦 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } ) )
139 2 138 syl ( 𝜑 → ( { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘 ∈ { 𝑍 } ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ↔ ∃ 𝑦 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } ) )
140 139 adantr ( ( 𝜑 ∧ { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘 ∈ { 𝑍 } ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ↔ ∃ 𝑦 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } ) )
141 137 140 mpbid ( ( 𝜑 ∧ { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ∃ 𝑦 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } )
142 opex 𝑍 , 𝑥 ⟩ ∈ V
143 142 sneqr ( { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } → ⟨ 𝑍 , 𝑥 ⟩ = ⟨ 𝑍 , 𝑦 ⟩ )
144 143 adantl ( ( 𝜑 ∧ { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } ) → ⟨ 𝑍 , 𝑥 ⟩ = ⟨ 𝑍 , 𝑦 ⟩ )
145 vex 𝑥 ∈ V
146 145 a1i ( 𝜑𝑥 ∈ V )
147 opthg ( ( 𝑍𝑉𝑥 ∈ V ) → ( ⟨ 𝑍 , 𝑥 ⟩ = ⟨ 𝑍 , 𝑦 ⟩ ↔ ( 𝑍 = 𝑍𝑥 = 𝑦 ) ) )
148 2 146 147 syl2anc ( 𝜑 → ( ⟨ 𝑍 , 𝑥 ⟩ = ⟨ 𝑍 , 𝑦 ⟩ ↔ ( 𝑍 = 𝑍𝑥 = 𝑦 ) ) )
149 148 adantr ( ( 𝜑 ∧ { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } ) → ( ⟨ 𝑍 , 𝑥 ⟩ = ⟨ 𝑍 , 𝑦 ⟩ ↔ ( 𝑍 = 𝑍𝑥 = 𝑦 ) ) )
150 144 149 mpbid ( ( 𝜑 ∧ { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } ) → ( 𝑍 = 𝑍𝑥 = 𝑦 ) )
151 150 simprd ( ( 𝜑 ∧ { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } ) → 𝑥 = 𝑦 )
152 151 3adant2 ( ( 𝜑𝑦 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ∧ { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } ) → 𝑥 = 𝑦 )
153 simp2 ( ( 𝜑𝑦 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ∧ { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } ) → 𝑦 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
154 152 153 eqeltrd ( ( 𝜑𝑦 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ∧ { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } ) → 𝑥 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
155 154 3exp ( 𝜑 → ( 𝑦 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) → ( { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } → 𝑥 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) )
156 155 adantr ( ( 𝜑 ∧ { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( 𝑦 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) → ( { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } → 𝑥 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) )
157 156 rexlimdv ( ( 𝜑 ∧ { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( ∃ 𝑦 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } → 𝑥 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) )
158 141 157 mpd ( ( 𝜑 ∧ { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → 𝑥 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
159 158 ex ( 𝜑 → ( { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) → 𝑥 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) )
160 159 ad2antrr ( ( ( 𝜑𝑥 ∈ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ) ∧ 𝑗 ∈ ℕ ) → ( { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) → 𝑥 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) )
161 160 reximdva ( ( 𝜑𝑥 ∈ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ) → ( ∃ 𝑗 ∈ ℕ { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘𝑋 ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) → ∃ 𝑗 ∈ ℕ 𝑥 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) )
162 132 161 mpd ( ( 𝜑𝑥 ∈ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ) → ∃ 𝑗 ∈ ℕ 𝑥 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
163 eliun ( 𝑥 𝑗 ∈ ℕ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ↔ ∃ 𝑗 ∈ ℕ 𝑥 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
164 162 163 sylibr ( ( 𝜑𝑥 ∈ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ) → 𝑥 𝑗 ∈ ℕ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
165 164 ralrimiva ( 𝜑 → ∀ 𝑥 ∈ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) 𝑥 𝑗 ∈ ℕ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
166 dfss3 ( ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ⊆ 𝑗 ∈ ℕ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ↔ ∀ 𝑥 ∈ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) 𝑥 𝑗 ∈ ℕ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
167 165 166 sylibr ( 𝜑 → ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ⊆ 𝑗 ∈ ℕ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
168 eqidd ( ( 𝜑𝑖 ∈ ℕ ) → ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) )
169 fveq2 ( 𝑗 = 𝑖 → ( 𝐶𝑗 ) = ( 𝐶𝑖 ) )
170 169 fveq1d ( 𝑗 = 𝑖 → ( ( 𝐶𝑗 ) ‘ 𝑍 ) = ( ( 𝐶𝑖 ) ‘ 𝑍 ) )
171 170 adantl ( ( ( 𝜑𝑖 ∈ ℕ ) ∧ 𝑗 = 𝑖 ) → ( ( 𝐶𝑗 ) ‘ 𝑍 ) = ( ( 𝐶𝑖 ) ‘ 𝑍 ) )
172 simpr ( ( 𝜑𝑖 ∈ ℕ ) → 𝑖 ∈ ℕ )
173 fvexd ( ( 𝜑𝑖 ∈ ℕ ) → ( ( 𝐶𝑖 ) ‘ 𝑍 ) ∈ V )
174 168 171 172 173 fvmptd ( ( 𝜑𝑖 ∈ ℕ ) → ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) = ( ( 𝐶𝑖 ) ‘ 𝑍 ) )
175 eqidd ( ( 𝜑𝑖 ∈ ℕ ) → ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
176 fveq2 ( 𝑗 = 𝑖 → ( 𝐷𝑗 ) = ( 𝐷𝑖 ) )
177 176 fveq1d ( 𝑗 = 𝑖 → ( ( 𝐷𝑗 ) ‘ 𝑍 ) = ( ( 𝐷𝑖 ) ‘ 𝑍 ) )
178 177 adantl ( ( ( 𝜑𝑖 ∈ ℕ ) ∧ 𝑗 = 𝑖 ) → ( ( 𝐷𝑗 ) ‘ 𝑍 ) = ( ( 𝐷𝑖 ) ‘ 𝑍 ) )
179 fvexd ( ( 𝜑𝑖 ∈ ℕ ) → ( ( 𝐷𝑖 ) ‘ 𝑍 ) ∈ V )
180 175 178 172 179 fvmptd ( ( 𝜑𝑖 ∈ ℕ ) → ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) = ( ( 𝐷𝑖 ) ‘ 𝑍 ) )
181 174 180 oveq12d ( ( 𝜑𝑖 ∈ ℕ ) → ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ) = ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) )
182 181 iuneq2dv ( 𝜑 𝑖 ∈ ℕ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ) = 𝑖 ∈ ℕ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) )
183 170 177 oveq12d ( 𝑗 = 𝑖 → ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) = ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) )
184 183 cbviunv 𝑗 ∈ ℕ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) = 𝑖 ∈ ℕ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) )
185 184 eqcomi 𝑖 ∈ ℕ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) = 𝑗 ∈ ℕ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) )
186 185 a1i ( 𝜑 𝑖 ∈ ℕ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) = 𝑗 ∈ ℕ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
187 182 186 eqtr2d ( 𝜑 𝑗 ∈ ℕ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) = 𝑖 ∈ ℕ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ) )
188 167 187 sseqtrd ( 𝜑 → ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ⊆ 𝑖 ∈ ℕ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ) )
189 188 ad2antrr ( ( ( 𝜑 ∧ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) ∈ ℝ ) → ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ⊆ 𝑖 ∈ ℕ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ) )
190 fvex ( ( 𝐶𝑖 ) ‘ 𝑍 ) ∈ V
191 170 84 190 fvmpt ( 𝑖 ∈ ℕ → ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) = ( ( 𝐶𝑖 ) ‘ 𝑍 ) )
192 fvex ( ( 𝐷𝑖 ) ‘ 𝑍 ) ∈ V
193 177 87 192 fvmpt ( 𝑖 ∈ ℕ → ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) = ( ( 𝐷𝑖 ) ‘ 𝑍 ) )
194 191 193 oveq12d ( 𝑖 ∈ ℕ → ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ) = ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) )
195 194 fveq2d ( 𝑖 ∈ ℕ → ( vol ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ) ) = ( vol ‘ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) ) )
196 195 mpteq2ia ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ) ) ) = ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) ) )
197 eqcom ( 𝑗 = 𝑖𝑖 = 𝑗 )
198 197 imbi1i ( ( 𝑗 = 𝑖 → ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) = ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) ) ↔ ( 𝑖 = 𝑗 → ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) = ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) ) )
199 eqcom ( ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) = ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) ↔ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) = ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
200 199 imbi2i ( ( 𝑖 = 𝑗 → ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) = ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) ) ↔ ( 𝑖 = 𝑗 → ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) = ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) )
201 198 200 bitri ( ( 𝑗 = 𝑖 → ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) = ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) ) ↔ ( 𝑖 = 𝑗 → ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) = ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) )
202 183 201 mpbi ( 𝑖 = 𝑗 → ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) = ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
203 202 fveq2d ( 𝑖 = 𝑗 → ( vol ‘ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) ) = ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) )
204 203 cbvmptv ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) )
205 196 204 eqtri ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) )
206 205 fveq2i ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) )
207 206 a1i ( ( ( 𝜑 ∧ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) ∈ ℝ ) → ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) )
208 simpr ( ( ( 𝜑 ∧ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) ∈ ℝ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) ∈ ℝ )
209 207 208 eqeltrd ( ( ( 𝜑 ∧ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) ∈ ℝ ) → ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ) ) ) ) ∈ ℝ )
210 oveq1 ( 𝑤 = 𝑧 → ( 𝑤 − ( 𝐴𝑍 ) ) = ( 𝑧 − ( 𝐴𝑍 ) ) )
211 193 breq1d ( 𝑖 ∈ ℕ → ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ≤ 𝑧 ↔ ( ( 𝐷𝑖 ) ‘ 𝑍 ) ≤ 𝑧 ) )
212 211 193 ifbieq1d ( 𝑖 ∈ ℕ → if ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ≤ 𝑧 , ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) , 𝑧 ) = if ( ( ( 𝐷𝑖 ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷𝑖 ) ‘ 𝑍 ) , 𝑧 ) )
213 191 212 oveq12d ( 𝑖 ∈ ℕ → ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) if ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ≤ 𝑧 , ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) , 𝑧 ) ) = ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) if ( ( ( 𝐷𝑖 ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷𝑖 ) ‘ 𝑍 ) , 𝑧 ) ) )
214 213 fveq2d ( 𝑖 ∈ ℕ → ( vol ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) if ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ≤ 𝑧 , ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) , 𝑧 ) ) ) = ( vol ‘ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) if ( ( ( 𝐷𝑖 ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷𝑖 ) ‘ 𝑍 ) , 𝑧 ) ) ) )
215 214 mpteq2ia ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) if ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ≤ 𝑧 , ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) , 𝑧 ) ) ) ) = ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) if ( ( ( 𝐷𝑖 ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷𝑖 ) ‘ 𝑍 ) , 𝑧 ) ) ) )
216 fveq2 ( 𝑖 = → ( 𝐶𝑖 ) = ( 𝐶 ) )
217 216 fveq1d ( 𝑖 = → ( ( 𝐶𝑖 ) ‘ 𝑍 ) = ( ( 𝐶 ) ‘ 𝑍 ) )
218 fveq2 ( 𝑖 = → ( 𝐷𝑖 ) = ( 𝐷 ) )
219 218 fveq1d ( 𝑖 = → ( ( 𝐷𝑖 ) ‘ 𝑍 ) = ( ( 𝐷 ) ‘ 𝑍 ) )
220 219 breq1d ( 𝑖 = → ( ( ( 𝐷𝑖 ) ‘ 𝑍 ) ≤ 𝑧 ↔ ( ( 𝐷 ) ‘ 𝑍 ) ≤ 𝑧 ) )
221 220 219 ifbieq1d ( 𝑖 = → if ( ( ( 𝐷𝑖 ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷𝑖 ) ‘ 𝑍 ) , 𝑧 ) = if ( ( ( 𝐷 ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷 ) ‘ 𝑍 ) , 𝑧 ) )
222 217 221 oveq12d ( 𝑖 = → ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) if ( ( ( 𝐷𝑖 ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷𝑖 ) ‘ 𝑍 ) , 𝑧 ) ) = ( ( ( 𝐶 ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷 ) ‘ 𝑍 ) , 𝑧 ) ) )
223 222 fveq2d ( 𝑖 = → ( vol ‘ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) if ( ( ( 𝐷𝑖 ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷𝑖 ) ‘ 𝑍 ) , 𝑧 ) ) ) = ( vol ‘ ( ( ( 𝐶 ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷 ) ‘ 𝑍 ) , 𝑧 ) ) ) )
224 223 cbvmptv ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) if ( ( ( 𝐷𝑖 ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷𝑖 ) ‘ 𝑍 ) , 𝑧 ) ) ) ) = ( ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷 ) ‘ 𝑍 ) , 𝑧 ) ) ) )
225 215 224 eqtri ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) if ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ≤ 𝑧 , ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) , 𝑧 ) ) ) ) = ( ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷 ) ‘ 𝑍 ) , 𝑧 ) ) ) )
226 225 a1i ( 𝑤 = 𝑧 → ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) if ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ≤ 𝑧 , ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) , 𝑧 ) ) ) ) = ( ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷 ) ‘ 𝑍 ) , 𝑧 ) ) ) ) )
227 breq2 ( 𝑤 = 𝑧 → ( ( ( 𝐷 ) ‘ 𝑍 ) ≤ 𝑤 ↔ ( ( 𝐷 ) ‘ 𝑍 ) ≤ 𝑧 ) )
228 id ( 𝑤 = 𝑧𝑤 = 𝑧 )
229 227 228 ifbieq2d ( 𝑤 = 𝑧 → if ( ( ( 𝐷 ) ‘ 𝑍 ) ≤ 𝑤 , ( ( 𝐷 ) ‘ 𝑍 ) , 𝑤 ) = if ( ( ( 𝐷 ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷 ) ‘ 𝑍 ) , 𝑧 ) )
230 229 eqcomd ( 𝑤 = 𝑧 → if ( ( ( 𝐷 ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷 ) ‘ 𝑍 ) , 𝑧 ) = if ( ( ( 𝐷 ) ‘ 𝑍 ) ≤ 𝑤 , ( ( 𝐷 ) ‘ 𝑍 ) , 𝑤 ) )
231 230 oveq2d ( 𝑤 = 𝑧 → ( ( ( 𝐶 ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷 ) ‘ 𝑍 ) , 𝑧 ) ) = ( ( ( 𝐶 ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ) ‘ 𝑍 ) ≤ 𝑤 , ( ( 𝐷 ) ‘ 𝑍 ) , 𝑤 ) ) )
232 231 fveq2d ( 𝑤 = 𝑧 → ( vol ‘ ( ( ( 𝐶 ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷 ) ‘ 𝑍 ) , 𝑧 ) ) ) = ( vol ‘ ( ( ( 𝐶 ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ) ‘ 𝑍 ) ≤ 𝑤 , ( ( 𝐷 ) ‘ 𝑍 ) , 𝑤 ) ) ) )
233 232 mpteq2dv ( 𝑤 = 𝑧 → ( ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷 ) ‘ 𝑍 ) , 𝑧 ) ) ) ) = ( ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ) ‘ 𝑍 ) ≤ 𝑤 , ( ( 𝐷 ) ‘ 𝑍 ) , 𝑤 ) ) ) ) )
234 226 233 eqtr2d ( 𝑤 = 𝑧 → ( ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ) ‘ 𝑍 ) ≤ 𝑤 , ( ( 𝐷 ) ‘ 𝑍 ) , 𝑤 ) ) ) ) = ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) if ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ≤ 𝑧 , ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) , 𝑧 ) ) ) ) )
235 234 fveq2d ( 𝑤 = 𝑧 → ( Σ^ ‘ ( ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ) ‘ 𝑍 ) ≤ 𝑤 , ( ( 𝐷 ) ‘ 𝑍 ) , 𝑤 ) ) ) ) ) = ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) if ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ≤ 𝑧 , ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) , 𝑧 ) ) ) ) ) )
236 210 235 breq12d ( 𝑤 = 𝑧 → ( ( 𝑤 − ( 𝐴𝑍 ) ) ≤ ( Σ^ ‘ ( ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ) ‘ 𝑍 ) ≤ 𝑤 , ( ( 𝐷 ) ‘ 𝑍 ) , 𝑤 ) ) ) ) ) ↔ ( 𝑧 − ( 𝐴𝑍 ) ) ≤ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) if ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ≤ 𝑧 , ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) , 𝑧 ) ) ) ) ) ) )
237 236 cbvrabv { 𝑤 ∈ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) ∣ ( 𝑤 − ( 𝐴𝑍 ) ) ≤ ( Σ^ ‘ ( ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ) ‘ 𝑍 ) ≤ 𝑤 , ( ( 𝐷 ) ‘ 𝑍 ) , 𝑤 ) ) ) ) ) } = { 𝑧 ∈ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) ∣ ( 𝑧 − ( 𝐴𝑍 ) ) ≤ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) if ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ≤ 𝑧 , ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) , 𝑧 ) ) ) ) ) }
238 eqid sup ( { 𝑤 ∈ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) ∣ ( 𝑤 − ( 𝐴𝑍 ) ) ≤ ( Σ^ ‘ ( ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ) ‘ 𝑍 ) ≤ 𝑤 , ( ( 𝐷 ) ‘ 𝑍 ) , 𝑤 ) ) ) ) ) } , ℝ , < ) = sup ( { 𝑤 ∈ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) ∣ ( 𝑤 − ( 𝐴𝑍 ) ) ≤ ( Σ^ ‘ ( ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ) ‘ 𝑍 ) ≤ 𝑤 , ( ( 𝐷 ) ‘ 𝑍 ) , 𝑤 ) ) ) ) ) } , ℝ , < )
239 81 82 83 86 89 189 209 237 238 hoidmv1lelem3 ( ( ( 𝜑 ∧ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) ∈ ℝ ) → ( ( 𝐵𝑍 ) − ( 𝐴𝑍 ) ) ≤ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ) ) ) ) )
240 239 207 breqtrd ( ( ( 𝜑 ∧ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) ∈ ℝ ) → ( ( 𝐵𝑍 ) − ( 𝐴𝑍 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) )
241 25 80 240 syl2anc ( ( ( 𝜑 ∧ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) ∧ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) = +∞ ) → ( ( 𝐵𝑍 ) − ( 𝐴𝑍 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) )
242 24 241 pm2.61dan ( ( 𝜑 ∧ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) → ( ( 𝐵𝑍 ) − ( 𝐴𝑍 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) )
243 1 32 34 4 5 hoidmvn0val ( 𝜑 → ( 𝐴 ( 𝐿𝑋 ) 𝐵 ) = ∏ 𝑘𝑋 ( vol ‘ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) )
244 29 prodeq1d ( 𝜑 → ∏ 𝑘𝑋 ( vol ‘ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) = ∏ 𝑘 ∈ { 𝑍 } ( vol ‘ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) )
245 volicore ( ( ( 𝐴𝑍 ) ∈ ℝ ∧ ( 𝐵𝑍 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ) ∈ ℝ )
246 13 12 245 syl2anc ( 𝜑 → ( vol ‘ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ) ∈ ℝ )
247 246 recnd ( 𝜑 → ( vol ‘ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ) ∈ ℂ )
248 117 119 oveq12d ( 𝑘 = 𝑍 → ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) = ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) )
249 248 fveq2d ( 𝑘 = 𝑍 → ( vol ‘ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) = ( vol ‘ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ) )
250 249 prodsn ( ( 𝑍𝑉 ∧ ( vol ‘ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ) ∈ ℂ ) → ∏ 𝑘 ∈ { 𝑍 } ( vol ‘ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) = ( vol ‘ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ) )
251 2 247 250 syl2anc ( 𝜑 → ∏ 𝑘 ∈ { 𝑍 } ( vol ‘ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) = ( vol ‘ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ) )
252 243 244 251 3eqtrd ( 𝜑 → ( 𝐴 ( 𝐿𝑋 ) 𝐵 ) = ( vol ‘ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ) )
253 252 adantr ( ( 𝜑 ∧ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) → ( 𝐴 ( 𝐿𝑋 ) 𝐵 ) = ( vol ‘ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ) )
254 volico ( ( ( 𝐴𝑍 ) ∈ ℝ ∧ ( 𝐵𝑍 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ) = if ( ( 𝐴𝑍 ) < ( 𝐵𝑍 ) , ( ( 𝐵𝑍 ) − ( 𝐴𝑍 ) ) , 0 ) )
255 13 12 254 syl2anc ( 𝜑 → ( vol ‘ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ) = if ( ( 𝐴𝑍 ) < ( 𝐵𝑍 ) , ( ( 𝐵𝑍 ) − ( 𝐴𝑍 ) ) , 0 ) )
256 255 adantr ( ( 𝜑 ∧ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) → ( vol ‘ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ) = if ( ( 𝐴𝑍 ) < ( 𝐵𝑍 ) , ( ( 𝐵𝑍 ) − ( 𝐴𝑍 ) ) , 0 ) )
257 iftrue ( ( 𝐴𝑍 ) < ( 𝐵𝑍 ) → if ( ( 𝐴𝑍 ) < ( 𝐵𝑍 ) , ( ( 𝐵𝑍 ) − ( 𝐴𝑍 ) ) , 0 ) = ( ( 𝐵𝑍 ) − ( 𝐴𝑍 ) ) )
258 257 adantl ( ( 𝜑 ∧ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) → if ( ( 𝐴𝑍 ) < ( 𝐵𝑍 ) , ( ( 𝐵𝑍 ) − ( 𝐴𝑍 ) ) , 0 ) = ( ( 𝐵𝑍 ) − ( 𝐴𝑍 ) ) )
259 253 256 258 3eqtrd ( ( 𝜑 ∧ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) → ( 𝐴 ( 𝐿𝑋 ) 𝐵 ) = ( ( 𝐵𝑍 ) − ( 𝐴𝑍 ) ) )
260 59 fveq2d ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑋 ) ( 𝐷𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) )
261 260 adantr ( ( 𝜑 ∧ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑋 ) ( 𝐷𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) )
262 259 261 breq12d ( ( 𝜑 ∧ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) → ( ( 𝐴 ( 𝐿𝑋 ) 𝐵 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑋 ) ( 𝐷𝑗 ) ) ) ) ↔ ( ( 𝐵𝑍 ) − ( 𝐴𝑍 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) ) ) ) )
263 242 262 mpbird ( ( 𝜑 ∧ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) → ( 𝐴 ( 𝐿𝑋 ) 𝐵 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑋 ) ( 𝐷𝑗 ) ) ) ) )
264 243 adantr ( ( 𝜑 ∧ ¬ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) → ( 𝐴 ( 𝐿𝑋 ) 𝐵 ) = ∏ 𝑘𝑋 ( vol ‘ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) )
265 244 adantr ( ( 𝜑 ∧ ¬ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) → ∏ 𝑘𝑋 ( vol ‘ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) = ∏ 𝑘 ∈ { 𝑍 } ( vol ‘ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) )
266 251 adantr ( ( 𝜑 ∧ ¬ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) → ∏ 𝑘 ∈ { 𝑍 } ( vol ‘ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) = ( vol ‘ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ) )
267 255 adantr ( ( 𝜑 ∧ ¬ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) → ( vol ‘ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ) = if ( ( 𝐴𝑍 ) < ( 𝐵𝑍 ) , ( ( 𝐵𝑍 ) − ( 𝐴𝑍 ) ) , 0 ) )
268 iffalse ( ¬ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) → if ( ( 𝐴𝑍 ) < ( 𝐵𝑍 ) , ( ( 𝐵𝑍 ) − ( 𝐴𝑍 ) ) , 0 ) = 0 )
269 268 adantl ( ( 𝜑 ∧ ¬ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) → if ( ( 𝐴𝑍 ) < ( 𝐵𝑍 ) , ( ( 𝐵𝑍 ) − ( 𝐴𝑍 ) ) , 0 ) = 0 )
270 266 267 269 3eqtrd ( ( 𝜑 ∧ ¬ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) → ∏ 𝑘 ∈ { 𝑍 } ( vol ‘ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) = 0 )
271 264 265 270 3eqtrd ( ( 𝜑 ∧ ¬ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) → ( 𝐴 ( 𝐿𝑋 ) 𝐵 ) = 0 )
272 27 a1i ( 𝜑 → ℕ ∈ V )
273 272 76 sge0ge0 ( 𝜑 → 0 ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑋 ) ( 𝐷𝑗 ) ) ) ) )
274 273 adantr ( ( 𝜑 ∧ ¬ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) → 0 ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑋 ) ( 𝐷𝑗 ) ) ) ) )
275 271 274 eqbrtrd ( ( 𝜑 ∧ ¬ ( 𝐴𝑍 ) < ( 𝐵𝑍 ) ) → ( 𝐴 ( 𝐿𝑋 ) 𝐵 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑋 ) ( 𝐷𝑗 ) ) ) ) )
276 263 275 pm2.61dan ( 𝜑 → ( 𝐴 ( 𝐿𝑋 ) 𝐵 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑋 ) ( 𝐷𝑗 ) ) ) ) )