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

Theorem itg1climres 23287
Description: Restricting the simple function 𝐹 to the increasing sequence 𝐴(𝑛) of measurable sets whose union is yields a sequence of simple functions whose integrals approach the integral of 𝐹. (Contributed by Mario Carneiro, 15-Aug-2014.)
Hypotheses
Ref Expression
itg1climres.1 (𝜑𝐴:ℕ⟶dom vol)
itg1climres.2 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ⊆ (𝐴‘(𝑛 + 1)))
itg1climres.3 (𝜑 ran 𝐴 = ℝ)
itg1climres.4 (𝜑𝐹 ∈ dom ∫1)
itg1climres.5 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0))
Assertion
Ref Expression
itg1climres (𝜑 → (𝑛 ∈ ℕ ↦ (∫1𝐺)) ⇝ (∫1𝐹))
Distinct variable groups:   𝑥,𝑛,𝐴   𝑛,𝐹,𝑥   𝜑,𝑛,𝑥
Allowed substitution hints:   𝐺(𝑥,𝑛)

Proof of Theorem itg1climres
Dummy variables 𝑗 𝑦 𝑧 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 11599 . . 3 ℕ = (ℤ‘1)
2 1zzd 11285 . . 3 (𝜑 → 1 ∈ ℤ)
3 itg1climres.4 . . . . 5 (𝜑𝐹 ∈ dom ∫1)
4 i1frn 23250 . . . . 5 (𝐹 ∈ dom ∫1 → ran 𝐹 ∈ Fin)
53, 4syl 17 . . . 4 (𝜑 → ran 𝐹 ∈ Fin)
6 difss 3699 . . . 4 (ran 𝐹 ∖ {0}) ⊆ ran 𝐹
7 ssfi 8065 . . . 4 ((ran 𝐹 ∈ Fin ∧ (ran 𝐹 ∖ {0}) ⊆ ran 𝐹) → (ran 𝐹 ∖ {0}) ∈ Fin)
85, 6, 7sylancl 693 . . 3 (𝜑 → (ran 𝐹 ∖ {0}) ∈ Fin)
9 1zzd 11285 . . . 4 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → 1 ∈ ℤ)
10 i1fima 23251 . . . . . . . . . . . 12 (𝐹 ∈ dom ∫1 → (𝐹 “ {𝑘}) ∈ dom vol)
113, 10syl 17 . . . . . . . . . . 11 (𝜑 → (𝐹 “ {𝑘}) ∈ dom vol)
1211ad2antrr 758 . . . . . . . . . 10 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (𝐹 “ {𝑘}) ∈ dom vol)
13 itg1climres.1 . . . . . . . . . . . 12 (𝜑𝐴:ℕ⟶dom vol)
1413ffvelrnda 6267 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ∈ dom vol)
1514adantlr 747 . . . . . . . . . 10 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (𝐴𝑛) ∈ dom vol)
16 inmbl 23117 . . . . . . . . . 10 (((𝐹 “ {𝑘}) ∈ dom vol ∧ (𝐴𝑛) ∈ dom vol) → ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ∈ dom vol)
1712, 15, 16syl2anc 691 . . . . . . . . 9 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ∈ dom vol)
18 mblvol 23105 . . . . . . . . 9 (((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ∈ dom vol → (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) = (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
1917, 18syl 17 . . . . . . . 8 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) = (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
20 inss1 3795 . . . . . . . . . 10 ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ (𝐹 “ {𝑘})
2120a1i 11 . . . . . . . . 9 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ (𝐹 “ {𝑘}))
22 mblss 23106 . . . . . . . . . 10 ((𝐹 “ {𝑘}) ∈ dom vol → (𝐹 “ {𝑘}) ⊆ ℝ)
2312, 22syl 17 . . . . . . . . 9 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (𝐹 “ {𝑘}) ⊆ ℝ)
24 mblvol 23105 . . . . . . . . . . 11 ((𝐹 “ {𝑘}) ∈ dom vol → (vol‘(𝐹 “ {𝑘})) = (vol*‘(𝐹 “ {𝑘})))
2512, 24syl 17 . . . . . . . . . 10 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘(𝐹 “ {𝑘})) = (vol*‘(𝐹 “ {𝑘})))
26 i1fima2sn 23253 . . . . . . . . . . . 12 ((𝐹 ∈ dom ∫1𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(𝐹 “ {𝑘})) ∈ ℝ)
273, 26sylan 487 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(𝐹 “ {𝑘})) ∈ ℝ)
2827adantr 480 . . . . . . . . . 10 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘(𝐹 “ {𝑘})) ∈ ℝ)
2925, 28eqeltrrd 2689 . . . . . . . . 9 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol*‘(𝐹 “ {𝑘})) ∈ ℝ)
30 ovolsscl 23061 . . . . . . . . 9 ((((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ (𝐹 “ {𝑘}) ∧ (𝐹 “ {𝑘}) ⊆ ℝ ∧ (vol*‘(𝐹 “ {𝑘})) ∈ ℝ) → (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ∈ ℝ)
3121, 23, 29, 30syl3anc 1318 . . . . . . . 8 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ∈ ℝ)
3219, 31eqeltrd 2688 . . . . . . 7 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ∈ ℝ)
33 eqid 2610 . . . . . . 7 (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
3432, 33fmptd 6292 . . . . . 6 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))):ℕ⟶ℝ)
35 itg1climres.2 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ⊆ (𝐴‘(𝑛 + 1)))
3635adantlr 747 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (𝐴𝑛) ⊆ (𝐴‘(𝑛 + 1)))
37 sslin 3801 . . . . . . . . . . . 12 ((𝐴𝑛) ⊆ (𝐴‘(𝑛 + 1)) → ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))))
3836, 37syl 17 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))))
3913adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝐴:ℕ⟶dom vol)
40 peano2nn 10909 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ)
41 ffvelrn 6265 . . . . . . . . . . . . . 14 ((𝐴:ℕ⟶dom vol ∧ (𝑛 + 1) ∈ ℕ) → (𝐴‘(𝑛 + 1)) ∈ dom vol)
4239, 40, 41syl2an 493 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (𝐴‘(𝑛 + 1)) ∈ dom vol)
43 inmbl 23117 . . . . . . . . . . . . 13 (((𝐹 “ {𝑘}) ∈ dom vol ∧ (𝐴‘(𝑛 + 1)) ∈ dom vol) → ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ∈ dom vol)
4412, 42, 43syl2anc 691 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ∈ dom vol)
45 mblss 23106 . . . . . . . . . . . 12 (((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ∈ dom vol → ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ⊆ ℝ)
4644, 45syl 17 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ⊆ ℝ)
47 ovolss 23060 . . . . . . . . . . 11 ((((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ∧ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ⊆ ℝ) → (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))))
4838, 46, 47syl2anc 691 . . . . . . . . . 10 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))))
49 mblvol 23105 . . . . . . . . . . 11 (((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ∈ dom vol → (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) = (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))))
5044, 49syl 17 . . . . . . . . . 10 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) = (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))))
5148, 19, 503brtr4d 4615 . . . . . . . . 9 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))))
5251ralrimiva 2949 . . . . . . . 8 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑛 ∈ ℕ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))))
53 fveq2 6103 . . . . . . . . . . . . . 14 (𝑛 = 𝑗 → (𝐴𝑛) = (𝐴𝑗))
5453ineq2d 3776 . . . . . . . . . . . . 13 (𝑛 = 𝑗 → ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) = ((𝐹 “ {𝑘}) ∩ (𝐴𝑗)))
5554fveq2d 6107 . . . . . . . . . . . 12 (𝑛 = 𝑗 → (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) = (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))))
56 fvex 6113 . . . . . . . . . . . 12 (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))) ∈ V
5755, 33, 56fvmpt 6191 . . . . . . . . . . 11 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) = (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))))
58 peano2nn 10909 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℕ)
59 fveq2 6103 . . . . . . . . . . . . . . 15 (𝑛 = (𝑗 + 1) → (𝐴𝑛) = (𝐴‘(𝑗 + 1)))
6059ineq2d 3776 . . . . . . . . . . . . . 14 (𝑛 = (𝑗 + 1) → ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) = ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))
6160fveq2d 6107 . . . . . . . . . . . . 13 (𝑛 = (𝑗 + 1) → (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) = (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))))
62 fvex 6113 . . . . . . . . . . . . 13 (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))) ∈ V
6361, 33, 62fvmpt 6191 . . . . . . . . . . . 12 ((𝑗 + 1) ∈ ℕ → ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘(𝑗 + 1)) = (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))))
6458, 63syl 17 . . . . . . . . . . 11 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘(𝑗 + 1)) = (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))))
6557, 64breq12d 4596 . . . . . . . . . 10 (𝑗 ∈ ℕ → (((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘(𝑗 + 1)) ↔ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))) ≤ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))))
6665ralbiia 2962 . . . . . . . . 9 (∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘(𝑗 + 1)) ↔ ∀𝑗 ∈ ℕ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))) ≤ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))))
67 oveq1 6556 . . . . . . . . . . . . . 14 (𝑛 = 𝑗 → (𝑛 + 1) = (𝑗 + 1))
6867fveq2d 6107 . . . . . . . . . . . . 13 (𝑛 = 𝑗 → (𝐴‘(𝑛 + 1)) = (𝐴‘(𝑗 + 1)))
6968ineq2d 3776 . . . . . . . . . . . 12 (𝑛 = 𝑗 → ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) = ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))
7069fveq2d 6107 . . . . . . . . . . 11 (𝑛 = 𝑗 → (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) = (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))))
7155, 70breq12d 4596 . . . . . . . . . 10 (𝑛 = 𝑗 → ((vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) ↔ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))) ≤ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))))
7271cbvralv 3147 . . . . . . . . 9 (∀𝑛 ∈ ℕ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) ↔ ∀𝑗 ∈ ℕ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))) ≤ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))))
7366, 72bitr4i 266 . . . . . . . 8 (∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘(𝑗 + 1)) ↔ ∀𝑛 ∈ ℕ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))))
7452, 73sylibr 223 . . . . . . 7 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘(𝑗 + 1)))
7574r19.21bi 2916 . . . . . 6 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘(𝑗 + 1)))
76 ovolss 23060 . . . . . . . . . . 11 ((((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ (𝐹 “ {𝑘}) ∧ (𝐹 “ {𝑘}) ⊆ ℝ) → (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol*‘(𝐹 “ {𝑘})))
7720, 23, 76sylancr 694 . . . . . . . . . 10 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol*‘(𝐹 “ {𝑘})))
7877, 19, 253brtr4d 4615 . . . . . . . . 9 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol‘(𝐹 “ {𝑘})))
7978ralrimiva 2949 . . . . . . . 8 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑛 ∈ ℕ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol‘(𝐹 “ {𝑘})))
8057breq1d 4593 . . . . . . . . . 10 (𝑗 ∈ ℕ → (((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ (vol‘(𝐹 “ {𝑘})) ↔ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))) ≤ (vol‘(𝐹 “ {𝑘}))))
8180ralbiia 2962 . . . . . . . . 9 (∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ (vol‘(𝐹 “ {𝑘})) ↔ ∀𝑗 ∈ ℕ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))) ≤ (vol‘(𝐹 “ {𝑘})))
8255breq1d 4593 . . . . . . . . . 10 (𝑛 = 𝑗 → ((vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol‘(𝐹 “ {𝑘})) ↔ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))) ≤ (vol‘(𝐹 “ {𝑘}))))
8382cbvralv 3147 . . . . . . . . 9 (∀𝑛 ∈ ℕ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol‘(𝐹 “ {𝑘})) ↔ ∀𝑗 ∈ ℕ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))) ≤ (vol‘(𝐹 “ {𝑘})))
8481, 83bitr4i 266 . . . . . . . 8 (∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ (vol‘(𝐹 “ {𝑘})) ↔ ∀𝑛 ∈ ℕ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol‘(𝐹 “ {𝑘})))
8579, 84sylibr 223 . . . . . . 7 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ (vol‘(𝐹 “ {𝑘})))
86 breq2 4587 . . . . . . . . 9 (𝑥 = (vol‘(𝐹 “ {𝑘})) → (((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ 𝑥 ↔ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ (vol‘(𝐹 “ {𝑘}))))
8786ralbidv 2969 . . . . . . . 8 (𝑥 = (vol‘(𝐹 “ {𝑘})) → (∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ (vol‘(𝐹 “ {𝑘}))))
8887rspcev 3282 . . . . . . 7 (((vol‘(𝐹 “ {𝑘})) ∈ ℝ ∧ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ (vol‘(𝐹 “ {𝑘}))) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ 𝑥)
8927, 85, 88syl2anc 691 . . . . . 6 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ 𝑥)
901, 9, 34, 75, 89climsup 14248 . . . . 5 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) ⇝ sup(ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ, < ))
91 eqid 2610 . . . . . . . 8 (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) = (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))
9217, 91fmptd 6292 . . . . . . 7 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))):ℕ⟶dom vol)
9338ralrimiva 2949 . . . . . . . 8 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑛 ∈ ℕ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))))
94 fvex 6113 . . . . . . . . . . . . 13 (𝐴𝑗) ∈ V
9594inex2 4728 . . . . . . . . . . . 12 ((𝐹 “ {𝑘}) ∩ (𝐴𝑗)) ∈ V
9654, 91, 95fvmpt 6191 . . . . . . . . . . 11 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) = ((𝐹 “ {𝑘}) ∩ (𝐴𝑗)))
97 fvex 6113 . . . . . . . . . . . . . 14 (𝐴‘(𝑗 + 1)) ∈ V
9897inex2 4728 . . . . . . . . . . . . 13 ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))) ∈ V
9960, 91, 98fvmpt 6191 . . . . . . . . . . . 12 ((𝑗 + 1) ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘(𝑗 + 1)) = ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))
10058, 99syl 17 . . . . . . . . . . 11 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘(𝑗 + 1)) = ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))
10196, 100sseq12d 3597 . . . . . . . . . 10 (𝑗 ∈ ℕ → (((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) ⊆ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘(𝑗 + 1)) ↔ ((𝐹 “ {𝑘}) ∩ (𝐴𝑗)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))))
102101ralbiia 2962 . . . . . . . . 9 (∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) ⊆ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘(𝑗 + 1)) ↔ ∀𝑗 ∈ ℕ ((𝐹 “ {𝑘}) ∩ (𝐴𝑗)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))
10354, 69sseq12d 3597 . . . . . . . . . 10 (𝑛 = 𝑗 → (((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ↔ ((𝐹 “ {𝑘}) ∩ (𝐴𝑗)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))))
104103cbvralv 3147 . . . . . . . . 9 (∀𝑛 ∈ ℕ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ↔ ∀𝑗 ∈ ℕ ((𝐹 “ {𝑘}) ∩ (𝐴𝑗)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))
105102, 104bitr4i 266 . . . . . . . 8 (∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) ⊆ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘(𝑗 + 1)) ↔ ∀𝑛 ∈ ℕ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))))
10693, 105sylibr 223 . . . . . . 7 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) ⊆ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘(𝑗 + 1)))
107 volsup 23131 . . . . . . 7 (((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))):ℕ⟶dom vol ∧ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) ⊆ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘(𝑗 + 1))) → (vol‘ ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = sup((vol “ ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ*, < ))
10892, 106, 107syl2anc 691 . . . . . 6 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘ ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = sup((vol “ ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ*, < ))
10996iuneq2i 4475 . . . . . . . . . 10 𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) = 𝑗 ∈ ℕ ((𝐹 “ {𝑘}) ∩ (𝐴𝑗))
11054cbviunv 4495 . . . . . . . . . 10 𝑛 ∈ ℕ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) = 𝑗 ∈ ℕ ((𝐹 “ {𝑘}) ∩ (𝐴𝑗))
111 iunin2 4520 . . . . . . . . . 10 𝑛 ∈ ℕ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) = ((𝐹 “ {𝑘}) ∩ 𝑛 ∈ ℕ (𝐴𝑛))
112109, 110, 1113eqtr2i 2638 . . . . . . . . 9 𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) = ((𝐹 “ {𝑘}) ∩ 𝑛 ∈ ℕ (𝐴𝑛))
113 ffn 5958 . . . . . . . . . . . . . 14 (𝐴:ℕ⟶dom vol → 𝐴 Fn ℕ)
114 fniunfv 6409 . . . . . . . . . . . . . 14 (𝐴 Fn ℕ → 𝑛 ∈ ℕ (𝐴𝑛) = ran 𝐴)
11513, 113, 1143syl 18 . . . . . . . . . . . . 13 (𝜑 𝑛 ∈ ℕ (𝐴𝑛) = ran 𝐴)
116 itg1climres.3 . . . . . . . . . . . . 13 (𝜑 ran 𝐴 = ℝ)
117115, 116eqtrd 2644 . . . . . . . . . . . 12 (𝜑 𝑛 ∈ ℕ (𝐴𝑛) = ℝ)
118117adantr 480 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑛 ∈ ℕ (𝐴𝑛) = ℝ)
119118ineq2d 3776 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ((𝐹 “ {𝑘}) ∩ 𝑛 ∈ ℕ (𝐴𝑛)) = ((𝐹 “ {𝑘}) ∩ ℝ))
12011adantr 480 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝐹 “ {𝑘}) ∈ dom vol)
121120, 22syl 17 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝐹 “ {𝑘}) ⊆ ℝ)
122 df-ss 3554 . . . . . . . . . . 11 ((𝐹 “ {𝑘}) ⊆ ℝ ↔ ((𝐹 “ {𝑘}) ∩ ℝ) = (𝐹 “ {𝑘}))
123121, 122sylib 207 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ((𝐹 “ {𝑘}) ∩ ℝ) = (𝐹 “ {𝑘}))
124119, 123eqtrd 2644 . . . . . . . . 9 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ((𝐹 “ {𝑘}) ∩ 𝑛 ∈ ℕ (𝐴𝑛)) = (𝐹 “ {𝑘}))
125112, 124syl5eq 2656 . . . . . . . 8 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) = (𝐹 “ {𝑘}))
126 ffn 5958 . . . . . . . . 9 ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))):ℕ⟶dom vol → (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) Fn ℕ)
127 fniunfv 6409 . . . . . . . . 9 ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) Fn ℕ → 𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) = ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
12892, 126, 1273syl 18 . . . . . . . 8 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) = ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
129125, 128eqtr3d 2646 . . . . . . 7 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝐹 “ {𝑘}) = ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
130129fveq2d 6107 . . . . . 6 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(𝐹 “ {𝑘})) = (vol‘ ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))
131 frn 5966 . . . . . . . . 9 ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))):ℕ⟶ℝ → ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) ⊆ ℝ)
13234, 131syl 17 . . . . . . . 8 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) ⊆ ℝ)
133 fdm 5964 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))):ℕ⟶ℝ → dom (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = ℕ)
13434, 133syl 17 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → dom (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = ℕ)
135 1nn 10908 . . . . . . . . . . 11 1 ∈ ℕ
136 ne0i 3880 . . . . . . . . . . 11 (1 ∈ ℕ → ℕ ≠ ∅)
137135, 136mp1i 13 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ℕ ≠ ∅)
138134, 137eqnetrd 2849 . . . . . . . . 9 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → dom (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) ≠ ∅)
139 dm0rn0 5263 . . . . . . . . . 10 (dom (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = ∅ ↔ ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = ∅)
140139necon3bii 2834 . . . . . . . . 9 (dom (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) ≠ ∅ ↔ ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) ≠ ∅)
141138, 140sylib 207 . . . . . . . 8 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) ≠ ∅)
142 ffn 5958 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))):ℕ⟶ℝ → (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) Fn ℕ)
143 breq1 4586 . . . . . . . . . . . 12 (𝑧 = ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) → (𝑧𝑥 ↔ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ 𝑥))
144143ralrn 6270 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) Fn ℕ → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))𝑧𝑥 ↔ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ 𝑥))
14534, 142, 1443syl 18 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))𝑧𝑥 ↔ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ 𝑥))
146145rexbidv 3034 . . . . . . . . 9 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))𝑧𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ 𝑥))
14789, 146mpbird 246 . . . . . . . 8 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))𝑧𝑥)
148 supxrre 12029 . . . . . . . 8 ((ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))𝑧𝑥) → sup(ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ*, < ) = sup(ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ, < ))
149132, 141, 147, 148syl3anc 1318 . . . . . . 7 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → sup(ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ*, < ) = sup(ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ, < ))
150 rnco2 5559 . . . . . . . . 9 ran (vol ∘ (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = (vol “ ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
151 eqidd 2611 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) = (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
152 volf 23104 . . . . . . . . . . . . 13 vol:dom vol⟶(0[,]+∞)
153152a1i 11 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → vol:dom vol⟶(0[,]+∞))
154153feqmptd 6159 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → vol = (𝑦 ∈ dom vol ↦ (vol‘𝑦)))
155 fveq2 6103 . . . . . . . . . . 11 (𝑦 = ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) → (vol‘𝑦) = (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
15617, 151, 154, 155fmptco 6303 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol ∘ (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))
157156rneqd 5274 . . . . . . . . 9 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ran (vol ∘ (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))
158150, 157syl5reqr 2659 . . . . . . . 8 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = (vol “ ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))
159158supeq1d 8235 . . . . . . 7 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → sup(ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ*, < ) = sup((vol “ ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ*, < ))
160149, 159eqtr3d 2646 . . . . . 6 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → sup(ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ, < ) = sup((vol “ ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ*, < ))
161108, 130, 1603eqtr4d 2654 . . . . 5 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(𝐹 “ {𝑘})) = sup(ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ, < ))
16290, 161breqtrrd 4611 . . . 4 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) ⇝ (vol‘(𝐹 “ {𝑘})))
163 i1ff 23249 . . . . . . . 8 (𝐹 ∈ dom ∫1𝐹:ℝ⟶ℝ)
164 frn 5966 . . . . . . . 8 (𝐹:ℝ⟶ℝ → ran 𝐹 ⊆ ℝ)
1653, 163, 1643syl 18 . . . . . . 7 (𝜑 → ran 𝐹 ⊆ ℝ)
166165ssdifssd 3710 . . . . . 6 (𝜑 → (ran 𝐹 ∖ {0}) ⊆ ℝ)
167166sselda 3568 . . . . 5 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑘 ∈ ℝ)
168167recnd 9947 . . . 4 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑘 ∈ ℂ)
169 nnex 10903 . . . . . 6 ℕ ∈ V
170169mptex 6390 . . . . 5 (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))) ∈ V
171170a1i 11 . . . 4 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))) ∈ V)
17234ffvelrnda 6267 . . . . 5 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ∈ ℝ)
173172recnd 9947 . . . 4 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ∈ ℂ)
17455oveq2d 6565 . . . . . . 7 (𝑛 = 𝑗 → (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗)))))
175 eqid 2610 . . . . . . 7 (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))) = (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))
176 ovex 6577 . . . . . . 7 (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗)))) ∈ V
177174, 175, 176fvmpt 6191 . . . . . 6 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗) = (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗)))))
17857oveq2d 6565 . . . . . 6 (𝑗 ∈ ℕ → (𝑘 · ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗)) = (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗)))))
179177, 178eqtr4d 2647 . . . . 5 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗) = (𝑘 · ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗)))
180179adantl 481 . . . 4 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗) = (𝑘 · ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗)))
1811, 9, 162, 168, 171, 173, 180climmulc2 14215 . . 3 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))) ⇝ (𝑘 · (vol‘(𝐹 “ {𝑘}))))
182169mptex 6390 . . . 4 (𝑛 ∈ ℕ ↦ (∫1𝐺)) ∈ V
183182a1i 11 . . 3 (𝜑 → (𝑛 ∈ ℕ ↦ (∫1𝐺)) ∈ V)
184167adantr 480 . . . . . . . 8 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → 𝑘 ∈ ℝ)
185184, 32remulcld 9949 . . . . . . 7 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) ∈ ℝ)
186185, 175fmptd 6292 . . . . . 6 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))):ℕ⟶ℝ)
187186ffvelrnda 6267 . . . . 5 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗) ∈ ℝ)
188187recnd 9947 . . . 4 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗) ∈ ℂ)
189188anasss 677 . . 3 ((𝜑 ∧ (𝑘 ∈ (ran 𝐹 ∖ {0}) ∧ 𝑗 ∈ ℕ)) → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗) ∈ ℂ)
1903adantr 480 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝐹 ∈ dom ∫1)
191 itg1climres.5 . . . . . . . . . 10 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0))
192191i1fres 23278 . . . . . . . . 9 ((𝐹 ∈ dom ∫1 ∧ (𝐴𝑛) ∈ dom vol) → 𝐺 ∈ dom ∫1)
193190, 14, 192syl2anc 691 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝐺 ∈ dom ∫1)
1948adantr 480 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (ran 𝐹 ∖ {0}) ∈ Fin)
195 ffn 5958 . . . . . . . . . . . . . 14 (𝐹:ℝ⟶ℝ → 𝐹 Fn ℝ)
1963, 163, 1953syl 18 . . . . . . . . . . . . 13 (𝜑𝐹 Fn ℝ)
197196adantr 480 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → 𝐹 Fn ℝ)
198 fnfvelrn 6264 . . . . . . . . . . . 12 ((𝐹 Fn ℝ ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ran 𝐹)
199197, 198sylan 487 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ran 𝐹)
200 i1f0rn 23255 . . . . . . . . . . . . 13 (𝐹 ∈ dom ∫1 → 0 ∈ ran 𝐹)
2013, 200syl 17 . . . . . . . . . . . 12 (𝜑 → 0 ∈ ran 𝐹)
202201ad2antrr 758 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ∈ ran 𝐹)
203199, 202ifcld 4081 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) ∈ ran 𝐹)
204203, 191fmptd 6292 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝐺:ℝ⟶ran 𝐹)
205 frn 5966 . . . . . . . . 9 (𝐺:ℝ⟶ran 𝐹 → ran 𝐺 ⊆ ran 𝐹)
206 ssdif 3707 . . . . . . . . 9 (ran 𝐺 ⊆ ran 𝐹 → (ran 𝐺 ∖ {0}) ⊆ (ran 𝐹 ∖ {0}))
207204, 205, 2063syl 18 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (ran 𝐺 ∖ {0}) ⊆ (ran 𝐹 ∖ {0}))
208165adantr 480 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ran 𝐹 ⊆ ℝ)
209208ssdifd 3708 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (ran 𝐹 ∖ {0}) ⊆ (ℝ ∖ {0}))
210 itg1val2 23257 . . . . . . . 8 ((𝐺 ∈ dom ∫1 ∧ ((ran 𝐹 ∖ {0}) ∈ Fin ∧ (ran 𝐺 ∖ {0}) ⊆ (ran 𝐹 ∖ {0}) ∧ (ran 𝐹 ∖ {0}) ⊆ (ℝ ∖ {0}))) → (∫1𝐺) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(𝐺 “ {𝑘}))))
211193, 194, 207, 209, 210syl13anc 1320 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (∫1𝐺) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(𝐺 “ {𝑘}))))
212 fvex 6113 . . . . . . . . . . . . . . . . . . . . 21 (𝐹𝑥) ∈ V
213 c0ex 9913 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ V
214212, 213ifex 4106 . . . . . . . . . . . . . . . . . . . 20 if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) ∈ V
215191fvmpt2 6200 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) ∈ V) → (𝐺𝑥) = if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0))
216214, 215mpan2 703 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ → (𝐺𝑥) = if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0))
217216adantl 481 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝐺𝑥) = if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0))
218217eqeq1d 2612 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑥) = 𝑘 ↔ if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 𝑘))
219 eldifsni 4261 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ (ran 𝐹 ∖ {0}) → 𝑘 ≠ 0)
220219ad2antlr 759 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ≠ 0)
221 neeq1 2844 . . . . . . . . . . . . . . . . . . . 20 (if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 𝑘 → (if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) ≠ 0 ↔ 𝑘 ≠ 0))
222220, 221syl5ibrcom 236 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 𝑘 → if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) ≠ 0))
223 iffalse 4045 . . . . . . . . . . . . . . . . . . . 20 𝑥 ∈ (𝐴𝑛) → if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 0)
224223necon1ai 2809 . . . . . . . . . . . . . . . . . . 19 (if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) ≠ 0 → 𝑥 ∈ (𝐴𝑛))
225222, 224syl6 34 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 𝑘𝑥 ∈ (𝐴𝑛)))
226225pm4.71rd 665 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 𝑘 ↔ (𝑥 ∈ (𝐴𝑛) ∧ if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 𝑘)))
227218, 226bitrd 267 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑥) = 𝑘 ↔ (𝑥 ∈ (𝐴𝑛) ∧ if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 𝑘)))
228 iftrue 4042 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝐴𝑛) → if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = (𝐹𝑥))
229228eqeq1d 2612 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴𝑛) → (if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 𝑘 ↔ (𝐹𝑥) = 𝑘))
230229pm5.32i 667 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (𝐴𝑛) ∧ if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 𝑘) ↔ (𝑥 ∈ (𝐴𝑛) ∧ (𝐹𝑥) = 𝑘))
231 ancom 465 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (𝐴𝑛) ∧ (𝐹𝑥) = 𝑘) ↔ ((𝐹𝑥) = 𝑘𝑥 ∈ (𝐴𝑛)))
232230, 231bitri 263 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (𝐴𝑛) ∧ if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 𝑘) ↔ ((𝐹𝑥) = 𝑘𝑥 ∈ (𝐴𝑛)))
233227, 232syl6bb 275 . . . . . . . . . . . . . . 15 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑥) = 𝑘 ↔ ((𝐹𝑥) = 𝑘𝑥 ∈ (𝐴𝑛))))
234233pm5.32da 671 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ((𝑥 ∈ ℝ ∧ (𝐺𝑥) = 𝑘) ↔ (𝑥 ∈ ℝ ∧ ((𝐹𝑥) = 𝑘𝑥 ∈ (𝐴𝑛)))))
235 anass 679 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℝ ∧ (𝐹𝑥) = 𝑘) ∧ 𝑥 ∈ (𝐴𝑛)) ↔ (𝑥 ∈ ℝ ∧ ((𝐹𝑥) = 𝑘𝑥 ∈ (𝐴𝑛))))
236234, 235syl6bbr 277 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ((𝑥 ∈ ℝ ∧ (𝐺𝑥) = 𝑘) ↔ ((𝑥 ∈ ℝ ∧ (𝐹𝑥) = 𝑘) ∧ 𝑥 ∈ (𝐴𝑛))))
237 i1ff 23249 . . . . . . . . . . . . . . . 16 (𝐺 ∈ dom ∫1𝐺:ℝ⟶ℝ)
238 ffn 5958 . . . . . . . . . . . . . . . 16 (𝐺:ℝ⟶ℝ → 𝐺 Fn ℝ)
239193, 237, 2383syl 18 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → 𝐺 Fn ℝ)
240239adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝐺 Fn ℝ)
241 fniniseg 6246 . . . . . . . . . . . . . 14 (𝐺 Fn ℝ → (𝑥 ∈ (𝐺 “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ (𝐺𝑥) = 𝑘)))
242240, 241syl 17 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑥 ∈ (𝐺 “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ (𝐺𝑥) = 𝑘)))
243 elin 3758 . . . . . . . . . . . . . 14 (𝑥 ∈ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ↔ (𝑥 ∈ (𝐹 “ {𝑘}) ∧ 𝑥 ∈ (𝐴𝑛)))
244197adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝐹 Fn ℝ)
245 fniniseg 6246 . . . . . . . . . . . . . . . 16 (𝐹 Fn ℝ → (𝑥 ∈ (𝐹 “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ (𝐹𝑥) = 𝑘)))
246244, 245syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑥 ∈ (𝐹 “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ (𝐹𝑥) = 𝑘)))
247246anbi1d 737 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ((𝑥 ∈ (𝐹 “ {𝑘}) ∧ 𝑥 ∈ (𝐴𝑛)) ↔ ((𝑥 ∈ ℝ ∧ (𝐹𝑥) = 𝑘) ∧ 𝑥 ∈ (𝐴𝑛))))
248243, 247syl5bb 271 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑥 ∈ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ↔ ((𝑥 ∈ ℝ ∧ (𝐹𝑥) = 𝑘) ∧ 𝑥 ∈ (𝐴𝑛))))
249236, 242, 2483bitr4d 299 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑥 ∈ (𝐺 “ {𝑘}) ↔ 𝑥 ∈ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
250249alrimiv 1842 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑥(𝑥 ∈ (𝐺 “ {𝑘}) ↔ 𝑥 ∈ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
251 nfmpt1 4675 . . . . . . . . . . . . . . 15 𝑥(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0))
252191, 251nfcxfr 2749 . . . . . . . . . . . . . 14 𝑥𝐺
253252nfcnv 5223 . . . . . . . . . . . . 13 𝑥𝐺
254 nfcv 2751 . . . . . . . . . . . . 13 𝑥{𝑘}
255253, 254nfima 5393 . . . . . . . . . . . 12 𝑥(𝐺 “ {𝑘})
256 nfcv 2751 . . . . . . . . . . . 12 𝑥((𝐹 “ {𝑘}) ∩ (𝐴𝑛))
257255, 256cleqf 2776 . . . . . . . . . . 11 ((𝐺 “ {𝑘}) = ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ↔ ∀𝑥(𝑥 ∈ (𝐺 “ {𝑘}) ↔ 𝑥 ∈ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
258250, 257sylibr 223 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝐺 “ {𝑘}) = ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))
259258fveq2d 6107 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(𝐺 “ {𝑘})) = (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
260259oveq2d 6565 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑘 · (vol‘(𝐺 “ {𝑘}))) = (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))
261260sumeq2dv 14281 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(𝐺 “ {𝑘}))) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))
262211, 261eqtrd 2644 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (∫1𝐺) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))
263262mpteq2dva 4672 . . . . 5 (𝜑 → (𝑛 ∈ ℕ ↦ (∫1𝐺)) = (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))))
264263fveq1d 6105 . . . 4 (𝜑 → ((𝑛 ∈ ℕ ↦ (∫1𝐺))‘𝑗) = ((𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗))
265174sumeq2sdv 14282 . . . . . 6 (𝑛 = 𝑗 → Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗)))))
266 eqid 2610 . . . . . 6 (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))) = (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))
267 sumex 14266 . . . . . 6 Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗)))) ∈ V
268265, 266, 267fvmpt 6191 . . . . 5 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗)))))
269177sumeq2sdv 14282 . . . . 5 (𝑗 ∈ ℕ → Σ𝑘 ∈ (ran 𝐹 ∖ {0})((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗)))))
270268, 269eqtr4d 2647 . . . 4 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗))
271264, 270sylan9eq 2664 . . 3 ((𝜑𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (∫1𝐺))‘𝑗) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗))
2721, 2, 8, 181, 183, 189, 271climfsum 14393 . 2 (𝜑 → (𝑛 ∈ ℕ ↦ (∫1𝐺)) ⇝ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(𝐹 “ {𝑘}))))
273 itg1val 23256 . . 3 (𝐹 ∈ dom ∫1 → (∫1𝐹) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(𝐹 “ {𝑘}))))
2743, 273syl 17 . 2 (𝜑 → (∫1𝐹) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(𝐹 “ {𝑘}))))
275272, 274breqtrrd 4611 1 (𝜑 → (𝑛 ∈ ℕ ↦ (∫1𝐺)) ⇝ (∫1𝐹))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383  wal 1473   = wceq 1475  wcel 1977  wne 2780  wral 2896  wrex 2897  Vcvv 3173  cdif 3537  cin 3539  wss 3540  c0 3874  ifcif 4036  {csn 4125   cuni 4372   ciun 4455   class class class wbr 4583  cmpt 4643  ccnv 5037  dom cdm 5038  ran crn 5039  cima 5041  ccom 5042   Fn wfn 5799  wf 5800  cfv 5804  (class class class)co 6549  Fincfn 7841  supcsup 8229  cc 9813  cr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820  +∞cpnf 9950  *cxr 9952   < clt 9953  cle 9954  cn 10897  [,]cicc 12049  cli 14063  Σcsu 14264  vol*covol 23038  volcvol 23039  1citg1 23190
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cc 9140  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893  ax-addf 9894
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-disj 4554  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fi 8200  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ioo 12050  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-fl 12455  df-seq 12664  df-exp 12723  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-rlim 14068  df-sum 14265  df-rest 15906  df-topgen 15927  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-top 20521  df-bases 20522  df-topon 20523  df-cmp 21000  df-ovol 23040  df-vol 23041  df-mbf 23194  df-itg1 23195
This theorem is referenced by:  itg2monolem1  23323
  Copyright terms: Public domain W3C validator