Metamath Proof Explorer

Theorem hspmbl

Description: Any half-space of the n-dimensional Real numbers is Lebesgue measurable. Lemma 115F of Fremlin1 p. 31. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses hspmbl.1 ⊢ 𝐻 = ( 𝑥 ∈ Fin ↦ ( 𝑙 ∈ 𝑥 , 𝑦 ∈ ℝ ↦ X 𝑘 ∈ 𝑥 if ( 𝑘 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) ) )
hspmbl.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
hspmbl.i ⊢ ( 𝜑 → 𝐾 ∈ 𝑋 )
hspmbl.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
Assertion hspmbl ( 𝜑 → ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ∈ dom ( voln ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 hspmbl.1 ⊢ 𝐻 = ( 𝑥 ∈ Fin ↦ ( 𝑙 ∈ 𝑥 , 𝑦 ∈ ℝ ↦ X 𝑘 ∈ 𝑥 if ( 𝑘 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) ) )
2 hspmbl.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
3 hspmbl.i ⊢ ( 𝜑 → 𝐾 ∈ 𝑋 )
4 hspmbl.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
5 2 ovnome ⊢ ( 𝜑 → ( voln* ‘ 𝑋 ) ∈ OutMeas )
6 eqid ⊢ ∪ dom ( voln* ‘ 𝑋 ) = ∪ dom ( voln* ‘ 𝑋 )
7 eqid ⊢ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) = ( CaraGen ‘ ( voln* ‘ 𝑋 ) )
8 ovex ⊢ ( -∞ (,) 𝑌 ) ∈ V
9 reex ⊢ ℝ ∈ V
10 8 9 ifex ⊢ if ( 𝑝 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ∈ V
11 10 ixpssmap ⊢ X 𝑝 ∈ 𝑋 if ( 𝑝 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ⊆ ( ∪ 𝑝 ∈ 𝑋 if ( 𝑝 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ↑m 𝑋 )
12 iftrue ⊢ ( 𝑝 = 𝐾 → if ( 𝑝 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) = ( -∞ (,) 𝑌 ) )
13 ioossre ⊢ ( -∞ (,) 𝑌 ) ⊆ ℝ
14 13 a1i ⊢ ( 𝑝 = 𝐾 → ( -∞ (,) 𝑌 ) ⊆ ℝ )
15 12 14 eqsstrd ⊢ ( 𝑝 = 𝐾 → if ( 𝑝 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ⊆ ℝ )
16 iffalse ⊢ ( ¬ 𝑝 = 𝐾 → if ( 𝑝 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) = ℝ )
17 ssid ⊢ ℝ ⊆ ℝ
18 17 a1i ⊢ ( ¬ 𝑝 = 𝐾 → ℝ ⊆ ℝ )
19 16 18 eqsstrd ⊢ ( ¬ 𝑝 = 𝐾 → if ( 𝑝 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ⊆ ℝ )
20 15 19 pm2.61i ⊢ if ( 𝑝 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ⊆ ℝ
21 20 rgenw ⊢ ∀ 𝑝 ∈ 𝑋 if ( 𝑝 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ⊆ ℝ
22 iunss ⊢ ( ∪ 𝑝 ∈ 𝑋 if ( 𝑝 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ⊆ ℝ ↔ ∀ 𝑝 ∈ 𝑋 if ( 𝑝 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ⊆ ℝ )
23 21 22 mpbir ⊢ ∪ 𝑝 ∈ 𝑋 if ( 𝑝 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ⊆ ℝ
24 mapss ⊢ ( ( ℝ ∈ V ∧ ∪ 𝑝 ∈ 𝑋 if ( 𝑝 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ⊆ ℝ ) → ( ∪ 𝑝 ∈ 𝑋 if ( 𝑝 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ↑m 𝑋 ) ⊆ ( ℝ ↑m 𝑋 ) )
25 9 23 24 mp2an ⊢ ( ∪ 𝑝 ∈ 𝑋 if ( 𝑝 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ↑m 𝑋 ) ⊆ ( ℝ ↑m 𝑋 )
26 11 25 sstri ⊢ X 𝑝 ∈ 𝑋 if ( 𝑝 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ⊆ ( ℝ ↑m 𝑋 )
27 10 rgenw ⊢ ∀ 𝑝 ∈ 𝑋 if ( 𝑝 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ∈ V
28 ixpexg ⊢ ( ∀ 𝑝 ∈ 𝑋 if ( 𝑝 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ∈ V → X 𝑝 ∈ 𝑋 if ( 𝑝 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ∈ V )
29 27 28 ax-mp ⊢ X 𝑝 ∈ 𝑋 if ( 𝑝 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ∈ V
30 elpwg ⊢ ( X 𝑝 ∈ 𝑋 if ( 𝑝 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ∈ V → ( X 𝑝 ∈ 𝑋 if ( 𝑝 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↔ X 𝑝 ∈ 𝑋 if ( 𝑝 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ⊆ ( ℝ ↑m 𝑋 ) ) )
31 29 30 ax-mp ⊢ ( X 𝑝 ∈ 𝑋 if ( 𝑝 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↔ X 𝑝 ∈ 𝑋 if ( 𝑝 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ⊆ ( ℝ ↑m 𝑋 ) )
32 26 31 mpbir ⊢ X 𝑝 ∈ 𝑋 if ( 𝑝 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ∈ 𝒫 ( ℝ ↑m 𝑋 )
33 32 a1i ⊢ ( 𝜑 → X 𝑝 ∈ 𝑋 if ( 𝑝 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ∈ 𝒫 ( ℝ ↑m 𝑋 ) )
34 equid ⊢ 𝑥 = 𝑥
35 eqid ⊢ ℝ = ℝ
36 equequ1 ⊢ ( 𝑘 = 𝑝 → ( 𝑘 = 𝑙 ↔ 𝑝 = 𝑙 ) )
37 36 ifbid ⊢ ( 𝑘 = 𝑝 → if ( 𝑘 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) = if ( 𝑝 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) )
38 37 cbvixpv ⊢ X 𝑘 ∈ 𝑥 if ( 𝑘 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) = X 𝑝 ∈ 𝑥 if ( 𝑝 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ )
39 34 35 38 mpoeq123i ⊢ ( 𝑙 ∈ 𝑥 , 𝑦 ∈ ℝ ↦ X 𝑘 ∈ 𝑥 if ( 𝑘 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) ) = ( 𝑙 ∈ 𝑥 , 𝑦 ∈ ℝ ↦ X 𝑝 ∈ 𝑥 if ( 𝑝 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) )
40 39 mpteq2i ⊢ ( 𝑥 ∈ Fin ↦ ( 𝑙 ∈ 𝑥 , 𝑦 ∈ ℝ ↦ X 𝑘 ∈ 𝑥 if ( 𝑘 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) ) ) = ( 𝑥 ∈ Fin ↦ ( 𝑙 ∈ 𝑥 , 𝑦 ∈ ℝ ↦ X 𝑝 ∈ 𝑥 if ( 𝑝 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) ) )
41 1 40 eqtri ⊢ 𝐻 = ( 𝑥 ∈ Fin ↦ ( 𝑙 ∈ 𝑥 , 𝑦 ∈ ℝ ↦ X 𝑝 ∈ 𝑥 if ( 𝑝 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) ) )
42 41 2 3 4 hspval ⊢ ( 𝜑 → ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) = X 𝑝 ∈ 𝑋 if ( 𝑝 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) )
43 2 ovnf ⊢ ( 𝜑 → ( voln* ‘ 𝑋 ) : 𝒫 ( ℝ ↑m 𝑋 ) ⟶ ( 0 [,] +∞ ) )
44 43 fdmd ⊢ ( 𝜑 → dom ( voln* ‘ 𝑋 ) = 𝒫 ( ℝ ↑m 𝑋 ) )
45 44 unieqd ⊢ ( 𝜑 → ∪ dom ( voln* ‘ 𝑋 ) = ∪ 𝒫 ( ℝ ↑m 𝑋 ) )
46 unipw ⊢ ∪ 𝒫 ( ℝ ↑m 𝑋 ) = ( ℝ ↑m 𝑋 )
47 46 a1i ⊢ ( 𝜑 → ∪ 𝒫 ( ℝ ↑m 𝑋 ) = ( ℝ ↑m 𝑋 ) )
48 45 47 eqtrd ⊢ ( 𝜑 → ∪ dom ( voln* ‘ 𝑋 ) = ( ℝ ↑m 𝑋 ) )
49 48 pweqd ⊢ ( 𝜑 → 𝒫 ∪ dom ( voln* ‘ 𝑋 ) = 𝒫 ( ℝ ↑m 𝑋 ) )
50 42 49 eleq12d ⊢ ( 𝜑 → ( ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ↔ X 𝑝 ∈ 𝑋 if ( 𝑝 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) )
51 33 50 mpbird ⊢ ( 𝜑 → ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) )
52 simpl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ) → 𝜑 )
53 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ) → 𝑎 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) )
54 52 49 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ) → 𝒫 ∪ dom ( voln* ‘ 𝑋 ) = 𝒫 ( ℝ ↑m 𝑋 ) )
55 53 54 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ) → 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) )
56 2 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) → 𝑋 ∈ Fin )
57 inss1 ⊢ ( 𝑎 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ⊆ 𝑎
58 57 a1i ⊢ ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) → ( 𝑎 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ⊆ 𝑎 )
59 elpwi ⊢ ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) → 𝑎 ⊆ ( ℝ ↑m 𝑋 ) )
60 58 59 sstrd ⊢ ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) → ( 𝑎 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ⊆ ( ℝ ↑m 𝑋 ) )
61 60 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) → ( 𝑎 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ⊆ ( ℝ ↑m 𝑋 ) )
62 56 61 ovnxrcl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) → ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∈ ℝ* )
63 59 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) → 𝑎 ⊆ ( ℝ ↑m 𝑋 ) )
64 63 ssdifssd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) → ( 𝑎 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ⊆ ( ℝ ↑m 𝑋 ) )
65 56 64 ovnxrcl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) → ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∈ ℝ* )
66 62 65 xaddcld ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) ∈ ℝ* )
67 pnfge ⊢ ( ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) ∈ ℝ* → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) ≤ +∞ )
68 66 67 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) ≤ +∞ )
69 68 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) ∧ ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) = +∞ ) → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) ≤ +∞ )
70 id ⊢ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) = +∞ → ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) = +∞ )
71 70 eqcomd ⊢ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) = +∞ → +∞ = ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) )
72 71 adantl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) ∧ ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) = +∞ ) → +∞ = ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) )
73 69 72 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) ∧ ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) = +∞ ) → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) )
74 simpl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) ∧ ¬ ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) = +∞ ) → ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) )
75 56 63 ovncl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) → ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ∈ ( 0 [,] +∞ ) )
76 75 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) ∧ ¬ ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) = +∞ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ∈ ( 0 [,] +∞ ) )
77 neqne ⊢ ( ¬ ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) = +∞ → ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ≠ +∞ )
78 77 adantl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) ∧ ¬ ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) = +∞ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ≠ +∞ )
79 ge0xrre ⊢ ( ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ∈ ( 0 [,] +∞ ) ∧ ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ≠ +∞ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ∈ ℝ )
80 76 78 79 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) ∧ ¬ ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) = +∞ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ∈ ℝ )
81 56 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) ∧ ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ∈ ℝ ) → 𝑋 ∈ Fin )
82 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) ∧ ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ∈ ℝ ) → 𝐾 ∈ 𝑋 )
83 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) ∧ ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ∈ ℝ ) → 𝑌 ∈ ℝ )
84 simpr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) ∧ ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ∈ ℝ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ∈ ℝ )
85 63 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) ∧ ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ∈ ℝ ) → 𝑎 ⊆ ( ℝ ↑m 𝑋 ) )
86 sseq1 ⊢ ( 𝑎 = 𝑏 → ( 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) ↔ 𝑏 ⊆ ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) ) )
87 86 rabbidv ⊢ ( 𝑎 = 𝑏 → { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) } = { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) } )
88 87 cbvmptv ⊢ ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) } ) = ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 ⊆ ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) } )
89 simpl ⊢ ( ( 𝑖 = ℎ ∧ 𝑝 ∈ 𝑋 ) → 𝑖 = ℎ )
90 89 coeq2d ⊢ ( ( 𝑖 = ℎ ∧ 𝑝 ∈ 𝑋 ) → ( [,) ∘ 𝑖 ) = ( [,) ∘ ℎ ) )
91 90 fveq1d ⊢ ( ( 𝑖 = ℎ ∧ 𝑝 ∈ 𝑋 ) → ( ( [,) ∘ 𝑖 ) ‘ 𝑝 ) = ( ( [,) ∘ ℎ ) ‘ 𝑝 ) )
92 91 fveq2d ⊢ ( ( 𝑖 = ℎ ∧ 𝑝 ∈ 𝑋 ) → ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑝 ) ) = ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑝 ) ) )
93 92 prodeq2dv ⊢ ( 𝑖 = ℎ → ∏ 𝑝 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑝 ) ) = ∏ 𝑝 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑝 ) ) )
94 93 cbvmptv ⊢ ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑝 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑝 ) ) ) = ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑝 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑝 ) ) )
95 fveq2 ⊢ ( 𝑛 = 𝑝 → ( ( [,) ∘ ( 𝑚 ‘ 𝑖 ) ) ‘ 𝑛 ) = ( ( [,) ∘ ( 𝑚 ‘ 𝑖 ) ) ‘ 𝑝 ) )
96 95 cbvixpv ⊢ X 𝑛 ∈ 𝑋 ( ( [,) ∘ ( 𝑚 ‘ 𝑖 ) ) ‘ 𝑛 ) = X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑚 ‘ 𝑖 ) ) ‘ 𝑝 )
97 96 a1i ⊢ ( 𝑚 = ℎ → X 𝑛 ∈ 𝑋 ( ( [,) ∘ ( 𝑚 ‘ 𝑖 ) ) ‘ 𝑛 ) = X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑚 ‘ 𝑖 ) ) ‘ 𝑝 ) )
98 fveq1 ⊢ ( 𝑚 = ℎ → ( 𝑚 ‘ 𝑖 ) = ( ℎ ‘ 𝑖 ) )
99 98 coeq2d ⊢ ( 𝑚 = ℎ → ( [,) ∘ ( 𝑚 ‘ 𝑖 ) ) = ( [,) ∘ ( ℎ ‘ 𝑖 ) ) )
100 99 fveq1d ⊢ ( 𝑚 = ℎ → ( ( [,) ∘ ( 𝑚 ‘ 𝑖 ) ) ‘ 𝑝 ) = ( ( [,) ∘ ( ℎ ‘ 𝑖 ) ) ‘ 𝑝 ) )
101 100 ixpeq2dv ⊢ ( 𝑚 = ℎ → X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑚 ‘ 𝑖 ) ) ‘ 𝑝 ) = X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑖 ) ) ‘ 𝑝 ) )
102 97 101 eqtrd ⊢ ( 𝑚 = ℎ → X 𝑛 ∈ 𝑋 ( ( [,) ∘ ( 𝑚 ‘ 𝑖 ) ) ‘ 𝑛 ) = X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑖 ) ) ‘ 𝑝 ) )
103 102 adantr ⊢ ( ( 𝑚 = ℎ ∧ 𝑖 ∈ ℕ ) → X 𝑛 ∈ 𝑋 ( ( [,) ∘ ( 𝑚 ‘ 𝑖 ) ) ‘ 𝑛 ) = X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑖 ) ) ‘ 𝑝 ) )
104 103 iuneq2dv ⊢ ( 𝑚 = ℎ → ∪ 𝑖 ∈ ℕ X 𝑛 ∈ 𝑋 ( ( [,) ∘ ( 𝑚 ‘ 𝑖 ) ) ‘ 𝑛 ) = ∪ 𝑖 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑖 ) ) ‘ 𝑝 ) )
105 104 sseq2d ⊢ ( 𝑚 = ℎ → ( 𝑎 ⊆ ∪ 𝑖 ∈ ℕ X 𝑛 ∈ 𝑋 ( ( [,) ∘ ( 𝑚 ‘ 𝑖 ) ) ‘ 𝑛 ) ↔ 𝑎 ⊆ ∪ 𝑖 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑖 ) ) ‘ 𝑝 ) ) )
106 105 cbvrabv ⊢ { 𝑚 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑖 ∈ ℕ X 𝑛 ∈ 𝑋 ( ( [,) ∘ ( 𝑚 ‘ 𝑖 ) ) ‘ 𝑛 ) } = { ℎ ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑖 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑖 ) ) ‘ 𝑝 ) }
107 fveq1 ⊢ ( ℎ = 𝑙 → ( ℎ ‘ 𝑖 ) = ( 𝑙 ‘ 𝑖 ) )
108 107 coeq2d ⊢ ( ℎ = 𝑙 → ( [,) ∘ ( ℎ ‘ 𝑖 ) ) = ( [,) ∘ ( 𝑙 ‘ 𝑖 ) ) )
109 108 fveq1d ⊢ ( ℎ = 𝑙 → ( ( [,) ∘ ( ℎ ‘ 𝑖 ) ) ‘ 𝑝 ) = ( ( [,) ∘ ( 𝑙 ‘ 𝑖 ) ) ‘ 𝑝 ) )
110 109 ixpeq2dv ⊢ ( ℎ = 𝑙 → X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑖 ) ) ‘ 𝑝 ) = X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑖 ) ) ‘ 𝑝 ) )
111 110 adantr ⊢ ( ( ℎ = 𝑙 ∧ 𝑖 ∈ ℕ ) → X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑖 ) ) ‘ 𝑝 ) = X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑖 ) ) ‘ 𝑝 ) )
112 111 iuneq2dv ⊢ ( ℎ = 𝑙 → ∪ 𝑖 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑖 ) ) ‘ 𝑝 ) = ∪ 𝑖 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑖 ) ) ‘ 𝑝 ) )
113 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝑙 ‘ 𝑖 ) = ( 𝑙 ‘ 𝑗 ) )
114 113 coeq2d ⊢ ( 𝑖 = 𝑗 → ( [,) ∘ ( 𝑙 ‘ 𝑖 ) ) = ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) )
115 114 fveq1d ⊢ ( 𝑖 = 𝑗 → ( ( [,) ∘ ( 𝑙 ‘ 𝑖 ) ) ‘ 𝑝 ) = ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) )
116 115 ixpeq2dv ⊢ ( 𝑖 = 𝑗 → X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑖 ) ) ‘ 𝑝 ) = X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) )
117 116 cbviunv ⊢ ∪ 𝑖 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑖 ) ) ‘ 𝑝 ) = ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 )
118 117 a1i ⊢ ( ℎ = 𝑙 → ∪ 𝑖 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑖 ) ) ‘ 𝑝 ) = ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) )
119 112 118 eqtrd ⊢ ( ℎ = 𝑙 → ∪ 𝑖 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑖 ) ) ‘ 𝑝 ) = ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) )
120 119 sseq2d ⊢ ( ℎ = 𝑙 → ( 𝑎 ⊆ ∪ 𝑖 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑖 ) ) ‘ 𝑝 ) ↔ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) ) )
121 120 cbvrabv ⊢ { ℎ ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑖 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑖 ) ) ‘ 𝑝 ) } = { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) }
122 106 121 eqtri ⊢ { 𝑚 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑖 ∈ ℕ X 𝑛 ∈ 𝑋 ( ( [,) ∘ ( 𝑚 ‘ 𝑖 ) ) ‘ 𝑛 ) } = { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) }
123 122 mpteq2i ⊢ ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑚 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑖 ∈ ℕ X 𝑛 ∈ 𝑋 ( ( [,) ∘ ( 𝑚 ‘ 𝑖 ) ) ‘ 𝑛 ) } ) = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) } )
124 123 a1i ⊢ ( 𝑐 = 𝑏 → ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑚 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑖 ∈ ℕ X 𝑛 ∈ 𝑋 ( ( [,) ∘ ( 𝑚 ‘ 𝑖 ) ) ‘ 𝑛 ) } ) = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) } ) )
125 id ⊢ ( 𝑐 = 𝑏 → 𝑐 = 𝑏 )
126 124 125 fveq12d ⊢ ( 𝑐 = 𝑏 → ( ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑚 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑖 ∈ ℕ X 𝑛 ∈ 𝑋 ( ( [,) ∘ ( 𝑚 ‘ 𝑖 ) ) ‘ 𝑛 ) } ) ‘ 𝑐 ) = ( ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) } ) ‘ 𝑏 ) )
127 126 eleq2d ⊢ ( 𝑐 = 𝑏 → ( 𝑡 ∈ ( ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑚 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑖 ∈ ℕ X 𝑛 ∈ 𝑋 ( ( [,) ∘ ( 𝑚 ‘ 𝑖 ) ) ‘ 𝑛 ) } ) ‘ 𝑐 ) ↔ 𝑡 ∈ ( ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) } ) ‘ 𝑏 ) ) )
128 2fveq3 ⊢ ( 𝑚 = 𝑝 → ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑚 ) ) = ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑝 ) ) )
129 128 cbvprodv ⊢ ∏ 𝑚 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑚 ) ) = ∏ 𝑝 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑝 ) )
130 129 mpteq2i ⊢ ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑚 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑚 ) ) ) = ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑝 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑝 ) ) )
131 130 a1i ⊢ ( 𝑚 = 𝑗 → ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑚 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑚 ) ) ) = ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑝 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑝 ) ) ) )
132 fveq2 ⊢ ( 𝑚 = 𝑗 → ( 𝑡 ‘ 𝑚 ) = ( 𝑡 ‘ 𝑗 ) )
133 131 132 fveq12d ⊢ ( 𝑚 = 𝑗 → ( ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑚 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑚 ) ) ) ‘ ( 𝑡 ‘ 𝑚 ) ) = ( ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑝 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑝 ) ) ) ‘ ( 𝑡 ‘ 𝑗 ) ) )
134 133 cbvmptv ⊢ ( 𝑚 ∈ ℕ ↦ ( ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑚 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑚 ) ) ) ‘ ( 𝑡 ‘ 𝑚 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑝 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑝 ) ) ) ‘ ( 𝑡 ‘ 𝑗 ) ) )
135 134 a1i ⊢ ( 𝑐 = 𝑏 → ( 𝑚 ∈ ℕ ↦ ( ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑚 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑚 ) ) ) ‘ ( 𝑡 ‘ 𝑚 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑝 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑝 ) ) ) ‘ ( 𝑡 ‘ 𝑗 ) ) ) )
136 135 fveq2d ⊢ ( 𝑐 = 𝑏 → ( Σ^ ‘ ( 𝑚 ∈ ℕ ↦ ( ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑚 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑚 ) ) ) ‘ ( 𝑡 ‘ 𝑚 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑝 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑝 ) ) ) ‘ ( 𝑡 ‘ 𝑗 ) ) ) ) )
137 fveq2 ⊢ ( 𝑐 = 𝑏 → ( ( voln* ‘ 𝑋 ) ‘ 𝑐 ) = ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) )
138 137 oveq1d ⊢ ( 𝑐 = 𝑏 → ( ( ( voln* ‘ 𝑋 ) ‘ 𝑐 ) +𝑒 𝑠 ) = ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +𝑒 𝑠 ) )
139 136 138 breq12d ⊢ ( 𝑐 = 𝑏 → ( ( Σ^ ‘ ( 𝑚 ∈ ℕ ↦ ( ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑚 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑚 ) ) ) ‘ ( 𝑡 ‘ 𝑚 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑐 ) +𝑒 𝑠 ) ↔ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑝 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑝 ) ) ) ‘ ( 𝑡 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +𝑒 𝑠 ) ) )
140 127 139 anbi12d ⊢ ( 𝑐 = 𝑏 → ( ( 𝑡 ∈ ( ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑚 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑖 ∈ ℕ X 𝑛 ∈ 𝑋 ( ( [,) ∘ ( 𝑚 ‘ 𝑖 ) ) ‘ 𝑛 ) } ) ‘ 𝑐 ) ∧ ( Σ^ ‘ ( 𝑚 ∈ ℕ ↦ ( ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑚 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑚 ) ) ) ‘ ( 𝑡 ‘ 𝑚 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑐 ) +𝑒 𝑠 ) ) ↔ ( 𝑡 ∈ ( ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) } ) ‘ 𝑏 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑝 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑝 ) ) ) ‘ ( 𝑡 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +𝑒 𝑠 ) ) ) )
141 140 rabbidva2 ⊢ ( 𝑐 = 𝑏 → { 𝑡 ∈ ( ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑚 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑖 ∈ ℕ X 𝑛 ∈ 𝑋 ( ( [,) ∘ ( 𝑚 ‘ 𝑖 ) ) ‘ 𝑛 ) } ) ‘ 𝑐 ) ∣ ( Σ^ ‘ ( 𝑚 ∈ ℕ ↦ ( ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑚 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑚 ) ) ) ‘ ( 𝑡 ‘ 𝑚 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑐 ) +𝑒 𝑠 ) } = { 𝑡 ∈ ( ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) } ) ‘ 𝑏 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑝 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑝 ) ) ) ‘ ( 𝑡 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +𝑒 𝑠 ) } )
142 141 mpteq2dv ⊢ ( 𝑐 = 𝑏 → ( 𝑠 ∈ ℝ+ ↦ { 𝑡 ∈ ( ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑚 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑖 ∈ ℕ X 𝑛 ∈ 𝑋 ( ( [,) ∘ ( 𝑚 ‘ 𝑖 ) ) ‘ 𝑛 ) } ) ‘ 𝑐 ) ∣ ( Σ^ ‘ ( 𝑚 ∈ ℕ ↦ ( ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑚 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑚 ) ) ) ‘ ( 𝑡 ‘ 𝑚 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑐 ) +𝑒 𝑠 ) } ) = ( 𝑠 ∈ ℝ+ ↦ { 𝑡 ∈ ( ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) } ) ‘ 𝑏 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑝 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑝 ) ) ) ‘ ( 𝑡 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +𝑒 𝑠 ) } ) )
143 eqidd ⊢ ( 𝑠 = 𝑟 → ( ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) } ) ‘ 𝑏 ) = ( ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) } ) ‘ 𝑏 ) )
144 143 eleq2d ⊢ ( 𝑠 = 𝑟 → ( 𝑡 ∈ ( ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) } ) ‘ 𝑏 ) ↔ 𝑡 ∈ ( ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) } ) ‘ 𝑏 ) ) )
145 oveq2 ⊢ ( 𝑠 = 𝑟 → ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +𝑒 𝑠 ) = ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +𝑒 𝑟 ) )
146 145 breq2d ⊢ ( 𝑠 = 𝑟 → ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑝 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑝 ) ) ) ‘ ( 𝑡 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +𝑒 𝑠 ) ↔ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑝 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑝 ) ) ) ‘ ( 𝑡 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +𝑒 𝑟 ) ) )
147 144 146 anbi12d ⊢ ( 𝑠 = 𝑟 → ( ( 𝑡 ∈ ( ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) } ) ‘ 𝑏 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑝 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑝 ) ) ) ‘ ( 𝑡 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +𝑒 𝑠 ) ) ↔ ( 𝑡 ∈ ( ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) } ) ‘ 𝑏 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑝 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑝 ) ) ) ‘ ( 𝑡 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +𝑒 𝑟 ) ) ) )
148 147 rabbidva2 ⊢ ( 𝑠 = 𝑟 → { 𝑡 ∈ ( ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) } ) ‘ 𝑏 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑝 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑝 ) ) ) ‘ ( 𝑡 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +𝑒 𝑠 ) } = { 𝑡 ∈ ( ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) } ) ‘ 𝑏 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑝 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑝 ) ) ) ‘ ( 𝑡 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +𝑒 𝑟 ) } )
149 148 cbvmptv ⊢ ( 𝑠 ∈ ℝ+ ↦ { 𝑡 ∈ ( ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) } ) ‘ 𝑏 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑝 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑝 ) ) ) ‘ ( 𝑡 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +𝑒 𝑠 ) } ) = ( 𝑟 ∈ ℝ+ ↦ { 𝑡 ∈ ( ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) } ) ‘ 𝑏 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑝 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑝 ) ) ) ‘ ( 𝑡 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +𝑒 𝑟 ) } )
150 149 a1i ⊢ ( 𝑐 = 𝑏 → ( 𝑠 ∈ ℝ+ ↦ { 𝑡 ∈ ( ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) } ) ‘ 𝑏 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑝 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑝 ) ) ) ‘ ( 𝑡 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +𝑒 𝑠 ) } ) = ( 𝑟 ∈ ℝ+ ↦ { 𝑡 ∈ ( ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) } ) ‘ 𝑏 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑝 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑝 ) ) ) ‘ ( 𝑡 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +𝑒 𝑟 ) } ) )
151 142 150 eqtrd ⊢ ( 𝑐 = 𝑏 → ( 𝑠 ∈ ℝ+ ↦ { 𝑡 ∈ ( ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑚 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑖 ∈ ℕ X 𝑛 ∈ 𝑋 ( ( [,) ∘ ( 𝑚 ‘ 𝑖 ) ) ‘ 𝑛 ) } ) ‘ 𝑐 ) ∣ ( Σ^ ‘ ( 𝑚 ∈ ℕ ↦ ( ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑚 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑚 ) ) ) ‘ ( 𝑡 ‘ 𝑚 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑐 ) +𝑒 𝑠 ) } ) = ( 𝑟 ∈ ℝ+ ↦ { 𝑡 ∈ ( ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) } ) ‘ 𝑏 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑝 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑝 ) ) ) ‘ ( 𝑡 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +𝑒 𝑟 ) } ) )
152 151 cbvmptv ⊢ ( 𝑐 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ ( 𝑠 ∈ ℝ+ ↦ { 𝑡 ∈ ( ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑚 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑖 ∈ ℕ X 𝑛 ∈ 𝑋 ( ( [,) ∘ ( 𝑚 ‘ 𝑖 ) ) ‘ 𝑛 ) } ) ‘ 𝑐 ) ∣ ( Σ^ ‘ ( 𝑚 ∈ ℕ ↦ ( ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑚 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑚 ) ) ) ‘ ( 𝑡 ‘ 𝑚 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑐 ) +𝑒 𝑠 ) } ) ) = ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ ( 𝑟 ∈ ℝ+ ↦ { 𝑡 ∈ ( ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑝 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑝 ) } ) ‘ 𝑏 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑝 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑝 ) ) ) ‘ ( 𝑡 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑏 ) +𝑒 𝑟 ) } ) )
153 2fveq3 ⊢ ( 𝑚 = 𝑝 → ( 1st ‘ ( ( 𝑡 ‘ 𝑗 ) ‘ 𝑚 ) ) = ( 1st ‘ ( ( 𝑡 ‘ 𝑗 ) ‘ 𝑝 ) ) )
154 153 cbvmptv ⊢ ( 𝑚 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑡 ‘ 𝑗 ) ‘ 𝑚 ) ) ) = ( 𝑝 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑡 ‘ 𝑗 ) ‘ 𝑝 ) ) )
155 154 mpteq2i ⊢ ( 𝑗 ∈ ℕ ↦ ( 𝑚 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑡 ‘ 𝑗 ) ‘ 𝑚 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( 𝑝 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑡 ‘ 𝑗 ) ‘ 𝑝 ) ) ) )
156 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝑡 ‘ 𝑖 ) = ( 𝑡 ‘ 𝑗 ) )
157 156 fveq1d ⊢ ( 𝑖 = 𝑗 → ( ( 𝑡 ‘ 𝑖 ) ‘ 𝑚 ) = ( ( 𝑡 ‘ 𝑗 ) ‘ 𝑚 ) )
158 157 fveq2d ⊢ ( 𝑖 = 𝑗 → ( 2nd ‘ ( ( 𝑡 ‘ 𝑖 ) ‘ 𝑚 ) ) = ( 2nd ‘ ( ( 𝑡 ‘ 𝑗 ) ‘ 𝑚 ) ) )
159 158 mpteq2dv ⊢ ( 𝑖 = 𝑗 → ( 𝑚 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑡 ‘ 𝑖 ) ‘ 𝑚 ) ) ) = ( 𝑚 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑡 ‘ 𝑗 ) ‘ 𝑚 ) ) ) )
160 2fveq3 ⊢ ( 𝑚 = 𝑝 → ( 2nd ‘ ( ( 𝑡 ‘ 𝑗 ) ‘ 𝑚 ) ) = ( 2nd ‘ ( ( 𝑡 ‘ 𝑗 ) ‘ 𝑝 ) ) )
161 160 cbvmptv ⊢ ( 𝑚 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑡 ‘ 𝑗 ) ‘ 𝑚 ) ) ) = ( 𝑝 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑡 ‘ 𝑗 ) ‘ 𝑝 ) ) )
162 161 a1i ⊢ ( 𝑖 = 𝑗 → ( 𝑚 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑡 ‘ 𝑗 ) ‘ 𝑚 ) ) ) = ( 𝑝 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑡 ‘ 𝑗 ) ‘ 𝑝 ) ) ) )
163 159 162 eqtrd ⊢ ( 𝑖 = 𝑗 → ( 𝑚 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑡 ‘ 𝑖 ) ‘ 𝑚 ) ) ) = ( 𝑝 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑡 ‘ 𝑗 ) ‘ 𝑝 ) ) ) )
164 163 cbvmptv ⊢ ( 𝑖 ∈ ℕ ↦ ( 𝑚 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑡 ‘ 𝑖 ) ‘ 𝑚 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( 𝑝 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑡 ‘ 𝑗 ) ‘ 𝑝 ) ) ) )
165 41 81 82 83 84 85 88 94 152 155 164 hspmbllem3 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) ∧ ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ∈ ℝ ) → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) )
166 74 80 165 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) ∧ ¬ ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) = +∞ ) → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) )
167 73 166 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) )
168 52 55 167 syl2anc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ) → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) )
169 5 6 7 51 168 caragenel2d ⊢ ( 𝜑 → ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ∈ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) )
170 2 dmvon ⊢ ( 𝜑 → dom ( voln ‘ 𝑋 ) = ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) )
171 170 eqcomd ⊢ ( 𝜑 → ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) = dom ( voln ‘ 𝑋 ) )
172 169 171 eleqtrd ⊢ ( 𝜑 → ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ∈ dom ( voln ‘ 𝑋 ) )