Metamath Proof Explorer


Theorem hspmbllem3

Description: Any half-space of the n-dimensional Real numbers is Lebesgue measurable. Lemma 115F of Fremlin1 p. 31. This proof handles the non-trivial cases (nonzero dimension and finite outer measure). (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses hspmbllem3.h 𝐻 = ( 𝑥 ∈ Fin ↦ ( 𝑙𝑥 , 𝑦 ∈ ℝ ↦ X 𝑘𝑥 if ( 𝑘 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) ) )
hspmbllem3.x ( 𝜑𝑋 ∈ Fin )
hspmbllem3.i ( 𝜑𝐾𝑋 )
hspmbllem3.y ( 𝜑𝑌 ∈ ℝ )
hspmbllem3.a ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ∈ ℝ )
hspmbllem3.s ( 𝜑𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
hspmbllem3.c 𝐶 = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } )
hspmbllem3.l 𝐿 = ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) )
hspmbllem3.d 𝐷 = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ ( 𝑟 ∈ ℝ+ ↦ { 𝑖 ∈ ( 𝐶𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑟 ) } ) )
hspmbllem3.10 𝐵 = ( 𝑗 ∈ ℕ ↦ ( 𝑘𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) ) )
hspmbllem3.11 𝑇 = ( 𝑗 ∈ ℕ ↦ ( 𝑘𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) ) )
Assertion hspmbllem3 ( 𝜑 → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 hspmbllem3.h 𝐻 = ( 𝑥 ∈ Fin ↦ ( 𝑙𝑥 , 𝑦 ∈ ℝ ↦ X 𝑘𝑥 if ( 𝑘 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) ) )
2 hspmbllem3.x ( 𝜑𝑋 ∈ Fin )
3 hspmbllem3.i ( 𝜑𝐾𝑋 )
4 hspmbllem3.y ( 𝜑𝑌 ∈ ℝ )
5 hspmbllem3.a ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ∈ ℝ )
6 hspmbllem3.s ( 𝜑𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
7 hspmbllem3.c 𝐶 = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } )
8 hspmbllem3.l 𝐿 = ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) )
9 hspmbllem3.d 𝐷 = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ ( 𝑟 ∈ ℝ+ ↦ { 𝑖 ∈ ( 𝐶𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑟 ) } ) )
10 hspmbllem3.10 𝐵 = ( 𝑗 ∈ ℕ ↦ ( 𝑘𝑋 ↦ ( 1st ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) ) )
11 hspmbllem3.11 𝑇 = ( 𝑗 ∈ ℕ ↦ ( 𝑘𝑋 ↦ ( 2nd ‘ ( ( 𝑖𝑗 ) ‘ 𝑘 ) ) ) )
12 inss1 ( 𝐴 ∩ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ⊆ 𝐴
13 12 6 sstrid ( 𝜑 → ( 𝐴 ∩ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ⊆ ( ℝ ↑m 𝑋 ) )
14 2 13 ovncl ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) ∈ ( 0 [,] +∞ ) )
15 12 a1i ( 𝜑 → ( 𝐴 ∩ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ⊆ 𝐴 )
16 2 15 6 ovnssle ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) )
17 5 14 16 ge0lere ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) ∈ ℝ )
18 6 ssdifssd ( 𝜑 → ( 𝐴 ∖ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ⊆ ( ℝ ↑m 𝑋 ) )
19 2 18 ovncl ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) ∈ ( 0 [,] +∞ ) )
20 difssd ( 𝜑 → ( 𝐴 ∖ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ⊆ 𝐴 )
21 2 20 6 ovnssle ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) )
22 5 19 21 ge0lere ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) ∈ ℝ )
23 rexadd ( ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) ∈ ℝ ∧ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) ∈ ℝ ) → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) ) = ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) ) )
24 17 22 23 syl2anc ( 𝜑 → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) ) = ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) ) )
25 2 adantr ( ( 𝜑𝑒 ∈ ℝ+ ) → 𝑋 ∈ Fin )
26 3 ne0d ( 𝜑𝑋 ≠ ∅ )
27 26 adantr ( ( 𝜑𝑒 ∈ ℝ+ ) → 𝑋 ≠ ∅ )
28 6 adantr ( ( 𝜑𝑒 ∈ ℝ+ ) → 𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
29 simpr ( ( 𝜑𝑒 ∈ ℝ+ ) → 𝑒 ∈ ℝ+ )
30 25 27 28 29 7 8 9 ovncvrrp ( ( 𝜑𝑒 ∈ ℝ+ ) → ∃ 𝑖 𝑖 ∈ ( ( 𝐷𝐴 ) ‘ 𝑒 ) )
31 25 adantr ( ( ( 𝜑𝑒 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ( 𝐷𝐴 ) ‘ 𝑒 ) ) → 𝑋 ∈ Fin )
32 3 ad2antrr ( ( ( 𝜑𝑒 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ( 𝐷𝐴 ) ‘ 𝑒 ) ) → 𝐾𝑋 )
33 4 ad2antrr ( ( ( 𝜑𝑒 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ( 𝐷𝐴 ) ‘ 𝑒 ) ) → 𝑌 ∈ ℝ )
34 29 adantr ( ( ( 𝜑𝑒 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ( 𝐷𝐴 ) ‘ 𝑒 ) ) → 𝑒 ∈ ℝ+ )
35 28 adantr ( ( ( 𝜑𝑒 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ( 𝐷𝐴 ) ‘ 𝑒 ) ) → 𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
36 fveq1 ( 𝑖 = → ( 𝑖𝑗 ) = ( 𝑗 ) )
37 36 fveq2d ( 𝑖 = → ( 𝐿 ‘ ( 𝑖𝑗 ) ) = ( 𝐿 ‘ ( 𝑗 ) ) )
38 37 mpteq2dv ( 𝑖 = → ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑗 ) ) ) )
39 38 fveq2d ( 𝑖 = → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑗 ) ) ) ) )
40 39 breq1d ( 𝑖 = → ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑟 ) ↔ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑟 ) ) )
41 40 cbvrabv { 𝑖 ∈ ( 𝐶𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑟 ) } = { ∈ ( 𝐶𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑟 ) }
42 41 mpteq2i ( 𝑟 ∈ ℝ+ ↦ { 𝑖 ∈ ( 𝐶𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑟 ) } ) = ( 𝑟 ∈ ℝ+ ↦ { ∈ ( 𝐶𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑟 ) } )
43 42 mpteq2i ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ ( 𝑟 ∈ ℝ+ ↦ { 𝑖 ∈ ( 𝐶𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑟 ) } ) ) = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ ( 𝑟 ∈ ℝ+ ↦ { ∈ ( 𝐶𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑟 ) } ) )
44 9 43 eqtri 𝐷 = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ ( 𝑟 ∈ ℝ+ ↦ { ∈ ( 𝐶𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑟 ) } ) )
45 simpr ( ( ( 𝜑𝑒 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ( 𝐷𝐴 ) ‘ 𝑒 ) ) → 𝑖 ∈ ( ( 𝐷𝐴 ) ‘ 𝑒 ) )
46 31 35 34 7 8 44 45 10 11 ovncvr2 ( ( ( 𝜑𝑒 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ( 𝐷𝐴 ) ‘ 𝑒 ) ) → ( ( ( 𝐵 : ℕ ⟶ ( ℝ ↑m 𝑋 ) ∧ 𝑇 : ℕ ⟶ ( ℝ ↑m 𝑋 ) ) ∧ 𝐴 𝑗 ∈ ℕ X 𝑘𝑋 ( ( ( 𝐵𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇𝑗 ) ‘ 𝑘 ) ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( ( 𝐵𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇𝑗 ) ‘ 𝑘 ) ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝑒 ) ) )
47 46 simplld ( ( ( 𝜑𝑒 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ( 𝐷𝐴 ) ‘ 𝑒 ) ) → ( 𝐵 : ℕ ⟶ ( ℝ ↑m 𝑋 ) ∧ 𝑇 : ℕ ⟶ ( ℝ ↑m 𝑋 ) ) )
48 47 simpld ( ( ( 𝜑𝑒 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ( 𝐷𝐴 ) ‘ 𝑒 ) ) → 𝐵 : ℕ ⟶ ( ℝ ↑m 𝑋 ) )
49 47 simprd ( ( ( 𝜑𝑒 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ( 𝐷𝐴 ) ‘ 𝑒 ) ) → 𝑇 : ℕ ⟶ ( ℝ ↑m 𝑋 ) )
50 46 simplrd ( ( ( 𝜑𝑒 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ( 𝐷𝐴 ) ‘ 𝑒 ) ) → 𝐴 𝑗 ∈ ℕ X 𝑘𝑋 ( ( ( 𝐵𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇𝑗 ) ‘ 𝑘 ) ) )
51 46 simprd ( ( ( 𝜑𝑒 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ( 𝐷𝐴 ) ‘ 𝑒 ) ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( ( 𝐵𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇𝑗 ) ‘ 𝑘 ) ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝑒 ) )
52 5 adantr ( ( 𝜑𝑒 ∈ ℝ+ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ∈ ℝ )
53 29 rpred ( ( 𝜑𝑒 ∈ ℝ+ ) → 𝑒 ∈ ℝ )
54 52 53 rexaddd ( ( 𝜑𝑒 ∈ ℝ+ ) → ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝑒 ) = ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) + 𝑒 ) )
55 54 adantr ( ( ( 𝜑𝑒 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ( 𝐷𝐴 ) ‘ 𝑒 ) ) → ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝑒 ) = ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) + 𝑒 ) )
56 51 55 breqtrd ( ( ( 𝜑𝑒 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ( 𝐷𝐴 ) ‘ 𝑒 ) ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( ( 𝐵𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇𝑗 ) ‘ 𝑘 ) ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) + 𝑒 ) )
57 5 ad2antrr ( ( ( 𝜑𝑒 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ( 𝐷𝐴 ) ‘ 𝑒 ) ) → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ∈ ℝ )
58 17 ad2antrr ( ( ( 𝜑𝑒 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ( 𝐷𝐴 ) ‘ 𝑒 ) ) → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) ∈ ℝ )
59 22 ad2antrr ( ( ( 𝜑𝑒 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ( 𝐷𝐴 ) ‘ 𝑒 ) ) → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) ∈ ℝ )
60 eqid ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘𝑥 ( vol ‘ ( ( 𝑎𝑘 ) [,) ( 𝑏𝑘 ) ) ) ) ) ) = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘𝑥 ( vol ‘ ( ( 𝑎𝑘 ) [,) ( 𝑏𝑘 ) ) ) ) ) )
61 eqid ( 𝑦 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑋 ) ↦ ( 𝑋 ↦ if ( ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ) , if ( ( 𝑐 ) ≤ 𝑦 , ( 𝑐 ) , 𝑦 ) ) ) ) ) = ( 𝑦 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑋 ) ↦ ( 𝑋 ↦ if ( ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ) , if ( ( 𝑐 ) ≤ 𝑦 , ( 𝑐 ) , 𝑦 ) ) ) ) )
62 eqid ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑋 ) ↦ ( 𝑋 ↦ if ( = 𝐾 , if ( 𝑥 ≤ ( 𝑐 ) , ( 𝑐 ) , 𝑥 ) , ( 𝑐 ) ) ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑋 ) ↦ ( 𝑋 ↦ if ( = 𝐾 , if ( 𝑥 ≤ ( 𝑐 ) , ( 𝑐 ) , 𝑥 ) , ( 𝑐 ) ) ) ) )
63 1 31 32 33 34 48 49 50 56 57 58 59 60 61 62 hspmbllem2 ( ( ( 𝜑𝑒 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ( 𝐷𝐴 ) ‘ 𝑒 ) ) → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) + 𝑒 ) )
64 63 ex ( ( 𝜑𝑒 ∈ ℝ+ ) → ( 𝑖 ∈ ( ( 𝐷𝐴 ) ‘ 𝑒 ) → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) + 𝑒 ) ) )
65 64 exlimdv ( ( 𝜑𝑒 ∈ ℝ+ ) → ( ∃ 𝑖 𝑖 ∈ ( ( 𝐷𝐴 ) ‘ 𝑒 ) → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) + 𝑒 ) ) )
66 30 65 mpd ( ( 𝜑𝑒 ∈ ℝ+ ) → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) + 𝑒 ) )
67 66 ralrimiva ( 𝜑 → ∀ 𝑒 ∈ ℝ+ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) + 𝑒 ) )
68 17 22 readdcld ( 𝜑 → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) ) ∈ ℝ )
69 alrple ( ( ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) ) ∈ ℝ ∧ ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ∈ ℝ ) → ( ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ↔ ∀ 𝑒 ∈ ℝ+ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) + 𝑒 ) ) )
70 68 5 69 syl2anc ( 𝜑 → ( ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ↔ ∀ 𝑒 ∈ ℝ+ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) + 𝑒 ) ) )
71 67 70 mpbird ( 𝜑 → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) )
72 24 71 eqbrtrd ( 𝜑 → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻𝑋 ) 𝑌 ) ) ) ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) )