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 eqtrid ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( ( 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* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ∩ 𝐴 ) ) )