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 bilani ⊢ ( ( 𝜑 ∧ { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) → { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘 ∈ { 𝑍 } ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) )
137 elixpsn ⊢ ( 𝑍 ∈ 𝑉 → ( { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘 ∈ { 𝑍 } ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ↔ ∃ 𝑦 ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } ) )
138 2 137 syl ⊢ ( 𝜑 → ( { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘 ∈ { 𝑍 } ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ↔ ∃ 𝑦 ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } ) )
139 138 adantr ⊢ ( ( 𝜑 ∧ { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) → ( { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘 ∈ { 𝑍 } ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ↔ ∃ 𝑦 ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } ) )
140 136 139 mpbid ⊢ ( ( 𝜑 ∧ { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) → ∃ 𝑦 ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } )
141 opex ⊢ ⟨ 𝑍 , 𝑥 ⟩ ∈ V
142 141 sneqr ⊢ ( { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } → ⟨ 𝑍 , 𝑥 ⟩ = ⟨ 𝑍 , 𝑦 ⟩ )
143 142 adantl ⊢ ( ( 𝜑 ∧ { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } ) → ⟨ 𝑍 , 𝑥 ⟩ = ⟨ 𝑍 , 𝑦 ⟩ )
144 vex ⊢ 𝑥 ∈ V
145 144 a1i ⊢ ( 𝜑 → 𝑥 ∈ V )
146 opthg ⊢ ( ( 𝑍 ∈ 𝑉 ∧ 𝑥 ∈ V ) → ( ⟨ 𝑍 , 𝑥 ⟩ = ⟨ 𝑍 , 𝑦 ⟩ ↔ ( 𝑍 = 𝑍 ∧ 𝑥 = 𝑦 ) ) )
147 2 145 146 syl2anc ⊢ ( 𝜑 → ( ⟨ 𝑍 , 𝑥 ⟩ = ⟨ 𝑍 , 𝑦 ⟩ ↔ ( 𝑍 = 𝑍 ∧ 𝑥 = 𝑦 ) ) )
148 147 adantr ⊢ ( ( 𝜑 ∧ { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } ) → ( ⟨ 𝑍 , 𝑥 ⟩ = ⟨ 𝑍 , 𝑦 ⟩ ↔ ( 𝑍 = 𝑍 ∧ 𝑥 = 𝑦 ) ) )
149 143 148 mpbid ⊢ ( ( 𝜑 ∧ { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } ) → ( 𝑍 = 𝑍 ∧ 𝑥 = 𝑦 ) )
150 149 simprd ⊢ ( ( 𝜑 ∧ { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } ) → 𝑥 = 𝑦 )
151 150 3adant2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ∧ { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } ) → 𝑥 = 𝑦 )
152 simp2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ∧ { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } ) → 𝑦 ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) )
153 151 152 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ∧ { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } ) → 𝑥 ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) )
154 153 3exp ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) → ( { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } → 𝑥 ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) ) )
155 154 adantr ⊢ ( ( 𝜑 ∧ { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) → ( 𝑦 ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) → ( { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } → 𝑥 ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) ) )
156 155 rexlimdv ⊢ ( ( 𝜑 ∧ { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) → ( ∃ 𝑦 ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) { ⟨ 𝑍 , 𝑥 ⟩ } = { ⟨ 𝑍 , 𝑦 ⟩ } → 𝑥 ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) )
157 140 156 mpd ⊢ ( ( 𝜑 ∧ { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) → 𝑥 ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) )
158 157 ex ⊢ ( 𝜑 → ( { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) → 𝑥 ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) )
159 158 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) ∧ 𝑗 ∈ ℕ ) → ( { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) → 𝑥 ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) )
160 159 reximdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) → ( ∃ 𝑗 ∈ ℕ { ⟨ 𝑍 , 𝑥 ⟩ } ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) → ∃ 𝑗 ∈ ℕ 𝑥 ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) )
161 132 160 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) → ∃ 𝑗 ∈ ℕ 𝑥 ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) )
162 eliun ⊢ ( 𝑥 ∈ ∪ 𝑗 ∈ ℕ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ↔ ∃ 𝑗 ∈ ℕ 𝑥 ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) )
163 161 162 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) → 𝑥 ∈ ∪ 𝑗 ∈ ℕ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) )
164 163 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) 𝑥 ∈ ∪ 𝑗 ∈ ℕ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) )
165 dfss3 ⊢ ( ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ⊆ ∪ 𝑗 ∈ ℕ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ↔ ∀ 𝑥 ∈ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) 𝑥 ∈ ∪ 𝑗 ∈ ℕ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) )
166 164 165 sylibr ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ⊆ ∪ 𝑗 ∈ ℕ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) )
167 eqidd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) ) )
168 fveq2 ⊢ ( 𝑗 = 𝑖 → ( 𝐶 ‘ 𝑗 ) = ( 𝐶 ‘ 𝑖 ) )
169 168 fveq1d ⊢ ( 𝑗 = 𝑖 → ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) = ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) )
170 169 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ 𝑗 = 𝑖 ) → ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) = ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) )
171 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → 𝑖 ∈ ℕ )
172 fvexd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) ∈ V )
173 167 170 171 172 fvmptd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) = ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) )
174 eqidd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) )
175 fveq2 ⊢ ( 𝑗 = 𝑖 → ( 𝐷 ‘ 𝑗 ) = ( 𝐷 ‘ 𝑖 ) )
176 175 fveq1d ⊢ ( 𝑗 = 𝑖 → ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) = ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) )
177 176 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ 𝑗 = 𝑖 ) → ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) = ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) )
178 fvexd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ∈ V )
179 174 177 171 178 fvmptd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) = ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) )
180 173 179 oveq12d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ) = ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) )
181 180 iuneq2dv ⊢ ( 𝜑 → ∪ 𝑖 ∈ ℕ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ) = ∪ 𝑖 ∈ ℕ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) )
182 169 176 oveq12d ⊢ ( 𝑗 = 𝑖 → ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) = ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) )
183 182 cbviunv ⊢ ∪ 𝑗 ∈ ℕ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) = ∪ 𝑖 ∈ ℕ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) )
184 183 eqcomi ⊢ ∪ 𝑖 ∈ ℕ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) = ∪ 𝑗 ∈ ℕ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) )
185 184 a1i ⊢ ( 𝜑 → ∪ 𝑖 ∈ ℕ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) = ∪ 𝑗 ∈ ℕ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) )
186 181 185 eqtr2d ⊢ ( 𝜑 → ∪ 𝑗 ∈ ℕ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) = ∪ 𝑖 ∈ ℕ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ) )
187 166 186 sseqtrd ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ⊆ ∪ 𝑖 ∈ ℕ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ) )
188 187 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) ) ) ∈ ℝ ) → ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ⊆ ∪ 𝑖 ∈ ℕ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ) )
189 fvex ⊢ ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) ∈ V
190 169 84 189 fvmpt ⊢ ( 𝑖 ∈ ℕ → ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) = ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) )
191 fvex ⊢ ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ∈ V
192 176 87 191 fvmpt ⊢ ( 𝑖 ∈ ℕ → ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) = ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) )
193 190 192 oveq12d ⊢ ( 𝑖 ∈ ℕ → ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ) = ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) )
194 193 fveq2d ⊢ ( 𝑖 ∈ ℕ → ( vol ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ) ) = ( vol ‘ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) ) )
195 194 mpteq2ia ⊢ ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ) ) ) = ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) ) )
196 eqcom ⊢ ( 𝑗 = 𝑖 ↔ 𝑖 = 𝑗 )
197 196 imbi1i ⊢ ( ( 𝑗 = 𝑖 → ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) = ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) ) ↔ ( 𝑖 = 𝑗 → ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) = ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) ) )
198 eqcom ⊢ ( ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) = ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) ↔ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) = ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) )
199 198 imbi2i ⊢ ( ( 𝑖 = 𝑗 → ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) = ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) ) ↔ ( 𝑖 = 𝑗 → ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) = ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) )
200 197 199 bitri ⊢ ( ( 𝑗 = 𝑖 → ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) = ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) ) ↔ ( 𝑖 = 𝑗 → ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) = ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) )
201 182 200 mpbi ⊢ ( 𝑖 = 𝑗 → ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) = ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) )
202 201 fveq2d ⊢ ( 𝑖 = 𝑗 → ( vol ‘ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) ) = ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) )
203 202 cbvmptv ⊢ ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) )
204 195 203 eqtri ⊢ ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) )
205 204 fveq2i ⊢ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) ) )
206 205 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) ) ) ∈ ℝ ) → ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) ) ) )
207 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) ) ) ∈ ℝ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) ) ) ∈ ℝ )
208 206 207 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) ) ) ∈ ℝ ) → ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ) ) ) ) ∈ ℝ )
209 oveq1 ⊢ ( 𝑤 = 𝑧 → ( 𝑤 − ( 𝐴 ‘ 𝑍 ) ) = ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) )
210 192 breq1d ⊢ ( 𝑖 ∈ ℕ → ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ≤ 𝑧 ↔ ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ≤ 𝑧 ) )
211 210 192 ifbieq1d ⊢ ( 𝑖 ∈ ℕ → if ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ≤ 𝑧 , ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) , 𝑧 ) = if ( ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) , 𝑧 ) )
212 190 211 oveq12d ⊢ ( 𝑖 ∈ ℕ → ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) if ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ≤ 𝑧 , ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) , 𝑧 ) ) = ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) , 𝑧 ) ) )
213 212 fveq2d ⊢ ( 𝑖 ∈ ℕ → ( vol ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) if ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ≤ 𝑧 , ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) , 𝑧 ) ) ) = ( vol ‘ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) , 𝑧 ) ) ) )
214 213 mpteq2ia ⊢ ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) if ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ≤ 𝑧 , ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) , 𝑧 ) ) ) ) = ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) , 𝑧 ) ) ) )
215 fveq2 ⊢ ( 𝑖 = ℎ → ( 𝐶 ‘ 𝑖 ) = ( 𝐶 ‘ ℎ ) )
216 215 fveq1d ⊢ ( 𝑖 = ℎ → ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) = ( ( 𝐶 ‘ ℎ ) ‘ 𝑍 ) )
217 fveq2 ⊢ ( 𝑖 = ℎ → ( 𝐷 ‘ 𝑖 ) = ( 𝐷 ‘ ℎ ) )
218 217 fveq1d ⊢ ( 𝑖 = ℎ → ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) = ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) )
219 218 breq1d ⊢ ( 𝑖 = ℎ → ( ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ≤ 𝑧 ↔ ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) ≤ 𝑧 ) )
220 219 218 ifbieq1d ⊢ ( 𝑖 = ℎ → if ( ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) , 𝑧 ) = if ( ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) , 𝑧 ) )
221 216 220 oveq12d ⊢ ( 𝑖 = ℎ → ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) , 𝑧 ) ) = ( ( ( 𝐶 ‘ ℎ ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) , 𝑧 ) ) )
222 221 fveq2d ⊢ ( 𝑖 = ℎ → ( vol ‘ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) , 𝑧 ) ) ) = ( vol ‘ ( ( ( 𝐶 ‘ ℎ ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) , 𝑧 ) ) ) )
223 222 cbvmptv ⊢ ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) , 𝑧 ) ) ) ) = ( ℎ ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ ℎ ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) , 𝑧 ) ) ) )
224 214 223 eqtri ⊢ ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) if ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ≤ 𝑧 , ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) , 𝑧 ) ) ) ) = ( ℎ ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ ℎ ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) , 𝑧 ) ) ) )
225 224 a1i ⊢ ( 𝑤 = 𝑧 → ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) if ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ≤ 𝑧 , ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) , 𝑧 ) ) ) ) = ( ℎ ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ ℎ ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) , 𝑧 ) ) ) ) )
226 breq2 ⊢ ( 𝑤 = 𝑧 → ( ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) ≤ 𝑤 ↔ ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) ≤ 𝑧 ) )
227 id ⊢ ( 𝑤 = 𝑧 → 𝑤 = 𝑧 )
228 226 227 ifbieq2d ⊢ ( 𝑤 = 𝑧 → if ( ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) ≤ 𝑤 , ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) , 𝑤 ) = if ( ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) , 𝑧 ) )
229 228 eqcomd ⊢ ( 𝑤 = 𝑧 → if ( ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) , 𝑧 ) = if ( ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) ≤ 𝑤 , ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) , 𝑤 ) )
230 229 oveq2d ⊢ ( 𝑤 = 𝑧 → ( ( ( 𝐶 ‘ ℎ ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) , 𝑧 ) ) = ( ( ( 𝐶 ‘ ℎ ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) ≤ 𝑤 , ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) , 𝑤 ) ) )
231 230 fveq2d ⊢ ( 𝑤 = 𝑧 → ( vol ‘ ( ( ( 𝐶 ‘ ℎ ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) , 𝑧 ) ) ) = ( vol ‘ ( ( ( 𝐶 ‘ ℎ ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) ≤ 𝑤 , ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) , 𝑤 ) ) ) )
232 231 mpteq2dv ⊢ ( 𝑤 = 𝑧 → ( ℎ ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ ℎ ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) ≤ 𝑧 , ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) , 𝑧 ) ) ) ) = ( ℎ ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ ℎ ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) ≤ 𝑤 , ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) , 𝑤 ) ) ) ) )
233 225 232 eqtr2d ⊢ ( 𝑤 = 𝑧 → ( ℎ ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ ℎ ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) ≤ 𝑤 , ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) , 𝑤 ) ) ) ) = ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) if ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ≤ 𝑧 , ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) , 𝑧 ) ) ) ) )
234 233 fveq2d ⊢ ( 𝑤 = 𝑧 → ( Σ^ ‘ ( ℎ ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ ℎ ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) ≤ 𝑤 , ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) , 𝑤 ) ) ) ) ) = ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) if ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ≤ 𝑧 , ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) , 𝑧 ) ) ) ) ) )
235 209 234 breq12d ⊢ ( 𝑤 = 𝑧 → ( ( 𝑤 − ( 𝐴 ‘ 𝑍 ) ) ≤ ( Σ^ ‘ ( ℎ ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ ℎ ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) ≤ 𝑤 , ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) , 𝑤 ) ) ) ) ) ↔ ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ≤ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) if ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ≤ 𝑧 , ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) , 𝑧 ) ) ) ) ) ) )
236 235 cbvrabv ⊢ { 𝑤 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝑤 − ( 𝐴 ‘ 𝑍 ) ) ≤ ( Σ^ ‘ ( ℎ ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ ℎ ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) ≤ 𝑤 , ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) , 𝑤 ) ) ) ) ) } = { 𝑧 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ≤ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) if ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ≤ 𝑧 , ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) , 𝑧 ) ) ) ) ) }
237 eqid ⊢ sup ( { 𝑤 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝑤 − ( 𝐴 ‘ 𝑍 ) ) ≤ ( Σ^ ‘ ( ℎ ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ ℎ ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) ≤ 𝑤 , ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) , 𝑤 ) ) ) ) ) } , ℝ , < ) = sup ( { 𝑤 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝑤 − ( 𝐴 ‘ 𝑍 ) ) ≤ ( Σ^ ‘ ( ℎ ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ ℎ ) ‘ 𝑍 ) [,) if ( ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) ≤ 𝑤 , ( ( 𝐷 ‘ ℎ ) ‘ 𝑍 ) , 𝑤 ) ) ) ) ) } , ℝ , < )
238 81 82 83 86 89 188 208 236 237 hoidmv1lelem3 ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) ) ) ∈ ℝ ) → ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ≤ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) [,) ( ( 𝑗 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ‘ 𝑖 ) ) ) ) ) )
239 238 206 breqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) ) ) ∈ ℝ ) → ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) ) ) )
240 25 80 239 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) ) ∧ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) ) ) = +∞ ) → ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) ) ) )
241 24 240 pm2.61dan ⊢ ( ( 𝜑 ∧ ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) ) → ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) ) ) )
242 1 32 34 4 5 hoidmvn0val ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
243 29 prodeq1d ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ { 𝑍 } ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
244 volicore ⊢ ( ( ( 𝐴 ‘ 𝑍 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑍 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) ∈ ℝ )
245 13 12 244 syl2anc ⊢ ( 𝜑 → ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) ∈ ℝ )
246 245 recnd ⊢ ( 𝜑 → ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) ∈ ℂ )
247 117 119 oveq12d ⊢ ( 𝑘 = 𝑍 → ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) )
248 247 fveq2d ⊢ ( 𝑘 = 𝑍 → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) )
249 248 prodsn ⊢ ( ( 𝑍 ∈ 𝑉 ∧ ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) ∈ ℂ ) → ∏ 𝑘 ∈ { 𝑍 } ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) )
250 2 246 249 syl2anc ⊢ ( 𝜑 → ∏ 𝑘 ∈ { 𝑍 } ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) )
251 242 243 250 3eqtrd ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) )
252 251 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) ) → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) )
253 volico ⊢ ( ( ( 𝐴 ‘ 𝑍 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑍 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) = if ( ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) , ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) , 0 ) )
254 13 12 253 syl2anc ⊢ ( 𝜑 → ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) = if ( ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) , ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) , 0 ) )
255 254 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) ) → ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) = if ( ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) , ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) , 0 ) )
256 iftrue ⊢ ( ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) → if ( ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) , ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) , 0 ) = ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) )
257 256 adantl ⊢ ( ( 𝜑 ∧ ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) ) → if ( ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) , ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) , 0 ) = ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) )
258 252 255 257 3eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) ) → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) )
259 59 fveq2d ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) ) ) )
260 259 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) ) ) )
261 258 260 breq12d ⊢ ( ( 𝜑 ∧ ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) ) → ( ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ↔ ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) ) ) ) )
262 241 261 mpbird ⊢ ( ( 𝜑 ∧ ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) ) → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
263 242 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) ) → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
264 243 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ { 𝑍 } ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
265 250 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) ) → ∏ 𝑘 ∈ { 𝑍 } ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) )
266 254 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) ) → ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) = if ( ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) , ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) , 0 ) )
267 iffalse ⊢ ( ¬ ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) → if ( ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) , ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) , 0 ) = 0 )
268 267 adantl ⊢ ( ( 𝜑 ∧ ¬ ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) ) → if ( ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) , ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) , 0 ) = 0 )
269 265 266 268 3eqtrd ⊢ ( ( 𝜑 ∧ ¬ ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) ) → ∏ 𝑘 ∈ { 𝑍 } ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = 0 )
270 263 264 269 3eqtrd ⊢ ( ( 𝜑 ∧ ¬ ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) ) → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = 0 )
271 27 a1i ⊢ ( 𝜑 → ℕ ∈ V )
272 271 76 sge0ge0 ⊢ ( 𝜑 → 0 ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
273 272 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) ) → 0 ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
274 270 273 eqbrtrd ⊢ ( ( 𝜑 ∧ ¬ ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) ) → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
275 262 274 pm2.61dan ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )