Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  uniioombllem2 Structured version   Visualization version   GIF version

Theorem uniioombllem2 23397
 Description: Lemma for uniioombl 23403. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by Mario Carneiro, 11-Dec-2016.) (Revised by AV, 13-Sep-2020.)
Hypotheses
Ref Expression
uniioombl.1 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
uniioombl.2 (𝜑Disj 𝑥 ∈ ℕ ((,)‘(𝐹𝑥)))
uniioombl.3 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
uniioombl.a 𝐴 = ran ((,) ∘ 𝐹)
uniioombl.e (𝜑 → (vol*‘𝐸) ∈ ℝ)
uniioombl.c (𝜑𝐶 ∈ ℝ+)
uniioombl.g (𝜑𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
uniioombl.s (𝜑𝐸 ran ((,) ∘ 𝐺))
uniioombl.t 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
uniioombl.v (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))
uniioombllem2.h 𝐻 = (𝑧 ∈ ℕ ↦ (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽))))
uniioombllem2.k 𝐾 = (𝑥 ∈ ran (,) ↦ if(𝑥 = ∅, ⟨0, 0⟩, ⟨inf(𝑥, ℝ*, < ), sup(𝑥, ℝ*, < )⟩))
Assertion
Ref Expression
uniioombllem2 ((𝜑𝐽 ∈ ℕ) → seq1( + , (vol* ∘ 𝐻)) ⇝ (vol*‘(((,)‘(𝐺𝐽)) ∩ 𝐴)))
Distinct variable groups:   𝑥,𝑧,𝐹   𝑥,𝐺,𝑧   𝑥,𝐾,𝑧   𝑥,𝐴,𝑧   𝑥,𝐶,𝑧   𝑥,𝐻,𝑧   𝑥,𝐽,𝑧   𝜑,𝑥,𝑧   𝑥,𝑇,𝑧
Allowed substitution hints:   𝑆(𝑥,𝑧)   𝐸(𝑥,𝑧)

Proof of Theorem uniioombllem2
Dummy variables 𝑛 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 11761 . . 3 ℕ = (ℤ‘1)
2 eqid 2651 . . 3 seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))) = seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻)))
3 1zzd 11446 . . 3 ((𝜑𝐽 ∈ ℕ) → 1 ∈ ℤ)
4 eqidd 2652 . . 3 (((𝜑𝐽 ∈ ℕ) ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ (𝐾𝐻))‘𝑛) = (((abs ∘ − ) ∘ (𝐾𝐻))‘𝑛))
5 uniioombl.1 . . . . . . . . . . 11 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
6 uniioombl.2 . . . . . . . . . . 11 (𝜑Disj 𝑥 ∈ ℕ ((,)‘(𝐹𝑥)))
7 uniioombl.3 . . . . . . . . . . 11 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
8 uniioombl.a . . . . . . . . . . 11 𝐴 = ran ((,) ∘ 𝐹)
9 uniioombl.e . . . . . . . . . . 11 (𝜑 → (vol*‘𝐸) ∈ ℝ)
10 uniioombl.c . . . . . . . . . . 11 (𝜑𝐶 ∈ ℝ+)
11 uniioombl.g . . . . . . . . . . 11 (𝜑𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
12 uniioombl.s . . . . . . . . . . 11 (𝜑𝐸 ran ((,) ∘ 𝐺))
13 uniioombl.t . . . . . . . . . . 11 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
14 uniioombl.v . . . . . . . . . . 11 (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))
155, 6, 7, 8, 9, 10, 11, 12, 13, 14uniioombllem2a 23396 . . . . . . . . . 10 (((𝜑𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽))) ∈ ran (,))
16 inss2 3867 . . . . . . . . . . . . 13 (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽))) ⊆ ((,)‘(𝐺𝐽))
1716a1i 11 . . . . . . . . . . . 12 ((𝜑𝐽 ∈ ℕ) → (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽))) ⊆ ((,)‘(𝐺𝐽)))
18 inss2 3867 . . . . . . . . . . . . . . . . 17 ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
1911ffvelrnda 6399 . . . . . . . . . . . . . . . . 17 ((𝜑𝐽 ∈ ℕ) → (𝐺𝐽) ∈ ( ≤ ∩ (ℝ × ℝ)))
2018, 19sseldi 3634 . . . . . . . . . . . . . . . 16 ((𝜑𝐽 ∈ ℕ) → (𝐺𝐽) ∈ (ℝ × ℝ))
21 1st2nd2 7249 . . . . . . . . . . . . . . . 16 ((𝐺𝐽) ∈ (ℝ × ℝ) → (𝐺𝐽) = ⟨(1st ‘(𝐺𝐽)), (2nd ‘(𝐺𝐽))⟩)
2220, 21syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝐽 ∈ ℕ) → (𝐺𝐽) = ⟨(1st ‘(𝐺𝐽)), (2nd ‘(𝐺𝐽))⟩)
2322fveq2d 6233 . . . . . . . . . . . . . 14 ((𝜑𝐽 ∈ ℕ) → ((,)‘(𝐺𝐽)) = ((,)‘⟨(1st ‘(𝐺𝐽)), (2nd ‘(𝐺𝐽))⟩))
24 df-ov 6693 . . . . . . . . . . . . . 14 ((1st ‘(𝐺𝐽))(,)(2nd ‘(𝐺𝐽))) = ((,)‘⟨(1st ‘(𝐺𝐽)), (2nd ‘(𝐺𝐽))⟩)
2523, 24syl6eqr 2703 . . . . . . . . . . . . 13 ((𝜑𝐽 ∈ ℕ) → ((,)‘(𝐺𝐽)) = ((1st ‘(𝐺𝐽))(,)(2nd ‘(𝐺𝐽))))
26 ioossre 12273 . . . . . . . . . . . . 13 ((1st ‘(𝐺𝐽))(,)(2nd ‘(𝐺𝐽))) ⊆ ℝ
2725, 26syl6eqss 3688 . . . . . . . . . . . 12 ((𝜑𝐽 ∈ ℕ) → ((,)‘(𝐺𝐽)) ⊆ ℝ)
2825fveq2d 6233 . . . . . . . . . . . . . 14 ((𝜑𝐽 ∈ ℕ) → (vol*‘((,)‘(𝐺𝐽))) = (vol*‘((1st ‘(𝐺𝐽))(,)(2nd ‘(𝐺𝐽)))))
29 ovolfcl 23281 . . . . . . . . . . . . . . . 16 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐽 ∈ ℕ) → ((1st ‘(𝐺𝐽)) ∈ ℝ ∧ (2nd ‘(𝐺𝐽)) ∈ ℝ ∧ (1st ‘(𝐺𝐽)) ≤ (2nd ‘(𝐺𝐽))))
3011, 29sylan 487 . . . . . . . . . . . . . . 15 ((𝜑𝐽 ∈ ℕ) → ((1st ‘(𝐺𝐽)) ∈ ℝ ∧ (2nd ‘(𝐺𝐽)) ∈ ℝ ∧ (1st ‘(𝐺𝐽)) ≤ (2nd ‘(𝐺𝐽))))
31 ovolioo 23382 . . . . . . . . . . . . . . 15 (((1st ‘(𝐺𝐽)) ∈ ℝ ∧ (2nd ‘(𝐺𝐽)) ∈ ℝ ∧ (1st ‘(𝐺𝐽)) ≤ (2nd ‘(𝐺𝐽))) → (vol*‘((1st ‘(𝐺𝐽))(,)(2nd ‘(𝐺𝐽)))) = ((2nd ‘(𝐺𝐽)) − (1st ‘(𝐺𝐽))))
3230, 31syl 17 . . . . . . . . . . . . . 14 ((𝜑𝐽 ∈ ℕ) → (vol*‘((1st ‘(𝐺𝐽))(,)(2nd ‘(𝐺𝐽)))) = ((2nd ‘(𝐺𝐽)) − (1st ‘(𝐺𝐽))))
3328, 32eqtrd 2685 . . . . . . . . . . . . 13 ((𝜑𝐽 ∈ ℕ) → (vol*‘((,)‘(𝐺𝐽))) = ((2nd ‘(𝐺𝐽)) − (1st ‘(𝐺𝐽))))
3430simp2d 1094 . . . . . . . . . . . . . 14 ((𝜑𝐽 ∈ ℕ) → (2nd ‘(𝐺𝐽)) ∈ ℝ)
3530simp1d 1093 . . . . . . . . . . . . . 14 ((𝜑𝐽 ∈ ℕ) → (1st ‘(𝐺𝐽)) ∈ ℝ)
3634, 35resubcld 10496 . . . . . . . . . . . . 13 ((𝜑𝐽 ∈ ℕ) → ((2nd ‘(𝐺𝐽)) − (1st ‘(𝐺𝐽))) ∈ ℝ)
3733, 36eqeltrd 2730 . . . . . . . . . . . 12 ((𝜑𝐽 ∈ ℕ) → (vol*‘((,)‘(𝐺𝐽))) ∈ ℝ)
38 ovolsscl 23300 . . . . . . . . . . . 12 (((((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽))) ⊆ ((,)‘(𝐺𝐽)) ∧ ((,)‘(𝐺𝐽)) ⊆ ℝ ∧ (vol*‘((,)‘(𝐺𝐽))) ∈ ℝ) → (vol*‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽)))) ∈ ℝ)
3917, 27, 37, 38syl3anc 1366 . . . . . . . . . . 11 ((𝜑𝐽 ∈ ℕ) → (vol*‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽)))) ∈ ℝ)
4039adantr 480 . . . . . . . . . 10 (((𝜑𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (vol*‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽)))) ∈ ℝ)
41 uniioombllem2.k . . . . . . . . . . 11 𝐾 = (𝑥 ∈ ran (,) ↦ if(𝑥 = ∅, ⟨0, 0⟩, ⟨inf(𝑥, ℝ*, < ), sup(𝑥, ℝ*, < )⟩))
4241ioorcl 23391 . . . . . . . . . 10 (((((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽))) ∈ ran (,) ∧ (vol*‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽)))) ∈ ℝ) → (𝐾‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽)))) ∈ ( ≤ ∩ (ℝ × ℝ)))
4315, 40, 42syl2anc 694 . . . . . . . . 9 (((𝜑𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (𝐾‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽)))) ∈ ( ≤ ∩ (ℝ × ℝ)))
44 eqid 2651 . . . . . . . . 9 (𝑧 ∈ ℕ ↦ (𝐾‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽))))) = (𝑧 ∈ ℕ ↦ (𝐾‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽)))))
4543, 44fmptd 6425 . . . . . . . 8 ((𝜑𝐽 ∈ ℕ) → (𝑧 ∈ ℕ ↦ (𝐾‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽))))):ℕ⟶( ≤ ∩ (ℝ × ℝ)))
46 uniioombllem2.h . . . . . . . . . . 11 𝐻 = (𝑧 ∈ ℕ ↦ (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽))))
4746a1i 11 . . . . . . . . . 10 ((𝜑𝐽 ∈ ℕ) → 𝐻 = (𝑧 ∈ ℕ ↦ (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽)))))
4841ioorf 23387 . . . . . . . . . . . 12 𝐾:ran (,)⟶( ≤ ∩ (ℝ* × ℝ*))
4948a1i 11 . . . . . . . . . . 11 ((𝜑𝐽 ∈ ℕ) → 𝐾:ran (,)⟶( ≤ ∩ (ℝ* × ℝ*)))
5049feqmptd 6288 . . . . . . . . . 10 ((𝜑𝐽 ∈ ℕ) → 𝐾 = (𝑦 ∈ ran (,) ↦ (𝐾𝑦)))
51 fveq2 6229 . . . . . . . . . 10 (𝑦 = (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽))) → (𝐾𝑦) = (𝐾‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽)))))
5215, 47, 50, 51fmptco 6436 . . . . . . . . 9 ((𝜑𝐽 ∈ ℕ) → (𝐾𝐻) = (𝑧 ∈ ℕ ↦ (𝐾‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽))))))
5352feq1d 6068 . . . . . . . 8 ((𝜑𝐽 ∈ ℕ) → ((𝐾𝐻):ℕ⟶( ≤ ∩ (ℝ × ℝ)) ↔ (𝑧 ∈ ℕ ↦ (𝐾‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽))))):ℕ⟶( ≤ ∩ (ℝ × ℝ))))
5445, 53mpbird 247 . . . . . . 7 ((𝜑𝐽 ∈ ℕ) → (𝐾𝐻):ℕ⟶( ≤ ∩ (ℝ × ℝ)))
55 eqid 2651 . . . . . . . 8 ((abs ∘ − ) ∘ (𝐾𝐻)) = ((abs ∘ − ) ∘ (𝐾𝐻))
5655ovolfsf 23286 . . . . . . 7 ((𝐾𝐻):ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ (𝐾𝐻)):ℕ⟶(0[,)+∞))
5754, 56syl 17 . . . . . 6 ((𝜑𝐽 ∈ ℕ) → ((abs ∘ − ) ∘ (𝐾𝐻)):ℕ⟶(0[,)+∞))
5857ffvelrnda 6399 . . . . 5 (((𝜑𝐽 ∈ ℕ) ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ (𝐾𝐻))‘𝑛) ∈ (0[,)+∞))
59 elrege0 12316 . . . . 5 ((((abs ∘ − ) ∘ (𝐾𝐻))‘𝑛) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ (𝐾𝐻))‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ (𝐾𝐻))‘𝑛)))
6058, 59sylib 208 . . . 4 (((𝜑𝐽 ∈ ℕ) ∧ 𝑛 ∈ ℕ) → ((((abs ∘ − ) ∘ (𝐾𝐻))‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ (𝐾𝐻))‘𝑛)))
6160simpld 474 . . 3 (((𝜑𝐽 ∈ ℕ) ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ (𝐾𝐻))‘𝑛) ∈ ℝ)
6260simprd 478 . . 3 (((𝜑𝐽 ∈ ℕ) ∧ 𝑛 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ (𝐾𝐻))‘𝑛))
6352fveq1d 6231 . . . . . . . . . . . . . . 15 ((𝜑𝐽 ∈ ℕ) → ((𝐾𝐻)‘𝑧) = ((𝑧 ∈ ℕ ↦ (𝐾‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽)))))‘𝑧))
64 fvex 6239 . . . . . . . . . . . . . . . 16 (𝐾‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽)))) ∈ V
6544fvmpt2 6330 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ ℕ ∧ (𝐾‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽)))) ∈ V) → ((𝑧 ∈ ℕ ↦ (𝐾‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽)))))‘𝑧) = (𝐾‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽)))))
6664, 65mpan2 707 . . . . . . . . . . . . . . 15 (𝑧 ∈ ℕ → ((𝑧 ∈ ℕ ↦ (𝐾‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽)))))‘𝑧) = (𝐾‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽)))))
6763, 66sylan9eq 2705 . . . . . . . . . . . . . 14 (((𝜑𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → ((𝐾𝐻)‘𝑧) = (𝐾‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽)))))
6867fveq2d 6233 . . . . . . . . . . . . 13 (((𝜑𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → ((,)‘((𝐾𝐻)‘𝑧)) = ((,)‘(𝐾‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽))))))
6941ioorinv 23390 . . . . . . . . . . . . . 14 ((((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽))) ∈ ran (,) → ((,)‘(𝐾‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽))))) = (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽))))
7015, 69syl 17 . . . . . . . . . . . . 13 (((𝜑𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → ((,)‘(𝐾‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽))))) = (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽))))
7168, 70eqtrd 2685 . . . . . . . . . . . 12 (((𝜑𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → ((,)‘((𝐾𝐻)‘𝑧)) = (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽))))
7271ralrimiva 2995 . . . . . . . . . . 11 ((𝜑𝐽 ∈ ℕ) → ∀𝑧 ∈ ℕ ((,)‘((𝐾𝐻)‘𝑧)) = (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽))))
73 fveq2 6229 . . . . . . . . . . . . . 14 (𝑧 = 𝑥 → ((𝐾𝐻)‘𝑧) = ((𝐾𝐻)‘𝑥))
7473fveq2d 6233 . . . . . . . . . . . . 13 (𝑧 = 𝑥 → ((,)‘((𝐾𝐻)‘𝑧)) = ((,)‘((𝐾𝐻)‘𝑥)))
75 fveq2 6229 . . . . . . . . . . . . . . 15 (𝑧 = 𝑥 → (𝐹𝑧) = (𝐹𝑥))
7675fveq2d 6233 . . . . . . . . . . . . . 14 (𝑧 = 𝑥 → ((,)‘(𝐹𝑧)) = ((,)‘(𝐹𝑥)))
7776ineq1d 3846 . . . . . . . . . . . . 13 (𝑧 = 𝑥 → (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽))) = (((,)‘(𝐹𝑥)) ∩ ((,)‘(𝐺𝐽))))
7874, 77eqeq12d 2666 . . . . . . . . . . . 12 (𝑧 = 𝑥 → (((,)‘((𝐾𝐻)‘𝑧)) = (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽))) ↔ ((,)‘((𝐾𝐻)‘𝑥)) = (((,)‘(𝐹𝑥)) ∩ ((,)‘(𝐺𝐽)))))
7978rspccva 3339 . . . . . . . . . . 11 ((∀𝑧 ∈ ℕ ((,)‘((𝐾𝐻)‘𝑧)) = (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽))) ∧ 𝑥 ∈ ℕ) → ((,)‘((𝐾𝐻)‘𝑥)) = (((,)‘(𝐹𝑥)) ∩ ((,)‘(𝐺𝐽))))
8072, 79sylan 487 . . . . . . . . . 10 (((𝜑𝐽 ∈ ℕ) ∧ 𝑥 ∈ ℕ) → ((,)‘((𝐾𝐻)‘𝑥)) = (((,)‘(𝐹𝑥)) ∩ ((,)‘(𝐺𝐽))))
81 inss1 3866 . . . . . . . . . 10 (((,)‘(𝐹𝑥)) ∩ ((,)‘(𝐺𝐽))) ⊆ ((,)‘(𝐹𝑥))
8280, 81syl6eqss 3688 . . . . . . . . 9 (((𝜑𝐽 ∈ ℕ) ∧ 𝑥 ∈ ℕ) → ((,)‘((𝐾𝐻)‘𝑥)) ⊆ ((,)‘(𝐹𝑥)))
8382ralrimiva 2995 . . . . . . . 8 ((𝜑𝐽 ∈ ℕ) → ∀𝑥 ∈ ℕ ((,)‘((𝐾𝐻)‘𝑥)) ⊆ ((,)‘(𝐹𝑥)))
846adantr 480 . . . . . . . 8 ((𝜑𝐽 ∈ ℕ) → Disj 𝑥 ∈ ℕ ((,)‘(𝐹𝑥)))
85 disjss2 4655 . . . . . . . 8 (∀𝑥 ∈ ℕ ((,)‘((𝐾𝐻)‘𝑥)) ⊆ ((,)‘(𝐹𝑥)) → (Disj 𝑥 ∈ ℕ ((,)‘(𝐹𝑥)) → Disj 𝑥 ∈ ℕ ((,)‘((𝐾𝐻)‘𝑥))))
8683, 84, 85sylc 65 . . . . . . 7 ((𝜑𝐽 ∈ ℕ) → Disj 𝑥 ∈ ℕ ((,)‘((𝐾𝐻)‘𝑥)))
8754, 86, 2uniioovol 23393 . . . . . 6 ((𝜑𝐽 ∈ ℕ) → (vol*‘ ran ((,) ∘ (𝐾𝐻))) = sup(ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))), ℝ*, < ))
8870mpteq2dva 4777 . . . . . . . . . . 11 ((𝜑𝐽 ∈ ℕ) → (𝑧 ∈ ℕ ↦ ((,)‘(𝐾‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽)))))) = (𝑧 ∈ ℕ ↦ (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽)))))
89 rexpssxrxp 10122 . . . . . . . . . . . . . 14 (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
9018, 89sstri 3645 . . . . . . . . . . . . 13 ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ* × ℝ*)
9190, 43sseldi 3634 . . . . . . . . . . . 12 (((𝜑𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (𝐾‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽)))) ∈ (ℝ* × ℝ*))
92 ioof 12309 . . . . . . . . . . . . . 14 (,):(ℝ* × ℝ*)⟶𝒫 ℝ
9392a1i 11 . . . . . . . . . . . . 13 ((𝜑𝐽 ∈ ℕ) → (,):(ℝ* × ℝ*)⟶𝒫 ℝ)
9493feqmptd 6288 . . . . . . . . . . . 12 ((𝜑𝐽 ∈ ℕ) → (,) = (𝑦 ∈ (ℝ* × ℝ*) ↦ ((,)‘𝑦)))
95 fveq2 6229 . . . . . . . . . . . 12 (𝑦 = (𝐾‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽)))) → ((,)‘𝑦) = ((,)‘(𝐾‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽))))))
9691, 52, 94, 95fmptco 6436 . . . . . . . . . . 11 ((𝜑𝐽 ∈ ℕ) → ((,) ∘ (𝐾𝐻)) = (𝑧 ∈ ℕ ↦ ((,)‘(𝐾‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽)))))))
9788, 96, 473eqtr4d 2695 . . . . . . . . . 10 ((𝜑𝐽 ∈ ℕ) → ((,) ∘ (𝐾𝐻)) = 𝐻)
9897rneqd 5385 . . . . . . . . 9 ((𝜑𝐽 ∈ ℕ) → ran ((,) ∘ (𝐾𝐻)) = ran 𝐻)
9998unieqd 4478 . . . . . . . 8 ((𝜑𝐽 ∈ ℕ) → ran ((,) ∘ (𝐾𝐻)) = ran 𝐻)
100 fvex 6239 . . . . . . . . . . . . . 14 ((,)‘(𝐹𝑧)) ∈ V
101100inex1 4832 . . . . . . . . . . . . 13 (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽))) ∈ V
10246fvmpt2 6330 . . . . . . . . . . . . 13 ((𝑧 ∈ ℕ ∧ (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽))) ∈ V) → (𝐻𝑧) = (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽))))
103101, 102mpan2 707 . . . . . . . . . . . 12 (𝑧 ∈ ℕ → (𝐻𝑧) = (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽))))
104 incom 3838 . . . . . . . . . . . 12 (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝐽))) = (((,)‘(𝐺𝐽)) ∩ ((,)‘(𝐹𝑧)))
105103, 104syl6eq 2701 . . . . . . . . . . 11 (𝑧 ∈ ℕ → (𝐻𝑧) = (((,)‘(𝐺𝐽)) ∩ ((,)‘(𝐹𝑧))))
106105iuneq2i 4571 . . . . . . . . . 10 𝑧 ∈ ℕ (𝐻𝑧) = 𝑧 ∈ ℕ (((,)‘(𝐺𝐽)) ∩ ((,)‘(𝐹𝑧)))
107 iunin2 4616 . . . . . . . . . 10 𝑧 ∈ ℕ (((,)‘(𝐺𝐽)) ∩ ((,)‘(𝐹𝑧))) = (((,)‘(𝐺𝐽)) ∩ 𝑧 ∈ ℕ ((,)‘(𝐹𝑧)))
108106, 107eqtri 2673 . . . . . . . . 9 𝑧 ∈ ℕ (𝐻𝑧) = (((,)‘(𝐺𝐽)) ∩ 𝑧 ∈ ℕ ((,)‘(𝐹𝑧)))
10915, 46fmptd 6425 . . . . . . . . . . 11 ((𝜑𝐽 ∈ ℕ) → 𝐻:ℕ⟶ran (,))
110 ffn 6083 . . . . . . . . . . 11 (𝐻:ℕ⟶ran (,) → 𝐻 Fn ℕ)
111109, 110syl 17 . . . . . . . . . 10 ((𝜑𝐽 ∈ ℕ) → 𝐻 Fn ℕ)
112 fniunfv 6545 . . . . . . . . . 10 (𝐻 Fn ℕ → 𝑧 ∈ ℕ (𝐻𝑧) = ran 𝐻)
113111, 112syl 17 . . . . . . . . 9 ((𝜑𝐽 ∈ ℕ) → 𝑧 ∈ ℕ (𝐻𝑧) = ran 𝐻)
114108, 113syl5eqr 2699 . . . . . . . 8 ((𝜑𝐽 ∈ ℕ) → (((,)‘(𝐺𝐽)) ∩ 𝑧 ∈ ℕ ((,)‘(𝐹𝑧))) = ran 𝐻)
1155adantr 480 . . . . . . . . . . . 12 ((𝜑𝐽 ∈ ℕ) → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
116 fvco3 6314 . . . . . . . . . . . 12 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑧 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑧) = ((,)‘(𝐹𝑧)))
117115, 116sylan 487 . . . . . . . . . . 11 (((𝜑𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑧) = ((,)‘(𝐹𝑧)))
118117iuneq2dv 4574 . . . . . . . . . 10 ((𝜑𝐽 ∈ ℕ) → 𝑧 ∈ ℕ (((,) ∘ 𝐹)‘𝑧) = 𝑧 ∈ ℕ ((,)‘(𝐹𝑧)))
119 ffn 6083 . . . . . . . . . . . . . 14 ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → (,) Fn (ℝ* × ℝ*))
12092, 119ax-mp 5 . . . . . . . . . . . . 13 (,) Fn (ℝ* × ℝ*)
121 fss 6094 . . . . . . . . . . . . . 14 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ* × ℝ*)) → 𝐹:ℕ⟶(ℝ* × ℝ*))
122115, 90, 121sylancl 695 . . . . . . . . . . . . 13 ((𝜑𝐽 ∈ ℕ) → 𝐹:ℕ⟶(ℝ* × ℝ*))
123 fnfco 6107 . . . . . . . . . . . . 13 (((,) Fn (ℝ* × ℝ*) ∧ 𝐹:ℕ⟶(ℝ* × ℝ*)) → ((,) ∘ 𝐹) Fn ℕ)
124120, 122, 123sylancr 696 . . . . . . . . . . . 12 ((𝜑𝐽 ∈ ℕ) → ((,) ∘ 𝐹) Fn ℕ)
125 fniunfv 6545 . . . . . . . . . . . 12 (((,) ∘ 𝐹) Fn ℕ → 𝑧 ∈ ℕ (((,) ∘ 𝐹)‘𝑧) = ran ((,) ∘ 𝐹))
126124, 125syl 17 . . . . . . . . . . 11 ((𝜑𝐽 ∈ ℕ) → 𝑧 ∈ ℕ (((,) ∘ 𝐹)‘𝑧) = ran ((,) ∘ 𝐹))
127126, 8syl6eqr 2703 . . . . . . . . . 10 ((𝜑𝐽 ∈ ℕ) → 𝑧 ∈ ℕ (((,) ∘ 𝐹)‘𝑧) = 𝐴)
128118, 127eqtr3d 2687 . . . . . . . . 9 ((𝜑𝐽 ∈ ℕ) → 𝑧 ∈ ℕ ((,)‘(𝐹𝑧)) = 𝐴)
129128ineq2d 3847 . . . . . . . 8 ((𝜑𝐽 ∈ ℕ) → (((,)‘(𝐺𝐽)) ∩ 𝑧 ∈ ℕ ((,)‘(𝐹𝑧))) = (((,)‘(𝐺𝐽)) ∩ 𝐴))
13099, 114, 1293eqtr2d 2691 . . . . . . 7 ((𝜑𝐽 ∈ ℕ) → ran ((,) ∘ (𝐾𝐻)) = (((,)‘(𝐺𝐽)) ∩ 𝐴))
131130fveq2d 6233 . . . . . 6 ((𝜑𝐽 ∈ ℕ) → (vol*‘ ran ((,) ∘ (𝐾𝐻))) = (vol*‘(((,)‘(𝐺𝐽)) ∩ 𝐴)))
13287, 131eqtr3d 2687 . . . . 5 ((𝜑𝐽 ∈ ℕ) → sup(ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))), ℝ*, < ) = (vol*‘(((,)‘(𝐺𝐽)) ∩ 𝐴)))
133 inss1 3866 . . . . . . 7 (((,)‘(𝐺𝐽)) ∩ 𝐴) ⊆ ((,)‘(𝐺𝐽))
134133a1i 11 . . . . . 6 ((𝜑𝐽 ∈ ℕ) → (((,)‘(𝐺𝐽)) ∩ 𝐴) ⊆ ((,)‘(𝐺𝐽)))
135 ovolsscl 23300 . . . . . 6 (((((,)‘(𝐺𝐽)) ∩ 𝐴) ⊆ ((,)‘(𝐺𝐽)) ∧ ((,)‘(𝐺𝐽)) ⊆ ℝ ∧ (vol*‘((,)‘(𝐺𝐽))) ∈ ℝ) → (vol*‘(((,)‘(𝐺𝐽)) ∩ 𝐴)) ∈ ℝ)
136134, 27, 37, 135syl3anc 1366 . . . . 5 ((𝜑𝐽 ∈ ℕ) → (vol*‘(((,)‘(𝐺𝐽)) ∩ 𝐴)) ∈ ℝ)
137132, 136eqeltrd 2730 . . . 4 ((𝜑𝐽 ∈ ℕ) → sup(ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))), ℝ*, < ) ∈ ℝ)
13855, 2ovolsf 23287 . . . . . . . . 9 ((𝐾𝐻):ℕ⟶( ≤ ∩ (ℝ × ℝ)) → seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))):ℕ⟶(0[,)+∞))
13954, 138syl 17 . . . . . . . 8 ((𝜑𝐽 ∈ ℕ) → seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))):ℕ⟶(0[,)+∞))
140 ffn 6083 . . . . . . . 8 (seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))):ℕ⟶(0[,)+∞) → seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))) Fn ℕ)
141139, 140syl 17 . . . . . . 7 ((𝜑𝐽 ∈ ℕ) → seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))) Fn ℕ)
142 fnfvelrn 6396 . . . . . . 7 ((seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))) Fn ℕ ∧ 𝑦 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻)))‘𝑦) ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))))
143141, 142sylan 487 . . . . . 6 (((𝜑𝐽 ∈ ℕ) ∧ 𝑦 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻)))‘𝑦) ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))))
144 frn 6091 . . . . . . . . 9 (seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))):ℕ⟶(0[,)+∞) → ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))) ⊆ (0[,)+∞))
145139, 144syl 17 . . . . . . . 8 ((𝜑𝐽 ∈ ℕ) → ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))) ⊆ (0[,)+∞))
146 icossxr 12296 . . . . . . . 8 (0[,)+∞) ⊆ ℝ*
147145, 146syl6ss 3648 . . . . . . 7 ((𝜑𝐽 ∈ ℕ) → ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))) ⊆ ℝ*)
148 supxrub 12192 . . . . . . 7 ((ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))) ⊆ ℝ* ∧ (seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻)))‘𝑦) ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻)))) → (seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻)))‘𝑦) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))), ℝ*, < ))
149147, 148sylan 487 . . . . . 6 (((𝜑𝐽 ∈ ℕ) ∧ (seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻)))‘𝑦) ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻)))) → (seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻)))‘𝑦) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))), ℝ*, < ))
150143, 149syldan 486 . . . . 5 (((𝜑𝐽 ∈ ℕ) ∧ 𝑦 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻)))‘𝑦) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))), ℝ*, < ))
151150ralrimiva 2995 . . . 4 ((𝜑𝐽 ∈ ℕ) → ∀𝑦 ∈ ℕ (seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻)))‘𝑦) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))), ℝ*, < ))
152 breq2 4689 . . . . . 6 (𝑥 = sup(ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))), ℝ*, < ) → ((seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻)))‘𝑦) ≤ 𝑥 ↔ (seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻)))‘𝑦) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))), ℝ*, < )))
153152ralbidv 3015 . . . . 5 (𝑥 = sup(ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))), ℝ*, < ) → (∀𝑦 ∈ ℕ (seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻)))‘𝑦) ≤ 𝑥 ↔ ∀𝑦 ∈ ℕ (seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻)))‘𝑦) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))), ℝ*, < )))
154153rspcev 3340 . . . 4 ((sup(ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))), ℝ*, < ) ∈ ℝ ∧ ∀𝑦 ∈ ℕ (seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻)))‘𝑦) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))), ℝ*, < )) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℕ (seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻)))‘𝑦) ≤ 𝑥)
155137, 151, 154syl2anc 694 . . 3 ((𝜑𝐽 ∈ ℕ) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℕ (seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻)))‘𝑦) ≤ 𝑥)
1561, 2, 3, 4, 61, 62, 155isumsup2 14622 . 2 ((𝜑𝐽 ∈ ℕ) → seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))) ⇝ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))), ℝ, < ))
15755ovolfs2 23385 . . . . 5 ((𝐾𝐻):ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ (𝐾𝐻)) = ((vol* ∘ (,)) ∘ (𝐾𝐻)))
15854, 157syl 17 . . . 4 ((𝜑𝐽 ∈ ℕ) → ((abs ∘ − ) ∘ (𝐾𝐻)) = ((vol* ∘ (,)) ∘ (𝐾𝐻)))
159 coass 5692 . . . . 5 ((vol* ∘ (,)) ∘ (𝐾𝐻)) = (vol* ∘ ((,) ∘ (𝐾𝐻)))
16097coeq2d 5317 . . . . 5 ((𝜑𝐽 ∈ ℕ) → (vol* ∘ ((,) ∘ (𝐾𝐻))) = (vol* ∘ 𝐻))
161159, 160syl5eq 2697 . . . 4 ((𝜑𝐽 ∈ ℕ) → ((vol* ∘ (,)) ∘ (𝐾𝐻)) = (vol* ∘ 𝐻))
162158, 161eqtrd 2685 . . 3 ((𝜑𝐽 ∈ ℕ) → ((abs ∘ − ) ∘ (𝐾𝐻)) = (vol* ∘ 𝐻))
163162seqeq3d 12849 . 2 ((𝜑𝐽 ∈ ℕ) → seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))) = seq1( + , (vol* ∘ 𝐻)))
164 rge0ssre 12318 . . . . 5 (0[,)+∞) ⊆ ℝ
165145, 164syl6ss 3648 . . . 4 ((𝜑𝐽 ∈ ℕ) → ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))) ⊆ ℝ)
166 1nn 11069 . . . . . . 7 1 ∈ ℕ
167 fdm 6089 . . . . . . . 8 (seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))):ℕ⟶(0[,)+∞) → dom seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))) = ℕ)
168139, 167syl 17 . . . . . . 7 ((𝜑𝐽 ∈ ℕ) → dom seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))) = ℕ)
169166, 168syl5eleqr 2737 . . . . . 6 ((𝜑𝐽 ∈ ℕ) → 1 ∈ dom seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))))
170 ne0i 3954 . . . . . 6 (1 ∈ dom seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))) → dom seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))) ≠ ∅)
171169, 170syl 17 . . . . 5 ((𝜑𝐽 ∈ ℕ) → dom seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))) ≠ ∅)
172 dm0rn0 5374 . . . . . 6 (dom seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))) = ∅ ↔ ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))) = ∅)
173172necon3bii 2875 . . . . 5 (dom seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))) ≠ ∅ ↔ ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))) ≠ ∅)
174171, 173sylib 208 . . . 4 ((𝜑𝐽 ∈ ℕ) → ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))) ≠ ∅)
175 breq1 4688 . . . . . . . 8 (𝑧 = (seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻)))‘𝑦) → (𝑧𝑥 ↔ (seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻)))‘𝑦) ≤ 𝑥))
176175ralrn 6402 . . . . . . 7 (seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))) Fn ℕ → (∀𝑧 ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻)))𝑧𝑥 ↔ ∀𝑦 ∈ ℕ (seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻)))‘𝑦) ≤ 𝑥))
177141, 176syl 17 . . . . . 6 ((𝜑𝐽 ∈ ℕ) → (∀𝑧 ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻)))𝑧𝑥 ↔ ∀𝑦 ∈ ℕ (seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻)))‘𝑦) ≤ 𝑥))
178177rexbidv 3081 . . . . 5 ((𝜑𝐽 ∈ ℕ) → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻)))𝑧𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℕ (seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻)))‘𝑦) ≤ 𝑥))
179155, 178mpbird 247 . . . 4 ((𝜑𝐽 ∈ ℕ) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻)))𝑧𝑥)
180 supxrre 12195 . . . 4 ((ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))) ⊆ ℝ ∧ ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻)))𝑧𝑥) → sup(ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))), ℝ*, < ) = sup(ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))), ℝ, < ))
181165, 174, 179, 180syl3anc 1366 . . 3 ((𝜑𝐽 ∈ ℕ) → sup(ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))), ℝ*, < ) = sup(ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))), ℝ, < ))
182181, 132eqtr3d 2687 . 2 ((𝜑𝐽 ∈ ℕ) → sup(ran seq1( + , ((abs ∘ − ) ∘ (𝐾𝐻))), ℝ, < ) = (vol*‘(((,)‘(𝐺𝐽)) ∩ 𝐴)))
183156, 163, 1823brtr3d 4716 1 ((𝜑𝐽 ∈ ℕ) → seq1( + , (vol* ∘ 𝐻)) ⇝ (vol*‘(((,)‘(𝐺𝐽)) ∩ 𝐴)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030   ≠ wne 2823  ∀wral 2941  ∃wrex 2942  Vcvv 3231   ∩ cin 3606   ⊆ wss 3607  ∅c0 3948  ifcif 4119  𝒫 cpw 4191  ⟨cop 4216  ∪ cuni 4468  ∪ ciun 4552  Disj wdisj 4652   class class class wbr 4685   ↦ cmpt 4762   × cxp 5141  dom cdm 5143  ran crn 5144   ∘ ccom 5147   Fn wfn 5921  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690  1st c1st 7208  2nd c2nd 7209  supcsup 8387  infcinf 8388  ℝcr 9973  0cc0 9974  1c1 9975   + caddc 9977  +∞cpnf 10109  ℝ*cxr 10111   < clt 10112   ≤ cle 10113   − cmin 10304  ℕcn 11058  ℝ+crp 11870  (,)cioo 12213  [,)cico 12215  seqcseq 12841  abscabs 14018   ⇝ cli 14259  vol*covol 23277 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-disj 4653  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fi 8358  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ioo 12217  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-rlim 14264  df-sum 14461  df-rest 16130  df-topgen 16151  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-top 20747  df-topon 20764  df-bases 20798  df-cmp 21238  df-ovol 23279  df-vol 23280 This theorem is referenced by:  uniioombllem6  23402
 Copyright terms: Public domain W3C validator