Metamath Proof Explorer

Theorem ovnlecvr2

Description: Given a subset of multidimensional reals and a set of half-open intervals that covers it, the Lebesgue outer measure of the set is bounded by the generalized sum of the pre-measure of the half-open intervals. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses ovnlecvr2.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
ovnlecvr2.c ⊢ ( 𝜑 → 𝐶 : ℕ ⟶ ( ℝ ↑m 𝑋 ) )
ovnlecvr2.d ⊢ ( 𝜑 → 𝐷 : ℕ ⟶ ( ℝ ↑m 𝑋 ) )
ovnlecvr2.s ⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
ovnlecvr2.l ⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
Assertion ovnlecvr2 ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ovnlecvr2.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
2 ovnlecvr2.c ⊢ ( 𝜑 → 𝐶 : ℕ ⟶ ( ℝ ↑m 𝑋 ) )
3 ovnlecvr2.d ⊢ ( 𝜑 → 𝐷 : ℕ ⟶ ( ℝ ↑m 𝑋 ) )
4 ovnlecvr2.s ⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
5 ovnlecvr2.l ⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
6 fveq2 ⊢ ( 𝑋 = ∅ → ( voln* ‘ 𝑋 ) = ( voln* ‘ ∅ ) )
7 6 fveq1d ⊢ ( 𝑋 = ∅ → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) = ( ( voln* ‘ ∅ ) ‘ 𝐴 ) )
8 7 adantl ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) = ( ( voln* ‘ ∅ ) ‘ 𝐴 ) )
9 4 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
10 1nn ⊢ 1 ∈ ℕ
11 ne0i ⊢ ( 1 ∈ ℕ → ℕ ≠ ∅ )
12 10 11 ax-mp ⊢ ℕ ≠ ∅
13 12 a1i ⊢ ( 𝜑 → ℕ ≠ ∅ )
14 iunconst ⊢ ( ℕ ≠ ∅ → ∪ 𝑗 ∈ ℕ { ∅ } = { ∅ } )
15 13 14 syl ⊢ ( 𝜑 → ∪ 𝑗 ∈ ℕ { ∅ } = { ∅ } )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ∪ 𝑗 ∈ ℕ { ∅ } = { ∅ } )
17 ixpeq1 ⊢ ( 𝑋 = ∅ → X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) = X 𝑘 ∈ ∅ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
18 ixp0x ⊢ X 𝑘 ∈ ∅ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) = { ∅ }
19 18 a1i ⊢ ( 𝑋 = ∅ → X 𝑘 ∈ ∅ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) = { ∅ } )
20 17 19 eqtrd ⊢ ( 𝑋 = ∅ → X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) = { ∅ } )
21 20 adantr ⊢ ( ( 𝑋 = ∅ ∧ 𝑗 ∈ ℕ ) → X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) = { ∅ } )
22 21 iuneq2dv ⊢ ( 𝑋 = ∅ → ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) = ∪ 𝑗 ∈ ℕ { ∅ } )
23 22 adantl ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) = ∪ 𝑗 ∈ ℕ { ∅ } )
24 reex ⊢ ℝ ∈ V
25 mapdm0 ⊢ ( ℝ ∈ V → ( ℝ ↑m ∅ ) = { ∅ } )
26 24 25 ax-mp ⊢ ( ℝ ↑m ∅ ) = { ∅ }
27 26 a1i ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ℝ ↑m ∅ ) = { ∅ } )
28 16 23 27 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) = ( ℝ ↑m ∅ ) )
29 9 28 sseqtrd ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 𝐴 ⊆ ( ℝ ↑m ∅ ) )
30 29 ovn0val ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( voln* ‘ ∅ ) ‘ 𝐴 ) = 0 )
31 8 30 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) = 0 )
32 nfv ⊢ Ⅎ 𝑗 𝜑
33 nnex ⊢ ℕ ∈ V
34 33 a1i ⊢ ( 𝜑 → ℕ ∈ V )
35 icossicc ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
36 1 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑋 ∈ Fin )
37 2 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑋 ) )
38 elmapi ⊢ ( ( 𝐶 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑋 ) → ( 𝐶 ‘ 𝑗 ) : 𝑋 ⟶ ℝ )
39 37 38 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) : 𝑋 ⟶ ℝ )
40 3 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑋 ) )
41 elmapi ⊢ ( ( 𝐷 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑋 ) → ( 𝐷 ‘ 𝑗 ) : 𝑋 ⟶ ℝ )
42 40 41 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) : 𝑋 ⟶ ℝ )
43 5 36 39 42 hoidmvcl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ∈ ( 0 [,) +∞ ) )
44 35 43 sselid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ∈ ( 0 [,] +∞ ) )
45 32 34 44 sge0ge0mpt ⊢ ( 𝜑 → 0 ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
46 45 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 0 ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
47 31 46 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
48 simpl ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → 𝜑 )
49 neqne ⊢ ( ¬ 𝑋 = ∅ → 𝑋 ≠ ∅ )
50 49 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → 𝑋 ≠ ∅ )
51 1 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → 𝑋 ∈ Fin )
52 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → 𝑋 ≠ ∅ )
53 39 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) ∈ ℝ )
54 42 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ∈ ℝ )
55 54 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ∈ ℝ* )
56 icossre ⊢ ( ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) ∈ ℝ ∧ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ∈ ℝ* ) → ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ⊆ ℝ )
57 53 55 56 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ⊆ ℝ )
58 57 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ∀ 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ⊆ ℝ )
59 ss2ixp ⊢ ( ∀ 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ⊆ ℝ → X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ⊆ X 𝑘 ∈ 𝑋 ℝ )
60 58 59 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ⊆ X 𝑘 ∈ 𝑋 ℝ )
61 24 a1i ⊢ ( 𝜑 → ℝ ∈ V )
62 ixpconstg ⊢ ( ( 𝑋 ∈ Fin ∧ ℝ ∈ V ) → X 𝑘 ∈ 𝑋 ℝ = ( ℝ ↑m 𝑋 ) )
63 1 61 62 syl2anc ⊢ ( 𝜑 → X 𝑘 ∈ 𝑋 ℝ = ( ℝ ↑m 𝑋 ) )
64 63 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → X 𝑘 ∈ 𝑋 ℝ = ( ℝ ↑m 𝑋 ) )
65 60 64 sseqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ⊆ ( ℝ ↑m 𝑋 ) )
66 65 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ⊆ ( ℝ ↑m 𝑋 ) )
67 iunss ⊢ ( ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ⊆ ( ℝ ↑m 𝑋 ) ↔ ∀ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ⊆ ( ℝ ↑m 𝑋 ) )
68 66 67 sylibr ⊢ ( 𝜑 → ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ⊆ ( ℝ ↑m 𝑋 ) )
69 4 68 sstrd ⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
70 69 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → 𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
71 eqid ⊢ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } = { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) }
72 51 52 70 71 ovnn0val ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) = inf ( { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } , ℝ* , < ) )
73 ssrab2 ⊢ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ⊆ ℝ*
74 73 a1i ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ⊆ ℝ* )
75 32 34 44 sge0xrclmpt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ* )
76 75 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ* )
77 opelxpi ⊢ ( ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) ∈ ℝ ∧ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ∈ ℝ ) → ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ∈ ( ℝ × ℝ ) )
78 53 54 77 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ∈ ( ℝ × ℝ ) )
79 78 fmpttd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) : 𝑋 ⟶ ( ℝ × ℝ ) )
80 24 24 xpex ⊢ ( ℝ × ℝ ) ∈ V
81 80 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ℝ × ℝ ) ∈ V )
82 elmapg ⊢ ( ( ( ℝ × ℝ ) ∈ V ∧ 𝑋 ∈ Fin ) → ( ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↔ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) : 𝑋 ⟶ ( ℝ × ℝ ) ) )
83 81 36 82 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↔ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) : 𝑋 ⟶ ( ℝ × ℝ ) ) )
84 79 83 mpbird ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
85 84 fmpttd ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) : ℕ ⟶ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
86 ovexd ⊢ ( 𝜑 → ( ( ℝ × ℝ ) ↑m 𝑋 ) ∈ V )
87 elmapg ⊢ ( ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ∈ V ∧ ℕ ∈ V ) → ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ↔ ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) : ℕ ⟶ ( ( ℝ × ℝ ) ↑m 𝑋 ) ) )
88 86 34 87 syl2anc ⊢ ( 𝜑 → ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ↔ ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) : ℕ ⟶ ( ( ℝ × ℝ ) ↑m 𝑋 ) ) )
89 85 88 mpbird ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) )
90 89 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) )
91 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ )
92 mptexg ⊢ ( 𝑋 ∈ Fin → ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ∈ V )
93 1 92 syl ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ∈ V )
94 93 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ∈ V )
95 eqid ⊢ ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) )
96 95 fvmpt2 ⊢ ( ( 𝑗 ∈ ℕ ∧ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ∈ V ) → ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) = ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) )
97 91 94 96 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) = ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) )
98 97 coeq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) = ( [,) ∘ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) )
99 98 fveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( [,) ∘ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑘 ) )
100 99 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( [,) ∘ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑘 ) )
101 79 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) : 𝑋 ⟶ ( ℝ × ℝ ) )
102 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → 𝑘 ∈ 𝑋 )
103 101 102 fvovco ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( [,) ∘ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑘 ) = ( ( 1st ‘ ( ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ‘ 𝑘 ) ) ) )
104 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝑘 ∈ 𝑋 )
105 opex ⊢ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ∈ V
106 105 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ∈ V )
107 eqid ⊢ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) = ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ )
108 107 fvmpt2 ⊢ ( ( 𝑘 ∈ 𝑋 ∧ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ∈ V ) → ( ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ‘ 𝑘 ) = ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ )
109 104 106 108 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ‘ 𝑘 ) = ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ )
110 109 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 1st ‘ ( ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ‘ 𝑘 ) ) = ( 1st ‘ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) )
111 fvex ⊢ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) ∈ V
112 fvex ⊢ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ∈ V
113 op1stg ⊢ ( ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) ∈ V ∧ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ∈ V ) → ( 1st ‘ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) = ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) )
114 111 112 113 mp2an ⊢ ( 1st ‘ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) = ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 )
115 114 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 1st ‘ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) = ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) )
116 110 115 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 1st ‘ ( ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ‘ 𝑘 ) ) = ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) )
117 109 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 2nd ‘ ( ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ‘ 𝑘 ) ) = ( 2nd ‘ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) )
118 111 112 op2nd ⊢ ( 2nd ‘ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) = ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 )
119 118 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 2nd ‘ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) = ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) )
120 117 119 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 2nd ‘ ( ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ‘ 𝑘 ) ) = ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) )
121 116 120 oveq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( 1st ‘ ( ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ‘ 𝑘 ) ) ) = ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
122 121 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 1st ‘ ( ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ‘ 𝑘 ) ) ) = ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
123 100 103 122 3eqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) = ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) )
124 123 ixpeq2dva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) = X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) )
125 124 iuneq2dv ⊢ ( 𝜑 → ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) = ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) )
126 4 125 sseqtrd ⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) )
127 126 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) )
128 eqidd ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) ) )
129 51 adantr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑗 ∈ ℕ ) → 𝑋 ∈ Fin )
130 52 adantr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑗 ∈ ℕ ) → 𝑋 ≠ ∅ )
131 39 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) : 𝑋 ⟶ ℝ )
132 42 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) : 𝑋 ⟶ ℝ )
133 5 129 130 131 132 hoidmvn0val ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) )
134 133 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) = ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) )
135 134 fveq2d ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) ) )
136 123 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
137 136 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) )
138 137 prodeq2dv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) )
139 138 mpteq2dva ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) = ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) )
140 139 fveq2d ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) ) )
141 140 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) ) )
142 128 135 141 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
143 127 142 jca ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
144 nfcv ⊢ Ⅎ 𝑗 𝑖
145 nfmpt1 ⊢ Ⅎ 𝑗 ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) )
146 144 145 nfeq ⊢ Ⅎ 𝑗 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) )
147 nfcv ⊢ Ⅎ 𝑘 𝑖
148 nfcv ⊢ Ⅎ 𝑘 ℕ
149 nfmpt1 ⊢ Ⅎ 𝑘 ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ )
150 148 149 nfmpt ⊢ Ⅎ 𝑘 ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) )
151 147 150 nfeq ⊢ Ⅎ 𝑘 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) )
152 fveq1 ⊢ ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) → ( 𝑖 ‘ 𝑗 ) = ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) )
153 152 coeq2d ⊢ ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) → ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) = ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) )
154 153 fveq1d ⊢ ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) → ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) )
155 154 adantr ⊢ ( ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ∧ 𝑘 ∈ 𝑋 ) → ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) )
156 151 155 ixpeq2d ⊢ ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) → X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) )
157 156 adantr ⊢ ( ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ∧ 𝑗 ∈ ℕ ) → X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) )
158 146 157 iuneq2df ⊢ ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) → ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) )
159 158 sseq2d ⊢ ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) → ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ↔ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
160 nfv ⊢ Ⅎ 𝑘 𝑗 ∈ ℕ
161 151 160 nfan ⊢ Ⅎ 𝑘 ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ∧ 𝑗 ∈ ℕ )
162 154 fveq2d ⊢ ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) → ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
163 162 a1d ⊢ ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) → ( 𝑘 ∈ 𝑋 → ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) )
164 163 adantr ⊢ ( ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ∧ 𝑗 ∈ ℕ ) → ( 𝑘 ∈ 𝑋 → ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) )
165 161 164 ralrimi ⊢ ( ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ∧ 𝑗 ∈ ℕ ) → ∀ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
166 165 prodeq2d ⊢ ( ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ∧ 𝑗 ∈ ℕ ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
167 146 166 mpteq2da ⊢ ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) → ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) = ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) )
168 167 fveq2d ⊢ ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
169 168 eqeq2d ⊢ ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) → ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ↔ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
170 159 169 anbi12d ⊢ ( 𝑖 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) → ( ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ↔ ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
171 170 rspcev ⊢ ( ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ⟨ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ⟩ ) ) ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
172 90 143 171 syl2anc ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
173 76 172 jca ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ* ∧ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
174 eqeq1 ⊢ ( 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) → ( 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ↔ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
175 174 anbi2d ⊢ ( 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) → ( ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ↔ ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
176 175 rexbidv ⊢ ( 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) → ( ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ↔ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
177 176 elrab ⊢ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ↔ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ* ∧ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
178 173 177 sylibr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } )
179 infxrlb ⊢ ( ( { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ⊆ ℝ* ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ) → inf ( { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } , ℝ* , < ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
180 74 178 179 syl2anc ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → inf ( { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } , ℝ* , < ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
181 72 180 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
182 48 50 181 syl2anc ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
183 47 182 pm2.61dan ⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )