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 ffvelcdmd ⊢ ( 𝜑 → ( 𝐵 ‘ 𝑍 ) ∈ ℝ )
13 4 11 ffvelcdmd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑍 ) ∈ ℝ )
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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑋 ) )
37 elmapi ⊢ ( ( 𝐶 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑋 ) → ( 𝐶 ‘ 𝑗 ) : 𝑋 ⟶ ℝ )
38 36 37 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) : 𝑋 ⟶ ℝ )
39 7 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) ∈ ( ℝ ↑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 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) ∈ ℝ )
48 41 46 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ∈ ℝ )
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 ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )