Metamath Proof Explorer


Theorem uniioombllem2

Description: Lemma for uniioombl . (Contributed by Mario Carneiro, 26-Mar-2015) (Revised by Mario Carneiro, 11-Dec-2016) (Revised by AV, 13-Sep-2020)

Ref Expression
Hypotheses uniioombl.1 ( 𝜑𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
uniioombl.2 ( 𝜑Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹𝑥 ) ) )
uniioombl.3 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
uniioombl.a 𝐴 = ran ( (,) ∘ 𝐹 )
uniioombl.e ( 𝜑 → ( vol* ‘ 𝐸 ) ∈ ℝ )
uniioombl.c ( 𝜑𝐶 ∈ ℝ+ )
uniioombl.g ( 𝜑𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
uniioombl.s ( 𝜑𝐸 ran ( (,) ∘ 𝐺 ) )
uniioombl.t 𝑇 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) )
uniioombl.v ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐸 ) + 𝐶 ) )
uniioombllem2.h 𝐻 = ( 𝑧 ∈ ℕ ↦ ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) )
uniioombllem2.k 𝐾 = ( 𝑥 ∈ ran (,) ↦ if ( 𝑥 = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( 𝑥 , ℝ* , < ) , sup ( 𝑥 , ℝ* , < ) ⟩ ) )
Assertion uniioombllem2 ( ( 𝜑𝐽 ∈ ℕ ) → seq 1 ( + , ( vol* ∘ 𝐻 ) ) ⇝ ( vol* ‘ ( ( (,) ‘ ( 𝐺𝐽 ) ) ∩ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 uniioombl.1 ( 𝜑𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
2 uniioombl.2 ( 𝜑Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹𝑥 ) ) )
3 uniioombl.3 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
4 uniioombl.a 𝐴 = ran ( (,) ∘ 𝐹 )
5 uniioombl.e ( 𝜑 → ( vol* ‘ 𝐸 ) ∈ ℝ )
6 uniioombl.c ( 𝜑𝐶 ∈ ℝ+ )
7 uniioombl.g ( 𝜑𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
8 uniioombl.s ( 𝜑𝐸 ran ( (,) ∘ 𝐺 ) )
9 uniioombl.t 𝑇 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) )
10 uniioombl.v ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐸 ) + 𝐶 ) )
11 uniioombllem2.h 𝐻 = ( 𝑧 ∈ ℕ ↦ ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) )
12 uniioombllem2.k 𝐾 = ( 𝑥 ∈ ran (,) ↦ if ( 𝑥 = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( 𝑥 , ℝ* , < ) , sup ( 𝑥 , ℝ* , < ) ⟩ ) )
13 nnuz ℕ = ( ℤ ‘ 1 )
14 eqid seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) )
15 1zzd ( ( 𝜑𝐽 ∈ ℕ ) → 1 ∈ ℤ )
16 eqidd ( ( ( 𝜑𝐽 ∈ ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ‘ 𝑛 ) = ( ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ‘ 𝑛 ) )
17 1 2 3 4 5 6 7 8 9 10 uniioombllem2a ( ( ( 𝜑𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ∈ ran (,) )
18 11 a1i ( ( 𝜑𝐽 ∈ ℕ ) → 𝐻 = ( 𝑧 ∈ ℕ ↦ ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ) )
19 12 ioorf 𝐾 : ran (,) ⟶ ( ≤ ∩ ( ℝ* × ℝ* ) )
20 19 a1i ( ( 𝜑𝐽 ∈ ℕ ) → 𝐾 : ran (,) ⟶ ( ≤ ∩ ( ℝ* × ℝ* ) ) )
21 20 feqmptd ( ( 𝜑𝐽 ∈ ℕ ) → 𝐾 = ( 𝑦 ∈ ran (,) ↦ ( 𝐾𝑦 ) ) )
22 fveq2 ( 𝑦 = ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) → ( 𝐾𝑦 ) = ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ) )
23 17 18 21 22 fmptco ( ( 𝜑𝐽 ∈ ℕ ) → ( 𝐾𝐻 ) = ( 𝑧 ∈ ℕ ↦ ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ) ) )
24 inss2 ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ⊆ ( (,) ‘ ( 𝐺𝐽 ) )
25 inss2 ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
26 7 ffvelrnda ( ( 𝜑𝐽 ∈ ℕ ) → ( 𝐺𝐽 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
27 25 26 sselid ( ( 𝜑𝐽 ∈ ℕ ) → ( 𝐺𝐽 ) ∈ ( ℝ × ℝ ) )
28 1st2nd2 ( ( 𝐺𝐽 ) ∈ ( ℝ × ℝ ) → ( 𝐺𝐽 ) = ⟨ ( 1st ‘ ( 𝐺𝐽 ) ) , ( 2nd ‘ ( 𝐺𝐽 ) ) ⟩ )
29 27 28 syl ( ( 𝜑𝐽 ∈ ℕ ) → ( 𝐺𝐽 ) = ⟨ ( 1st ‘ ( 𝐺𝐽 ) ) , ( 2nd ‘ ( 𝐺𝐽 ) ) ⟩ )
30 29 fveq2d ( ( 𝜑𝐽 ∈ ℕ ) → ( (,) ‘ ( 𝐺𝐽 ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐺𝐽 ) ) , ( 2nd ‘ ( 𝐺𝐽 ) ) ⟩ ) )
31 df-ov ( ( 1st ‘ ( 𝐺𝐽 ) ) (,) ( 2nd ‘ ( 𝐺𝐽 ) ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐺𝐽 ) ) , ( 2nd ‘ ( 𝐺𝐽 ) ) ⟩ )
32 30 31 eqtr4di ( ( 𝜑𝐽 ∈ ℕ ) → ( (,) ‘ ( 𝐺𝐽 ) ) = ( ( 1st ‘ ( 𝐺𝐽 ) ) (,) ( 2nd ‘ ( 𝐺𝐽 ) ) ) )
33 ioossre ( ( 1st ‘ ( 𝐺𝐽 ) ) (,) ( 2nd ‘ ( 𝐺𝐽 ) ) ) ⊆ ℝ
34 32 33 eqsstrdi ( ( 𝜑𝐽 ∈ ℕ ) → ( (,) ‘ ( 𝐺𝐽 ) ) ⊆ ℝ )
35 32 fveq2d ( ( 𝜑𝐽 ∈ ℕ ) → ( vol* ‘ ( (,) ‘ ( 𝐺𝐽 ) ) ) = ( vol* ‘ ( ( 1st ‘ ( 𝐺𝐽 ) ) (,) ( 2nd ‘ ( 𝐺𝐽 ) ) ) ) )
36 ovolfcl ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐽 ∈ ℕ ) → ( ( 1st ‘ ( 𝐺𝐽 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐺𝐽 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐺𝐽 ) ) ≤ ( 2nd ‘ ( 𝐺𝐽 ) ) ) )
37 7 36 sylan ( ( 𝜑𝐽 ∈ ℕ ) → ( ( 1st ‘ ( 𝐺𝐽 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐺𝐽 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐺𝐽 ) ) ≤ ( 2nd ‘ ( 𝐺𝐽 ) ) ) )
38 ovolioo ( ( ( 1st ‘ ( 𝐺𝐽 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐺𝐽 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐺𝐽 ) ) ≤ ( 2nd ‘ ( 𝐺𝐽 ) ) ) → ( vol* ‘ ( ( 1st ‘ ( 𝐺𝐽 ) ) (,) ( 2nd ‘ ( 𝐺𝐽 ) ) ) ) = ( ( 2nd ‘ ( 𝐺𝐽 ) ) − ( 1st ‘ ( 𝐺𝐽 ) ) ) )
39 37 38 syl ( ( 𝜑𝐽 ∈ ℕ ) → ( vol* ‘ ( ( 1st ‘ ( 𝐺𝐽 ) ) (,) ( 2nd ‘ ( 𝐺𝐽 ) ) ) ) = ( ( 2nd ‘ ( 𝐺𝐽 ) ) − ( 1st ‘ ( 𝐺𝐽 ) ) ) )
40 35 39 eqtrd ( ( 𝜑𝐽 ∈ ℕ ) → ( vol* ‘ ( (,) ‘ ( 𝐺𝐽 ) ) ) = ( ( 2nd ‘ ( 𝐺𝐽 ) ) − ( 1st ‘ ( 𝐺𝐽 ) ) ) )
41 37 simp2d ( ( 𝜑𝐽 ∈ ℕ ) → ( 2nd ‘ ( 𝐺𝐽 ) ) ∈ ℝ )
42 37 simp1d ( ( 𝜑𝐽 ∈ ℕ ) → ( 1st ‘ ( 𝐺𝐽 ) ) ∈ ℝ )
43 41 42 resubcld ( ( 𝜑𝐽 ∈ ℕ ) → ( ( 2nd ‘ ( 𝐺𝐽 ) ) − ( 1st ‘ ( 𝐺𝐽 ) ) ) ∈ ℝ )
44 40 43 eqeltrd ( ( 𝜑𝐽 ∈ ℕ ) → ( vol* ‘ ( (,) ‘ ( 𝐺𝐽 ) ) ) ∈ ℝ )
45 ovolsscl ( ( ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ⊆ ( (,) ‘ ( 𝐺𝐽 ) ) ∧ ( (,) ‘ ( 𝐺𝐽 ) ) ⊆ ℝ ∧ ( vol* ‘ ( (,) ‘ ( 𝐺𝐽 ) ) ) ∈ ℝ ) → ( vol* ‘ ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ) ∈ ℝ )
46 24 34 44 45 mp3an2i ( ( 𝜑𝐽 ∈ ℕ ) → ( vol* ‘ ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ) ∈ ℝ )
47 46 adantr ( ( ( 𝜑𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( vol* ‘ ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ) ∈ ℝ )
48 12 ioorcl ( ( ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ∈ ran (,) ∧ ( vol* ‘ ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ) ∈ ℝ ) → ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
49 17 47 48 syl2anc ( ( ( 𝜑𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
50 23 49 fmpt3d ( ( 𝜑𝐽 ∈ ℕ ) → ( 𝐾𝐻 ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
51 eqid ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) = ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) )
52 51 ovolfsf ( ( 𝐾𝐻 ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) : ℕ ⟶ ( 0 [,) +∞ ) )
53 50 52 syl ( ( 𝜑𝐽 ∈ ℕ ) → ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) : ℕ ⟶ ( 0 [,) +∞ ) )
54 53 ffvelrnda ( ( ( 𝜑𝐽 ∈ ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ‘ 𝑛 ) ∈ ( 0 [,) +∞ ) )
55 elrege0 ( ( ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ‘ 𝑛 ) ∈ ( 0 [,) +∞ ) ↔ ( ( ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ‘ 𝑛 ) ∈ ℝ ∧ 0 ≤ ( ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ‘ 𝑛 ) ) )
56 54 55 sylib ( ( ( 𝜑𝐽 ∈ ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ‘ 𝑛 ) ∈ ℝ ∧ 0 ≤ ( ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ‘ 𝑛 ) ) )
57 56 simpld ( ( ( 𝜑𝐽 ∈ ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ‘ 𝑛 ) ∈ ℝ )
58 56 simprd ( ( ( 𝜑𝐽 ∈ ℕ ) ∧ 𝑛 ∈ ℕ ) → 0 ≤ ( ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ‘ 𝑛 ) )
59 23 fveq1d ( ( 𝜑𝐽 ∈ ℕ ) → ( ( 𝐾𝐻 ) ‘ 𝑧 ) = ( ( 𝑧 ∈ ℕ ↦ ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ) ) ‘ 𝑧 ) )
60 fvex ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ) ∈ V
61 eqid ( 𝑧 ∈ ℕ ↦ ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ) ) = ( 𝑧 ∈ ℕ ↦ ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ) )
62 61 fvmpt2 ( ( 𝑧 ∈ ℕ ∧ ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ) ∈ V ) → ( ( 𝑧 ∈ ℕ ↦ ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ) ) ‘ 𝑧 ) = ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ) )
63 60 62 mpan2 ( 𝑧 ∈ ℕ → ( ( 𝑧 ∈ ℕ ↦ ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ) ) ‘ 𝑧 ) = ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ) )
64 59 63 sylan9eq ( ( ( 𝜑𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( ( 𝐾𝐻 ) ‘ 𝑧 ) = ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ) )
65 64 fveq2d ( ( ( 𝜑𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( (,) ‘ ( ( 𝐾𝐻 ) ‘ 𝑧 ) ) = ( (,) ‘ ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ) ) )
66 12 ioorinv ( ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ∈ ran (,) → ( (,) ‘ ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ) ) = ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) )
67 17 66 syl ( ( ( 𝜑𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( (,) ‘ ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ) ) = ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) )
68 65 67 eqtrd ( ( ( 𝜑𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( (,) ‘ ( ( 𝐾𝐻 ) ‘ 𝑧 ) ) = ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) )
69 68 ralrimiva ( ( 𝜑𝐽 ∈ ℕ ) → ∀ 𝑧 ∈ ℕ ( (,) ‘ ( ( 𝐾𝐻 ) ‘ 𝑧 ) ) = ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) )
70 2fveq3 ( 𝑧 = 𝑥 → ( (,) ‘ ( ( 𝐾𝐻 ) ‘ 𝑧 ) ) = ( (,) ‘ ( ( 𝐾𝐻 ) ‘ 𝑥 ) ) )
71 2fveq3 ( 𝑧 = 𝑥 → ( (,) ‘ ( 𝐹𝑧 ) ) = ( (,) ‘ ( 𝐹𝑥 ) ) )
72 71 ineq1d ( 𝑧 = 𝑥 → ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) = ( ( (,) ‘ ( 𝐹𝑥 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) )
73 70 72 eqeq12d ( 𝑧 = 𝑥 → ( ( (,) ‘ ( ( 𝐾𝐻 ) ‘ 𝑧 ) ) = ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ↔ ( (,) ‘ ( ( 𝐾𝐻 ) ‘ 𝑥 ) ) = ( ( (,) ‘ ( 𝐹𝑥 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ) )
74 73 rspccva ( ( ∀ 𝑧 ∈ ℕ ( (,) ‘ ( ( 𝐾𝐻 ) ‘ 𝑧 ) ) = ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( (,) ‘ ( ( 𝐾𝐻 ) ‘ 𝑥 ) ) = ( ( (,) ‘ ( 𝐹𝑥 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) )
75 69 74 sylan ( ( ( 𝜑𝐽 ∈ ℕ ) ∧ 𝑥 ∈ ℕ ) → ( (,) ‘ ( ( 𝐾𝐻 ) ‘ 𝑥 ) ) = ( ( (,) ‘ ( 𝐹𝑥 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) )
76 inss1 ( ( (,) ‘ ( 𝐹𝑥 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ⊆ ( (,) ‘ ( 𝐹𝑥 ) )
77 75 76 eqsstrdi ( ( ( 𝜑𝐽 ∈ ℕ ) ∧ 𝑥 ∈ ℕ ) → ( (,) ‘ ( ( 𝐾𝐻 ) ‘ 𝑥 ) ) ⊆ ( (,) ‘ ( 𝐹𝑥 ) ) )
78 77 ralrimiva ( ( 𝜑𝐽 ∈ ℕ ) → ∀ 𝑥 ∈ ℕ ( (,) ‘ ( ( 𝐾𝐻 ) ‘ 𝑥 ) ) ⊆ ( (,) ‘ ( 𝐹𝑥 ) ) )
79 2 adantr ( ( 𝜑𝐽 ∈ ℕ ) → Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹𝑥 ) ) )
80 disjss2 ( ∀ 𝑥 ∈ ℕ ( (,) ‘ ( ( 𝐾𝐻 ) ‘ 𝑥 ) ) ⊆ ( (,) ‘ ( 𝐹𝑥 ) ) → ( Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹𝑥 ) ) → Disj 𝑥 ∈ ℕ ( (,) ‘ ( ( 𝐾𝐻 ) ‘ 𝑥 ) ) ) )
81 78 79 80 sylc ( ( 𝜑𝐽 ∈ ℕ ) → Disj 𝑥 ∈ ℕ ( (,) ‘ ( ( 𝐾𝐻 ) ‘ 𝑥 ) ) )
82 50 81 14 uniioovol ( ( 𝜑𝐽 ∈ ℕ ) → ( vol* ‘ ran ( (,) ∘ ( 𝐾𝐻 ) ) ) = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) , ℝ* , < ) )
83 67 mpteq2dva ( ( 𝜑𝐽 ∈ ℕ ) → ( 𝑧 ∈ ℕ ↦ ( (,) ‘ ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ) ) ) = ( 𝑧 ∈ ℕ ↦ ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ) )
84 rexpssxrxp ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* )
85 25 84 sstri ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ* × ℝ* )
86 85 49 sselid ( ( ( 𝜑𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ) ∈ ( ℝ* × ℝ* ) )
87 ioof (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
88 87 a1i ( ( 𝜑𝐽 ∈ ℕ ) → (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ )
89 88 feqmptd ( ( 𝜑𝐽 ∈ ℕ ) → (,) = ( 𝑦 ∈ ( ℝ* × ℝ* ) ↦ ( (,) ‘ 𝑦 ) ) )
90 fveq2 ( 𝑦 = ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ) → ( (,) ‘ 𝑦 ) = ( (,) ‘ ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ) ) )
91 86 23 89 90 fmptco ( ( 𝜑𝐽 ∈ ℕ ) → ( (,) ∘ ( 𝐾𝐻 ) ) = ( 𝑧 ∈ ℕ ↦ ( (,) ‘ ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ) ) ) )
92 83 91 18 3eqtr4d ( ( 𝜑𝐽 ∈ ℕ ) → ( (,) ∘ ( 𝐾𝐻 ) ) = 𝐻 )
93 92 rneqd ( ( 𝜑𝐽 ∈ ℕ ) → ran ( (,) ∘ ( 𝐾𝐻 ) ) = ran 𝐻 )
94 93 unieqd ( ( 𝜑𝐽 ∈ ℕ ) → ran ( (,) ∘ ( 𝐾𝐻 ) ) = ran 𝐻 )
95 fvex ( (,) ‘ ( 𝐹𝑧 ) ) ∈ V
96 95 inex1 ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ∈ V
97 11 fvmpt2 ( ( 𝑧 ∈ ℕ ∧ ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) ∈ V ) → ( 𝐻𝑧 ) = ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) )
98 96 97 mpan2 ( 𝑧 ∈ ℕ → ( 𝐻𝑧 ) = ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) )
99 incom ( ( (,) ‘ ( 𝐹𝑧 ) ) ∩ ( (,) ‘ ( 𝐺𝐽 ) ) ) = ( ( (,) ‘ ( 𝐺𝐽 ) ) ∩ ( (,) ‘ ( 𝐹𝑧 ) ) )
100 98 99 eqtrdi ( 𝑧 ∈ ℕ → ( 𝐻𝑧 ) = ( ( (,) ‘ ( 𝐺𝐽 ) ) ∩ ( (,) ‘ ( 𝐹𝑧 ) ) ) )
101 100 iuneq2i 𝑧 ∈ ℕ ( 𝐻𝑧 ) = 𝑧 ∈ ℕ ( ( (,) ‘ ( 𝐺𝐽 ) ) ∩ ( (,) ‘ ( 𝐹𝑧 ) ) )
102 iunin2 𝑧 ∈ ℕ ( ( (,) ‘ ( 𝐺𝐽 ) ) ∩ ( (,) ‘ ( 𝐹𝑧 ) ) ) = ( ( (,) ‘ ( 𝐺𝐽 ) ) ∩ 𝑧 ∈ ℕ ( (,) ‘ ( 𝐹𝑧 ) ) )
103 101 102 eqtri 𝑧 ∈ ℕ ( 𝐻𝑧 ) = ( ( (,) ‘ ( 𝐺𝐽 ) ) ∩ 𝑧 ∈ ℕ ( (,) ‘ ( 𝐹𝑧 ) ) )
104 17 11 fmptd ( ( 𝜑𝐽 ∈ ℕ ) → 𝐻 : ℕ ⟶ ran (,) )
105 104 ffnd ( ( 𝜑𝐽 ∈ ℕ ) → 𝐻 Fn ℕ )
106 fniunfv ( 𝐻 Fn ℕ → 𝑧 ∈ ℕ ( 𝐻𝑧 ) = ran 𝐻 )
107 105 106 syl ( ( 𝜑𝐽 ∈ ℕ ) → 𝑧 ∈ ℕ ( 𝐻𝑧 ) = ran 𝐻 )
108 103 107 eqtr3id ( ( 𝜑𝐽 ∈ ℕ ) → ( ( (,) ‘ ( 𝐺𝐽 ) ) ∩ 𝑧 ∈ ℕ ( (,) ‘ ( 𝐹𝑧 ) ) ) = ran 𝐻 )
109 1 adantr ( ( 𝜑𝐽 ∈ ℕ ) → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
110 fvco3 ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑧 ∈ ℕ ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑧 ) = ( (,) ‘ ( 𝐹𝑧 ) ) )
111 109 110 sylan ( ( ( 𝜑𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑧 ) = ( (,) ‘ ( 𝐹𝑧 ) ) )
112 111 iuneq2dv ( ( 𝜑𝐽 ∈ ℕ ) → 𝑧 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑧 ) = 𝑧 ∈ ℕ ( (,) ‘ ( 𝐹𝑧 ) ) )
113 ffn ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → (,) Fn ( ℝ* × ℝ* ) )
114 87 113 ax-mp (,) Fn ( ℝ* × ℝ* )
115 fss ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ* × ℝ* ) ) → 𝐹 : ℕ ⟶ ( ℝ* × ℝ* ) )
116 109 85 115 sylancl ( ( 𝜑𝐽 ∈ ℕ ) → 𝐹 : ℕ ⟶ ( ℝ* × ℝ* ) )
117 fnfco ( ( (,) Fn ( ℝ* × ℝ* ) ∧ 𝐹 : ℕ ⟶ ( ℝ* × ℝ* ) ) → ( (,) ∘ 𝐹 ) Fn ℕ )
118 114 116 117 sylancr ( ( 𝜑𝐽 ∈ ℕ ) → ( (,) ∘ 𝐹 ) Fn ℕ )
119 fniunfv ( ( (,) ∘ 𝐹 ) Fn ℕ → 𝑧 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑧 ) = ran ( (,) ∘ 𝐹 ) )
120 118 119 syl ( ( 𝜑𝐽 ∈ ℕ ) → 𝑧 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑧 ) = ran ( (,) ∘ 𝐹 ) )
121 120 4 eqtr4di ( ( 𝜑𝐽 ∈ ℕ ) → 𝑧 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑧 ) = 𝐴 )
122 112 121 eqtr3d ( ( 𝜑𝐽 ∈ ℕ ) → 𝑧 ∈ ℕ ( (,) ‘ ( 𝐹𝑧 ) ) = 𝐴 )
123 122 ineq2d ( ( 𝜑𝐽 ∈ ℕ ) → ( ( (,) ‘ ( 𝐺𝐽 ) ) ∩ 𝑧 ∈ ℕ ( (,) ‘ ( 𝐹𝑧 ) ) ) = ( ( (,) ‘ ( 𝐺𝐽 ) ) ∩ 𝐴 ) )
124 94 108 123 3eqtr2d ( ( 𝜑𝐽 ∈ ℕ ) → ran ( (,) ∘ ( 𝐾𝐻 ) ) = ( ( (,) ‘ ( 𝐺𝐽 ) ) ∩ 𝐴 ) )
125 124 fveq2d ( ( 𝜑𝐽 ∈ ℕ ) → ( vol* ‘ ran ( (,) ∘ ( 𝐾𝐻 ) ) ) = ( vol* ‘ ( ( (,) ‘ ( 𝐺𝐽 ) ) ∩ 𝐴 ) ) )
126 82 125 eqtr3d ( ( 𝜑𝐽 ∈ ℕ ) → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) , ℝ* , < ) = ( vol* ‘ ( ( (,) ‘ ( 𝐺𝐽 ) ) ∩ 𝐴 ) ) )
127 inss1 ( ( (,) ‘ ( 𝐺𝐽 ) ) ∩ 𝐴 ) ⊆ ( (,) ‘ ( 𝐺𝐽 ) )
128 ovolsscl ( ( ( ( (,) ‘ ( 𝐺𝐽 ) ) ∩ 𝐴 ) ⊆ ( (,) ‘ ( 𝐺𝐽 ) ) ∧ ( (,) ‘ ( 𝐺𝐽 ) ) ⊆ ℝ ∧ ( vol* ‘ ( (,) ‘ ( 𝐺𝐽 ) ) ) ∈ ℝ ) → ( vol* ‘ ( ( (,) ‘ ( 𝐺𝐽 ) ) ∩ 𝐴 ) ) ∈ ℝ )
129 127 34 44 128 mp3an2i ( ( 𝜑𝐽 ∈ ℕ ) → ( vol* ‘ ( ( (,) ‘ ( 𝐺𝐽 ) ) ∩ 𝐴 ) ) ∈ ℝ )
130 126 129 eqeltrd ( ( 𝜑𝐽 ∈ ℕ ) → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) , ℝ* , < ) ∈ ℝ )
131 51 14 ovolsf ( ( 𝐾𝐻 ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) : ℕ ⟶ ( 0 [,) +∞ ) )
132 50 131 syl ( ( 𝜑𝐽 ∈ ℕ ) → seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) : ℕ ⟶ ( 0 [,) +∞ ) )
133 132 frnd ( ( 𝜑𝐽 ∈ ℕ ) → ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) ⊆ ( 0 [,) +∞ ) )
134 icossxr ( 0 [,) +∞ ) ⊆ ℝ*
135 133 134 sstrdi ( ( 𝜑𝐽 ∈ ℕ ) → ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) ⊆ ℝ* )
136 132 ffnd ( ( 𝜑𝐽 ∈ ℕ ) → seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) Fn ℕ )
137 fnfvelrn ( ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) Fn ℕ ∧ 𝑦 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) ‘ 𝑦 ) ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) )
138 136 137 sylan ( ( ( 𝜑𝐽 ∈ ℕ ) ∧ 𝑦 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) ‘ 𝑦 ) ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) )
139 supxrub ( ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) ⊆ ℝ* ∧ ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) ‘ 𝑦 ) ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) ‘ 𝑦 ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) , ℝ* , < ) )
140 135 138 139 syl2an2r ( ( ( 𝜑𝐽 ∈ ℕ ) ∧ 𝑦 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) ‘ 𝑦 ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) , ℝ* , < ) )
141 140 ralrimiva ( ( 𝜑𝐽 ∈ ℕ ) → ∀ 𝑦 ∈ ℕ ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) ‘ 𝑦 ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) , ℝ* , < ) )
142 brralrspcev ( ( sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) , ℝ* , < ) ∈ ℝ ∧ ∀ 𝑦 ∈ ℕ ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) ‘ 𝑦 ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) , ℝ* , < ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℕ ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) ‘ 𝑦 ) ≤ 𝑥 )
143 130 141 142 syl2anc ( ( 𝜑𝐽 ∈ ℕ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℕ ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) ‘ 𝑦 ) ≤ 𝑥 )
144 13 14 15 16 57 58 143 isumsup2 ( ( 𝜑𝐽 ∈ ℕ ) → seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) ⇝ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) , ℝ , < ) )
145 51 ovolfs2 ( ( 𝐾𝐻 ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) = ( ( vol* ∘ (,) ) ∘ ( 𝐾𝐻 ) ) )
146 50 145 syl ( ( 𝜑𝐽 ∈ ℕ ) → ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) = ( ( vol* ∘ (,) ) ∘ ( 𝐾𝐻 ) ) )
147 coass ( ( vol* ∘ (,) ) ∘ ( 𝐾𝐻 ) ) = ( vol* ∘ ( (,) ∘ ( 𝐾𝐻 ) ) )
148 92 coeq2d ( ( 𝜑𝐽 ∈ ℕ ) → ( vol* ∘ ( (,) ∘ ( 𝐾𝐻 ) ) ) = ( vol* ∘ 𝐻 ) )
149 147 148 syl5eq ( ( 𝜑𝐽 ∈ ℕ ) → ( ( vol* ∘ (,) ) ∘ ( 𝐾𝐻 ) ) = ( vol* ∘ 𝐻 ) )
150 146 149 eqtrd ( ( 𝜑𝐽 ∈ ℕ ) → ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) = ( vol* ∘ 𝐻 ) )
151 150 seqeq3d ( ( 𝜑𝐽 ∈ ℕ ) → seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) = seq 1 ( + , ( vol* ∘ 𝐻 ) ) )
152 rge0ssre ( 0 [,) +∞ ) ⊆ ℝ
153 133 152 sstrdi ( ( 𝜑𝐽 ∈ ℕ ) → ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) ⊆ ℝ )
154 1nn 1 ∈ ℕ
155 132 fdmd ( ( 𝜑𝐽 ∈ ℕ ) → dom seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) = ℕ )
156 154 155 eleqtrrid ( ( 𝜑𝐽 ∈ ℕ ) → 1 ∈ dom seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) )
157 156 ne0d ( ( 𝜑𝐽 ∈ ℕ ) → dom seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) ≠ ∅ )
158 dm0rn0 ( dom seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) = ∅ ↔ ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) = ∅ )
159 158 necon3bii ( dom seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) ≠ ∅ ↔ ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) ≠ ∅ )
160 157 159 sylib ( ( 𝜑𝐽 ∈ ℕ ) → ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) ≠ ∅ )
161 breq1 ( 𝑧 = ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) ‘ 𝑦 ) → ( 𝑧𝑥 ↔ ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) ‘ 𝑦 ) ≤ 𝑥 ) )
162 161 ralrn ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) Fn ℕ → ( ∀ 𝑧 ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) 𝑧𝑥 ↔ ∀ 𝑦 ∈ ℕ ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) ‘ 𝑦 ) ≤ 𝑥 ) )
163 136 162 syl ( ( 𝜑𝐽 ∈ ℕ ) → ( ∀ 𝑧 ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) 𝑧𝑥 ↔ ∀ 𝑦 ∈ ℕ ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) ‘ 𝑦 ) ≤ 𝑥 ) )
164 163 rexbidv ( ( 𝜑𝐽 ∈ ℕ ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) 𝑧𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℕ ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) ‘ 𝑦 ) ≤ 𝑥 ) )
165 143 164 mpbird ( ( 𝜑𝐽 ∈ ℕ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) 𝑧𝑥 )
166 supxrre ( ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) ⊆ ℝ ∧ ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) 𝑧𝑥 ) → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) , ℝ* , < ) = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) , ℝ , < ) )
167 153 160 165 166 syl3anc ( ( 𝜑𝐽 ∈ ℕ ) → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) , ℝ* , < ) = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) , ℝ , < ) )
168 167 126 eqtr3d ( ( 𝜑𝐽 ∈ ℕ ) → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾𝐻 ) ) ) , ℝ , < ) = ( vol* ‘ ( ( (,) ‘ ( 𝐺𝐽 ) ) ∩ 𝐴 ) ) )
169 144 151 168 3brtr3d ( ( 𝜑𝐽 ∈ ℕ ) → seq 1 ( + , ( vol* ∘ 𝐻 ) ) ⇝ ( vol* ‘ ( ( (,) ‘ ( 𝐺𝐽 ) ) ∩ 𝐴 ) ) )