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

Theorem itg1climres 24318
 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 12284 . . 3 ℕ = (ℤ‘1)
2 1zzd 12016 . . 3 (𝜑 → 1 ∈ ℤ)
3 itg1climres.4 . . . . 5 (𝜑𝐹 ∈ dom ∫1)
4 i1frn 24281 . . . . 5 (𝐹 ∈ dom ∫1 → ran 𝐹 ∈ Fin)
53, 4syl 17 . . . 4 (𝜑 → ran 𝐹 ∈ Fin)
6 difss 4111 . . . 4 (ran 𝐹 ∖ {0}) ⊆ ran 𝐹
7 ssfi 8741 . . . 4 ((ran 𝐹 ∈ Fin ∧ (ran 𝐹 ∖ {0}) ⊆ ran 𝐹) → (ran 𝐹 ∖ {0}) ∈ Fin)
85, 6, 7sylancl 588 . . 3 (𝜑 → (ran 𝐹 ∖ {0}) ∈ Fin)
9 1zzd 12016 . . . 4 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → 1 ∈ ℤ)
10 i1fima 24282 . . . . . . . . . . . 12 (𝐹 ∈ dom ∫1 → (𝐹 “ {𝑘}) ∈ dom vol)
113, 10syl 17 . . . . . . . . . . 11 (𝜑 → (𝐹 “ {𝑘}) ∈ dom vol)
1211ad2antrr 724 . . . . . . . . . 10 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (𝐹 “ {𝑘}) ∈ dom vol)
13 itg1climres.1 . . . . . . . . . . . 12 (𝜑𝐴:ℕ⟶dom vol)
1413ffvelrnda 6854 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ∈ dom vol)
1514adantlr 713 . . . . . . . . . 10 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (𝐴𝑛) ∈ dom vol)
16 inmbl 24146 . . . . . . . . . 10 (((𝐹 “ {𝑘}) ∈ dom vol ∧ (𝐴𝑛) ∈ dom vol) → ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ∈ dom vol)
1712, 15, 16syl2anc 586 . . . . . . . . 9 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ∈ dom vol)
18 mblvol 24134 . . . . . . . . 9 (((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ∈ dom vol → (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) = (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
1917, 18syl 17 . . . . . . . 8 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) = (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
20 inss1 4208 . . . . . . . . . 10 ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ (𝐹 “ {𝑘})
2120a1i 11 . . . . . . . . 9 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ (𝐹 “ {𝑘}))
22 mblss 24135 . . . . . . . . . 10 ((𝐹 “ {𝑘}) ∈ dom vol → (𝐹 “ {𝑘}) ⊆ ℝ)
2312, 22syl 17 . . . . . . . . 9 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (𝐹 “ {𝑘}) ⊆ ℝ)
24 mblvol 24134 . . . . . . . . . . 11 ((𝐹 “ {𝑘}) ∈ dom vol → (vol‘(𝐹 “ {𝑘})) = (vol*‘(𝐹 “ {𝑘})))
2512, 24syl 17 . . . . . . . . . 10 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘(𝐹 “ {𝑘})) = (vol*‘(𝐹 “ {𝑘})))
26 i1fima2sn 24284 . . . . . . . . . . . 12 ((𝐹 ∈ dom ∫1𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(𝐹 “ {𝑘})) ∈ ℝ)
273, 26sylan 582 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(𝐹 “ {𝑘})) ∈ ℝ)
2827adantr 483 . . . . . . . . . 10 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘(𝐹 “ {𝑘})) ∈ ℝ)
2925, 28eqeltrrd 2917 . . . . . . . . 9 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol*‘(𝐹 “ {𝑘})) ∈ ℝ)
30 ovolsscl 24090 . . . . . . . . 9 ((((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ (𝐹 “ {𝑘}) ∧ (𝐹 “ {𝑘}) ⊆ ℝ ∧ (vol*‘(𝐹 “ {𝑘})) ∈ ℝ) → (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ∈ ℝ)
3121, 23, 29, 30syl3anc 1367 . . . . . . . 8 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ∈ ℝ)
3219, 31eqeltrd 2916 . . . . . . 7 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ∈ ℝ)
3332fmpttd 6882 . . . . . 6 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))):ℕ⟶ℝ)
34 itg1climres.2 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ⊆ (𝐴‘(𝑛 + 1)))
3534adantlr 713 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (𝐴𝑛) ⊆ (𝐴‘(𝑛 + 1)))
36 sslin 4214 . . . . . . . . . . . 12 ((𝐴𝑛) ⊆ (𝐴‘(𝑛 + 1)) → ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))))
3735, 36syl 17 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))))
3813adantr 483 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝐴:ℕ⟶dom vol)
39 peano2nn 11653 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ)
40 ffvelrn 6852 . . . . . . . . . . . . . 14 ((𝐴:ℕ⟶dom vol ∧ (𝑛 + 1) ∈ ℕ) → (𝐴‘(𝑛 + 1)) ∈ dom vol)
4138, 39, 40syl2an 597 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (𝐴‘(𝑛 + 1)) ∈ dom vol)
42 inmbl 24146 . . . . . . . . . . . . 13 (((𝐹 “ {𝑘}) ∈ dom vol ∧ (𝐴‘(𝑛 + 1)) ∈ dom vol) → ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ∈ dom vol)
4312, 41, 42syl2anc 586 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ∈ dom vol)
44 mblss 24135 . . . . . . . . . . . 12 (((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ∈ dom vol → ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ⊆ ℝ)
4543, 44syl 17 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ⊆ ℝ)
46 ovolss 24089 . . . . . . . . . . 11 ((((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ∧ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ⊆ ℝ) → (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))))
4737, 45, 46syl2anc 586 . . . . . . . . . 10 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))))
48 mblvol 24134 . . . . . . . . . . 11 (((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ∈ dom vol → (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) = (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))))
4943, 48syl 17 . . . . . . . . . 10 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) = (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))))
5047, 19, 493brtr4d 5101 . . . . . . . . 9 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))))
5150ralrimiva 3185 . . . . . . . 8 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑛 ∈ ℕ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))))
52 fveq2 6673 . . . . . . . . . . . . . 14 (𝑛 = 𝑗 → (𝐴𝑛) = (𝐴𝑗))
5352ineq2d 4192 . . . . . . . . . . . . 13 (𝑛 = 𝑗 → ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) = ((𝐹 “ {𝑘}) ∩ (𝐴𝑗)))
5453fveq2d 6677 . . . . . . . . . . . 12 (𝑛 = 𝑗 → (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) = (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))))
55 eqid 2824 . . . . . . . . . . . 12 (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
56 fvex 6686 . . . . . . . . . . . 12 (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))) ∈ V
5754, 55, 56fvmpt 6771 . . . . . . . . . . 11 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) = (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))))
58 peano2nn 11653 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℕ)
59 fveq2 6673 . . . . . . . . . . . . . . 15 (𝑛 = (𝑗 + 1) → (𝐴𝑛) = (𝐴‘(𝑗 + 1)))
6059ineq2d 4192 . . . . . . . . . . . . . 14 (𝑛 = (𝑗 + 1) → ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) = ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))
6160fveq2d 6677 . . . . . . . . . . . . 13 (𝑛 = (𝑗 + 1) → (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) = (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))))
62 fvex 6686 . . . . . . . . . . . . 13 (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))) ∈ V
6361, 55, 62fvmpt 6771 . . . . . . . . . . . 12 ((𝑗 + 1) ∈ ℕ → ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘(𝑗 + 1)) = (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))))
6458, 63syl 17 . . . . . . . . . . 11 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘(𝑗 + 1)) = (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))))
6557, 64breq12d 5082 . . . . . . . . . 10 (𝑗 ∈ ℕ → (((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘(𝑗 + 1)) ↔ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))) ≤ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))))
6665ralbiia 3167 . . . . . . . . 9 (∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘(𝑗 + 1)) ↔ ∀𝑗 ∈ ℕ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))) ≤ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))))
67 fvoveq1 7182 . . . . . . . . . . . . 13 (𝑛 = 𝑗 → (𝐴‘(𝑛 + 1)) = (𝐴‘(𝑗 + 1)))
6867ineq2d 4192 . . . . . . . . . . . 12 (𝑛 = 𝑗 → ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) = ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))
6968fveq2d 6677 . . . . . . . . . . 11 (𝑛 = 𝑗 → (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) = (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))))
7054, 69breq12d 5082 . . . . . . . . . 10 (𝑛 = 𝑗 → ((vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) ↔ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))) ≤ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))))
7170cbvralvw 3452 . . . . . . . . 9 (∀𝑛 ∈ ℕ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) ↔ ∀𝑗 ∈ ℕ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))) ≤ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))))
7266, 71bitr4i 280 . . . . . . . 8 (∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘(𝑗 + 1)) ↔ ∀𝑛 ∈ ℕ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))))
7351, 72sylibr 236 . . . . . . 7 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘(𝑗 + 1)))
7473r19.21bi 3211 . . . . . 6 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘(𝑗 + 1)))
75 ovolss 24089 . . . . . . . . . . 11 ((((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ (𝐹 “ {𝑘}) ∧ (𝐹 “ {𝑘}) ⊆ ℝ) → (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol*‘(𝐹 “ {𝑘})))
7620, 23, 75sylancr 589 . . . . . . . . . 10 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol*‘(𝐹 “ {𝑘})))
7776, 19, 253brtr4d 5101 . . . . . . . . 9 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol‘(𝐹 “ {𝑘})))
7877ralrimiva 3185 . . . . . . . 8 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑛 ∈ ℕ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol‘(𝐹 “ {𝑘})))
7957breq1d 5079 . . . . . . . . . 10 (𝑗 ∈ ℕ → (((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ (vol‘(𝐹 “ {𝑘})) ↔ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))) ≤ (vol‘(𝐹 “ {𝑘}))))
8079ralbiia 3167 . . . . . . . . 9 (∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ (vol‘(𝐹 “ {𝑘})) ↔ ∀𝑗 ∈ ℕ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))) ≤ (vol‘(𝐹 “ {𝑘})))
8154breq1d 5079 . . . . . . . . . 10 (𝑛 = 𝑗 → ((vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol‘(𝐹 “ {𝑘})) ↔ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))) ≤ (vol‘(𝐹 “ {𝑘}))))
8281cbvralvw 3452 . . . . . . . . 9 (∀𝑛 ∈ ℕ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol‘(𝐹 “ {𝑘})) ↔ ∀𝑗 ∈ ℕ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))) ≤ (vol‘(𝐹 “ {𝑘})))
8380, 82bitr4i 280 . . . . . . . 8 (∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ (vol‘(𝐹 “ {𝑘})) ↔ ∀𝑛 ∈ ℕ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol‘(𝐹 “ {𝑘})))
8478, 83sylibr 236 . . . . . . 7 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ (vol‘(𝐹 “ {𝑘})))
85 brralrspcev 5129 . . . . . . 7 (((vol‘(𝐹 “ {𝑘})) ∈ ℝ ∧ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ (vol‘(𝐹 “ {𝑘}))) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ 𝑥)
8627, 84, 85syl2anc 586 . . . . . 6 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ 𝑥)
871, 9, 33, 74, 86climsup 15029 . . . . 5 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) ⇝ sup(ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ, < ))
8817fmpttd 6882 . . . . . . 7 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))):ℕ⟶dom vol)
8937ralrimiva 3185 . . . . . . . 8 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑛 ∈ ℕ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))))
90 eqid 2824 . . . . . . . . . . . 12 (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) = (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))
91 fvex 6686 . . . . . . . . . . . . 13 (𝐴𝑗) ∈ V
9291inex2 5225 . . . . . . . . . . . 12 ((𝐹 “ {𝑘}) ∩ (𝐴𝑗)) ∈ V
9353, 90, 92fvmpt 6771 . . . . . . . . . . 11 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) = ((𝐹 “ {𝑘}) ∩ (𝐴𝑗)))
94 fvex 6686 . . . . . . . . . . . . . 14 (𝐴‘(𝑗 + 1)) ∈ V
9594inex2 5225 . . . . . . . . . . . . 13 ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))) ∈ V
9660, 90, 95fvmpt 6771 . . . . . . . . . . . 12 ((𝑗 + 1) ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘(𝑗 + 1)) = ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))
9758, 96syl 17 . . . . . . . . . . 11 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘(𝑗 + 1)) = ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))
9893, 97sseq12d 4003 . . . . . . . . . 10 (𝑗 ∈ ℕ → (((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) ⊆ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘(𝑗 + 1)) ↔ ((𝐹 “ {𝑘}) ∩ (𝐴𝑗)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))))
9998ralbiia 3167 . . . . . . . . 9 (∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) ⊆ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘(𝑗 + 1)) ↔ ∀𝑗 ∈ ℕ ((𝐹 “ {𝑘}) ∩ (𝐴𝑗)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))
10053, 68sseq12d 4003 . . . . . . . . . 10 (𝑛 = 𝑗 → (((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ↔ ((𝐹 “ {𝑘}) ∩ (𝐴𝑗)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))))
101100cbvralvw 3452 . . . . . . . . 9 (∀𝑛 ∈ ℕ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ↔ ∀𝑗 ∈ ℕ ((𝐹 “ {𝑘}) ∩ (𝐴𝑗)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))
10299, 101bitr4i 280 . . . . . . . 8 (∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) ⊆ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘(𝑗 + 1)) ↔ ∀𝑛 ∈ ℕ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))))
10389, 102sylibr 236 . . . . . . 7 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) ⊆ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘(𝑗 + 1)))
104 volsup 24160 . . . . . . 7 (((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))):ℕ⟶dom vol ∧ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) ⊆ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘(𝑗 + 1))) → (vol‘ ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = sup((vol “ ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ*, < ))
10588, 103, 104syl2anc 586 . . . . . 6 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘ ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = sup((vol “ ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ*, < ))
10693iuneq2i 4943 . . . . . . . . . 10 𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) = 𝑗 ∈ ℕ ((𝐹 “ {𝑘}) ∩ (𝐴𝑗))
10753cbviunv 4968 . . . . . . . . . 10 𝑛 ∈ ℕ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) = 𝑗 ∈ ℕ ((𝐹 “ {𝑘}) ∩ (𝐴𝑗))
108 iunin2 4996 . . . . . . . . . 10 𝑛 ∈ ℕ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) = ((𝐹 “ {𝑘}) ∩ 𝑛 ∈ ℕ (𝐴𝑛))
109106, 107, 1083eqtr2i 2853 . . . . . . . . 9 𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) = ((𝐹 “ {𝑘}) ∩ 𝑛 ∈ ℕ (𝐴𝑛))
110 ffn 6517 . . . . . . . . . . . . . 14 (𝐴:ℕ⟶dom vol → 𝐴 Fn ℕ)
111 fniunfv 7009 . . . . . . . . . . . . . 14 (𝐴 Fn ℕ → 𝑛 ∈ ℕ (𝐴𝑛) = ran 𝐴)
11213, 110, 1113syl 18 . . . . . . . . . . . . 13 (𝜑 𝑛 ∈ ℕ (𝐴𝑛) = ran 𝐴)
113 itg1climres.3 . . . . . . . . . . . . 13 (𝜑 ran 𝐴 = ℝ)
114112, 113eqtrd 2859 . . . . . . . . . . . 12 (𝜑 𝑛 ∈ ℕ (𝐴𝑛) = ℝ)
115114adantr 483 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑛 ∈ ℕ (𝐴𝑛) = ℝ)
116115ineq2d 4192 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ((𝐹 “ {𝑘}) ∩ 𝑛 ∈ ℕ (𝐴𝑛)) = ((𝐹 “ {𝑘}) ∩ ℝ))
11711adantr 483 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝐹 “ {𝑘}) ∈ dom vol)
118117, 22syl 17 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝐹 “ {𝑘}) ⊆ ℝ)
119 df-ss 3955 . . . . . . . . . . 11 ((𝐹 “ {𝑘}) ⊆ ℝ ↔ ((𝐹 “ {𝑘}) ∩ ℝ) = (𝐹 “ {𝑘}))
120118, 119sylib 220 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ((𝐹 “ {𝑘}) ∩ ℝ) = (𝐹 “ {𝑘}))
121116, 120eqtrd 2859 . . . . . . . . 9 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ((𝐹 “ {𝑘}) ∩ 𝑛 ∈ ℕ (𝐴𝑛)) = (𝐹 “ {𝑘}))
122109, 121syl5eq 2871 . . . . . . . 8 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) = (𝐹 “ {𝑘}))
123 ffn 6517 . . . . . . . . 9 ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))):ℕ⟶dom vol → (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) Fn ℕ)
124 fniunfv 7009 . . . . . . . . 9 ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) Fn ℕ → 𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) = ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
12588, 123, 1243syl 18 . . . . . . . 8 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) = ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
126122, 125eqtr3d 2861 . . . . . . 7 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝐹 “ {𝑘}) = ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
127126fveq2d 6677 . . . . . 6 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(𝐹 “ {𝑘})) = (vol‘ ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))
12833frnd 6524 . . . . . . . 8 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) ⊆ ℝ)
12933fdmd 6526 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → dom (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = ℕ)
130 1nn 11652 . . . . . . . . . . 11 1 ∈ ℕ
131 ne0i 4303 . . . . . . . . . . 11 (1 ∈ ℕ → ℕ ≠ ∅)
132130, 131mp1i 13 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ℕ ≠ ∅)
133129, 132eqnetrd 3086 . . . . . . . . 9 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → dom (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) ≠ ∅)
134 dm0rn0 5798 . . . . . . . . . 10 (dom (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = ∅ ↔ ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = ∅)
135134necon3bii 3071 . . . . . . . . 9 (dom (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) ≠ ∅ ↔ ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) ≠ ∅)
136133, 135sylib 220 . . . . . . . 8 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) ≠ ∅)
137 ffn 6517 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))):ℕ⟶ℝ → (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) Fn ℕ)
138 breq1 5072 . . . . . . . . . . . 12 (𝑧 = ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) → (𝑧𝑥 ↔ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ 𝑥))
139138ralrn 6857 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) Fn ℕ → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))𝑧𝑥 ↔ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ 𝑥))
14033, 137, 1393syl 18 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))𝑧𝑥 ↔ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ 𝑥))
141140rexbidv 3300 . . . . . . . . 9 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))𝑧𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ 𝑥))
14286, 141mpbird 259 . . . . . . . 8 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))𝑧𝑥)
143 supxrre 12723 . . . . . . . 8 ((ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))𝑧𝑥) → sup(ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ*, < ) = sup(ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ, < ))
144128, 136, 142, 143syl3anc 1367 . . . . . . 7 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → sup(ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ*, < ) = sup(ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ, < ))
145 rnco2 6109 . . . . . . . . 9 ran (vol ∘ (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = (vol “ ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
146 volf 24133 . . . . . . . . . . . 12 vol:dom vol⟶(0[,]+∞)
147146a1i 11 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → vol:dom vol⟶(0[,]+∞))
148147, 17cofmpt 6897 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol ∘ (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))
149148rneqd 5811 . . . . . . . . 9 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ran (vol ∘ (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))
150145, 149syl5reqr 2874 . . . . . . . 8 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = (vol “ ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))
151150supeq1d 8913 . . . . . . 7 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → sup(ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ*, < ) = sup((vol “ ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ*, < ))
152144, 151eqtr3d 2861 . . . . . 6 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → sup(ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ, < ) = sup((vol “ ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ*, < ))
153105, 127, 1523eqtr4d 2869 . . . . 5 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(𝐹 “ {𝑘})) = sup(ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ, < ))
15487, 153breqtrrd 5097 . . . 4 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) ⇝ (vol‘(𝐹 “ {𝑘})))
155 i1ff 24280 . . . . . . . 8 (𝐹 ∈ dom ∫1𝐹:ℝ⟶ℝ)
156 frn 6523 . . . . . . . 8 (𝐹:ℝ⟶ℝ → ran 𝐹 ⊆ ℝ)
1573, 155, 1563syl 18 . . . . . . 7 (𝜑 → ran 𝐹 ⊆ ℝ)
158157ssdifssd 4122 . . . . . 6 (𝜑 → (ran 𝐹 ∖ {0}) ⊆ ℝ)
159158sselda 3970 . . . . 5 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑘 ∈ ℝ)
160159recnd 10672 . . . 4 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑘 ∈ ℂ)
161 nnex 11647 . . . . . 6 ℕ ∈ V
162161mptex 6989 . . . . 5 (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))) ∈ V
163162a1i 11 . . . 4 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))) ∈ V)
16433ffvelrnda 6854 . . . . 5 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ∈ ℝ)
165164recnd 10672 . . . 4 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ∈ ℂ)
16654oveq2d 7175 . . . . . . 7 (𝑛 = 𝑗 → (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗)))))
167 eqid 2824 . . . . . . 7 (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))) = (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))
168 ovex 7192 . . . . . . 7 (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗)))) ∈ V
169166, 167, 168fvmpt 6771 . . . . . 6 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗) = (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗)))))
17057oveq2d 7175 . . . . . 6 (𝑗 ∈ ℕ → (𝑘 · ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗)) = (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗)))))
171169, 170eqtr4d 2862 . . . . 5 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗) = (𝑘 · ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗)))
172171adantl 484 . . . 4 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗) = (𝑘 · ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗)))
1731, 9, 154, 160, 163, 165, 172climmulc2 14996 . . 3 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))) ⇝ (𝑘 · (vol‘(𝐹 “ {𝑘}))))
174161mptex 6989 . . . 4 (𝑛 ∈ ℕ ↦ (∫1𝐺)) ∈ V
175174a1i 11 . . 3 (𝜑 → (𝑛 ∈ ℕ ↦ (∫1𝐺)) ∈ V)
176159adantr 483 . . . . . . . 8 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → 𝑘 ∈ ℝ)
177176, 32remulcld 10674 . . . . . . 7 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) ∈ ℝ)
178177fmpttd 6882 . . . . . 6 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))):ℕ⟶ℝ)
179178ffvelrnda 6854 . . . . 5 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗) ∈ ℝ)
180179recnd 10672 . . . 4 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗) ∈ ℂ)
181180anasss 469 . . 3 ((𝜑 ∧ (𝑘 ∈ (ran 𝐹 ∖ {0}) ∧ 𝑗 ∈ ℕ)) → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗) ∈ ℂ)
1823adantr 483 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝐹 ∈ dom ∫1)
183 itg1climres.5 . . . . . . . . . 10 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0))
184183i1fres 24309 . . . . . . . . 9 ((𝐹 ∈ dom ∫1 ∧ (𝐴𝑛) ∈ dom vol) → 𝐺 ∈ dom ∫1)
185182, 14, 184syl2anc 586 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝐺 ∈ dom ∫1)
1868adantr 483 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (ran 𝐹 ∖ {0}) ∈ Fin)
187 ffn 6517 . . . . . . . . . . . . . 14 (𝐹:ℝ⟶ℝ → 𝐹 Fn ℝ)
1883, 155, 1873syl 18 . . . . . . . . . . . . 13 (𝜑𝐹 Fn ℝ)
189188adantr 483 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → 𝐹 Fn ℝ)
190 fnfvelrn 6851 . . . . . . . . . . . 12 ((𝐹 Fn ℝ ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ran 𝐹)
191189, 190sylan 582 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ran 𝐹)
192 i1f0rn 24286 . . . . . . . . . . . . 13 (𝐹 ∈ dom ∫1 → 0 ∈ ran 𝐹)
1933, 192syl 17 . . . . . . . . . . . 12 (𝜑 → 0 ∈ ran 𝐹)
194193ad2antrr 724 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ∈ ran 𝐹)
195191, 194ifcld 4515 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) ∈ ran 𝐹)
196195, 183fmptd 6881 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝐺:ℝ⟶ran 𝐹)
197 frn 6523 . . . . . . . . 9 (𝐺:ℝ⟶ran 𝐹 → ran 𝐺 ⊆ ran 𝐹)
198 ssdif 4119 . . . . . . . . 9 (ran 𝐺 ⊆ ran 𝐹 → (ran 𝐺 ∖ {0}) ⊆ (ran 𝐹 ∖ {0}))
199196, 197, 1983syl 18 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (ran 𝐺 ∖ {0}) ⊆ (ran 𝐹 ∖ {0}))
200157adantr 483 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ran 𝐹 ⊆ ℝ)
201200ssdifd 4120 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (ran 𝐹 ∖ {0}) ⊆ (ℝ ∖ {0}))
202 itg1val2 24288 . . . . . . . 8 ((𝐺 ∈ dom ∫1 ∧ ((ran 𝐹 ∖ {0}) ∈ Fin ∧ (ran 𝐺 ∖ {0}) ⊆ (ran 𝐹 ∖ {0}) ∧ (ran 𝐹 ∖ {0}) ⊆ (ℝ ∖ {0}))) → (∫1𝐺) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(𝐺 “ {𝑘}))))
203185, 186, 199, 201, 202syl13anc 1368 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (∫1𝐺) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(𝐺 “ {𝑘}))))
204 fvex 6686 . . . . . . . . . . . . . . . . . . . . 21 (𝐹𝑥) ∈ V
205 c0ex 10638 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ V
206204, 205ifex 4518 . . . . . . . . . . . . . . . . . . . 20 if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) ∈ V
207183fvmpt2 6782 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) ∈ V) → (𝐺𝑥) = if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0))
208206, 207mpan2 689 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ → (𝐺𝑥) = if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0))
209208adantl 484 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝐺𝑥) = if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0))
210209eqeq1d 2826 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑥) = 𝑘 ↔ if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 𝑘))
211 eldifsni 4725 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ (ran 𝐹 ∖ {0}) → 𝑘 ≠ 0)
212211ad2antlr 725 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ≠ 0)
213 neeq1 3081 . . . . . . . . . . . . . . . . . . . 20 (if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 𝑘 → (if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) ≠ 0 ↔ 𝑘 ≠ 0))
214212, 213syl5ibrcom 249 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 𝑘 → if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) ≠ 0))
215 iffalse 4479 . . . . . . . . . . . . . . . . . . . 20 𝑥 ∈ (𝐴𝑛) → if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 0)
216215necon1ai 3046 . . . . . . . . . . . . . . . . . . 19 (if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) ≠ 0 → 𝑥 ∈ (𝐴𝑛))
217214, 216syl6 35 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 𝑘𝑥 ∈ (𝐴𝑛)))
218217pm4.71rd 565 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 𝑘 ↔ (𝑥 ∈ (𝐴𝑛) ∧ if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 𝑘)))
219210, 218bitrd 281 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑥) = 𝑘 ↔ (𝑥 ∈ (𝐴𝑛) ∧ if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 𝑘)))
220 iftrue 4476 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝐴𝑛) → if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = (𝐹𝑥))
221220eqeq1d 2826 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴𝑛) → (if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 𝑘 ↔ (𝐹𝑥) = 𝑘))
222221pm5.32i 577 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (𝐴𝑛) ∧ if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 𝑘) ↔ (𝑥 ∈ (𝐴𝑛) ∧ (𝐹𝑥) = 𝑘))
223222biancomi 465 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (𝐴𝑛) ∧ if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 𝑘) ↔ ((𝐹𝑥) = 𝑘𝑥 ∈ (𝐴𝑛)))
224219, 223syl6bb 289 . . . . . . . . . . . . . . 15 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑥) = 𝑘 ↔ ((𝐹𝑥) = 𝑘𝑥 ∈ (𝐴𝑛))))
225224pm5.32da 581 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ((𝑥 ∈ ℝ ∧ (𝐺𝑥) = 𝑘) ↔ (𝑥 ∈ ℝ ∧ ((𝐹𝑥) = 𝑘𝑥 ∈ (𝐴𝑛)))))
226 anass 471 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℝ ∧ (𝐹𝑥) = 𝑘) ∧ 𝑥 ∈ (𝐴𝑛)) ↔ (𝑥 ∈ ℝ ∧ ((𝐹𝑥) = 𝑘𝑥 ∈ (𝐴𝑛))))
227225, 226syl6bbr 291 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ((𝑥 ∈ ℝ ∧ (𝐺𝑥) = 𝑘) ↔ ((𝑥 ∈ ℝ ∧ (𝐹𝑥) = 𝑘) ∧ 𝑥 ∈ (𝐴𝑛))))
228 i1ff 24280 . . . . . . . . . . . . . . . 16 (𝐺 ∈ dom ∫1𝐺:ℝ⟶ℝ)
229 ffn 6517 . . . . . . . . . . . . . . . 16 (𝐺:ℝ⟶ℝ → 𝐺 Fn ℝ)
230185, 228, 2293syl 18 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → 𝐺 Fn ℝ)
231230adantr 483 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝐺 Fn ℝ)
232 fniniseg 6833 . . . . . . . . . . . . . 14 (𝐺 Fn ℝ → (𝑥 ∈ (𝐺 “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ (𝐺𝑥) = 𝑘)))
233231, 232syl 17 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑥 ∈ (𝐺 “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ (𝐺𝑥) = 𝑘)))
234 elin 4172 . . . . . . . . . . . . . 14 (𝑥 ∈ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ↔ (𝑥 ∈ (𝐹 “ {𝑘}) ∧ 𝑥 ∈ (𝐴𝑛)))
235189adantr 483 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝐹 Fn ℝ)
236 fniniseg 6833 . . . . . . . . . . . . . . . 16 (𝐹 Fn ℝ → (𝑥 ∈ (𝐹 “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ (𝐹𝑥) = 𝑘)))
237235, 236syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑥 ∈ (𝐹 “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ (𝐹𝑥) = 𝑘)))
238237anbi1d 631 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ((𝑥 ∈ (𝐹 “ {𝑘}) ∧ 𝑥 ∈ (𝐴𝑛)) ↔ ((𝑥 ∈ ℝ ∧ (𝐹𝑥) = 𝑘) ∧ 𝑥 ∈ (𝐴𝑛))))
239234, 238syl5bb 285 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑥 ∈ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ↔ ((𝑥 ∈ ℝ ∧ (𝐹𝑥) = 𝑘) ∧ 𝑥 ∈ (𝐴𝑛))))
240227, 233, 2393bitr4d 313 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑥 ∈ (𝐺 “ {𝑘}) ↔ 𝑥 ∈ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
241240alrimiv 1927 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑥(𝑥 ∈ (𝐺 “ {𝑘}) ↔ 𝑥 ∈ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
242 nfmpt1 5167 . . . . . . . . . . . . . . 15 𝑥(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0))
243183, 242nfcxfr 2978 . . . . . . . . . . . . . 14 𝑥𝐺
244243nfcnv 5752 . . . . . . . . . . . . 13 𝑥𝐺
245 nfcv 2980 . . . . . . . . . . . . 13 𝑥{𝑘}
246244, 245nfima 5940 . . . . . . . . . . . 12 𝑥(𝐺 “ {𝑘})
247 nfcv 2980 . . . . . . . . . . . 12 𝑥((𝐹 “ {𝑘}) ∩ (𝐴𝑛))
248246, 247cleqf 3013 . . . . . . . . . . 11 ((𝐺 “ {𝑘}) = ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ↔ ∀𝑥(𝑥 ∈ (𝐺 “ {𝑘}) ↔ 𝑥 ∈ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
249241, 248sylibr 236 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝐺 “ {𝑘}) = ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))
250249fveq2d 6677 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(𝐺 “ {𝑘})) = (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
251250oveq2d 7175 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑘 · (vol‘(𝐺 “ {𝑘}))) = (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))
252251sumeq2dv 15063 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(𝐺 “ {𝑘}))) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))
253203, 252eqtrd 2859 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (∫1𝐺) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))
254253mpteq2dva 5164 . . . . 5 (𝜑 → (𝑛 ∈ ℕ ↦ (∫1𝐺)) = (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))))
255254fveq1d 6675 . . . 4 (𝜑 → ((𝑛 ∈ ℕ ↦ (∫1𝐺))‘𝑗) = ((𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗))
256166sumeq2sdv 15064 . . . . . 6 (𝑛 = 𝑗 → Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗)))))
257 eqid 2824 . . . . . 6 (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))) = (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))
258 sumex 15047 . . . . . 6 Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗)))) ∈ V
259256, 257, 258fvmpt 6771 . . . . 5 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗)))))
260169sumeq2sdv 15064 . . . . 5 (𝑗 ∈ ℕ → Σ𝑘 ∈ (ran 𝐹 ∖ {0})((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗)))))
261259, 260eqtr4d 2862 . . . 4 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗))
262255, 261sylan9eq 2879 . . 3 ((𝜑𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (∫1𝐺))‘𝑗) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗))
2631, 2, 8, 173, 175, 181, 262climfsum 15178 . 2 (𝜑 → (𝑛 ∈ ℕ ↦ (∫1𝐺)) ⇝ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(𝐹 “ {𝑘}))))
264 itg1val 24287 . . 3 (𝐹 ∈ dom ∫1 → (∫1𝐹) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(𝐹 “ {𝑘}))))
2653, 264syl 17 . 2 (𝜑 → (∫1𝐹) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(𝐹 “ {𝑘}))))
266263, 265breqtrrd 5097 1 (𝜑 → (𝑛 ∈ ℕ ↦ (∫1𝐺)) ⇝ (∫1𝐹))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1534   = wceq 1536   ∈ wcel 2113   ≠ wne 3019  ∀wral 3141  ∃wrex 3142  Vcvv 3497   ∖ cdif 3936   ∩ cin 3938   ⊆ wss 3939  ∅c0 4294  ifcif 4470  {csn 4570  ∪ cuni 4841  ∪ ciun 4922   class class class wbr 5069   ↦ cmpt 5149  ◡ccnv 5557  dom cdm 5558  ran crn 5559   “ cima 5561   ∘ ccom 5562   Fn wfn 6353  ⟶wf 6354  ‘cfv 6358  (class class class)co 7159  Fincfn 8512  supcsup 8907  ℂcc 10538  ℝcr 10539  0cc0 10540  1c1 10541   + caddc 10543   · cmul 10545  +∞cpnf 10675  ℝ*cxr 10677   < clt 10678   ≤ cle 10679  ℕcn 11641  [,]cicc 12744   ⇝ cli 14844  Σcsu 15045  vol*covol 24066  volcvol 24067  ∫1citg1 24219 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-rep 5193  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464  ax-inf2 9107  ax-cc 9860  ax-cnex 10596  ax-resscn 10597  ax-1cn 10598  ax-icn 10599  ax-addcl 10600  ax-addrcl 10601  ax-mulcl 10602  ax-mulrcl 10603  ax-mulcom 10604  ax-addass 10605  ax-mulass 10606  ax-distr 10607  ax-i2m1 10608  ax-1ne0 10609  ax-1rid 10610  ax-rnegex 10611  ax-rrecex 10612  ax-cnre 10613  ax-pre-lttri 10614  ax-pre-lttrn 10615  ax-pre-ltadd 10616  ax-pre-mulgt0 10617  ax-pre-sup 10618  ax-addf 10619 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1539  df-fal 1549  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-nel 3127  df-ral 3146  df-rex 3147  df-reu 3148  df-rmo 3149  df-rab 3150  df-v 3499  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-tp 4575  df-op 4577  df-uni 4842  df-int 4880  df-iun 4924  df-disj 5035  df-br 5070  df-opab 5132  df-mpt 5150  df-tr 5176  df-id 5463  df-eprel 5468  df-po 5477  df-so 5478  df-fr 5517  df-se 5518  df-we 5519  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-pred 6151  df-ord 6197  df-on 6198  df-lim 6199  df-suc 6200  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-isom 6367  df-riota 7117  df-ov 7162  df-oprab 7163  df-mpo 7164  df-of 7412  df-om 7584  df-1st 7692  df-2nd 7693  df-wrecs 7950  df-recs 8011  df-rdg 8049  df-1o 8105  df-2o 8106  df-oadd 8109  df-er 8292  df-map 8411  df-pm 8412  df-en 8513  df-dom 8514  df-sdom 8515  df-fin 8516  df-fi 8878  df-sup 8909  df-inf 8910  df-oi 8977  df-dju 9333  df-card 9371  df-pnf 10680  df-mnf 10681  df-xr 10682  df-ltxr 10683  df-le 10684  df-sub 10875  df-neg 10876  df-div 11301  df-nn 11642  df-2 11703  df-3 11704  df-n0 11901  df-z 11985  df-uz 12247  df-q 12352  df-rp 12393  df-xneg 12510  df-xadd 12511  df-xmul 12512  df-ioo 12745  df-ico 12747  df-icc 12748  df-fz 12896  df-fzo 13037  df-fl 13165  df-seq 13373  df-exp 13433  df-hash 13694  df-cj 14461  df-re 14462  df-im 14463  df-sqrt 14597  df-abs 14598  df-clim 14848  df-rlim 14849  df-sum 15046  df-rest 16699  df-topgen 16720  df-psmet 20540  df-xmet 20541  df-met 20542  df-bl 20543  df-mopn 20544  df-top 21505  df-topon 21522  df-bases 21557  df-cmp 21998  df-ovol 24068  df-vol 24069  df-mbf 24223  df-itg1 24224 This theorem is referenced by:  itg2monolem1  24354
 Copyright terms: Public domain W3C validator