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

Theorem itg1climres 23387
 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 11667 . . 3 ℕ = (ℤ‘1)
2 1zzd 11352 . . 3 (𝜑 → 1 ∈ ℤ)
3 itg1climres.4 . . . . 5 (𝜑𝐹 ∈ dom ∫1)
4 i1frn 23350 . . . . 5 (𝐹 ∈ dom ∫1 → ran 𝐹 ∈ Fin)
53, 4syl 17 . . . 4 (𝜑 → ran 𝐹 ∈ Fin)
6 difss 3715 . . . 4 (ran 𝐹 ∖ {0}) ⊆ ran 𝐹
7 ssfi 8124 . . . 4 ((ran 𝐹 ∈ Fin ∧ (ran 𝐹 ∖ {0}) ⊆ ran 𝐹) → (ran 𝐹 ∖ {0}) ∈ Fin)
85, 6, 7sylancl 693 . . 3 (𝜑 → (ran 𝐹 ∖ {0}) ∈ Fin)
9 1zzd 11352 . . . 4 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → 1 ∈ ℤ)
10 i1fima 23351 . . . . . . . . . . . 12 (𝐹 ∈ dom ∫1 → (𝐹 “ {𝑘}) ∈ dom vol)
113, 10syl 17 . . . . . . . . . . 11 (𝜑 → (𝐹 “ {𝑘}) ∈ dom vol)
1211ad2antrr 761 . . . . . . . . . 10 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (𝐹 “ {𝑘}) ∈ dom vol)
13 itg1climres.1 . . . . . . . . . . . 12 (𝜑𝐴:ℕ⟶dom vol)
1413ffvelrnda 6315 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ∈ dom vol)
1514adantlr 750 . . . . . . . . . 10 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (𝐴𝑛) ∈ dom vol)
16 inmbl 23217 . . . . . . . . . 10 (((𝐹 “ {𝑘}) ∈ dom vol ∧ (𝐴𝑛) ∈ dom vol) → ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ∈ dom vol)
1712, 15, 16syl2anc 692 . . . . . . . . 9 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ∈ dom vol)
18 mblvol 23205 . . . . . . . . 9 (((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ∈ dom vol → (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) = (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
1917, 18syl 17 . . . . . . . 8 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) = (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
20 inss1 3811 . . . . . . . . . 10 ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ (𝐹 “ {𝑘})
2120a1i 11 . . . . . . . . 9 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ (𝐹 “ {𝑘}))
22 mblss 23206 . . . . . . . . . 10 ((𝐹 “ {𝑘}) ∈ dom vol → (𝐹 “ {𝑘}) ⊆ ℝ)
2312, 22syl 17 . . . . . . . . 9 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (𝐹 “ {𝑘}) ⊆ ℝ)
24 mblvol 23205 . . . . . . . . . . 11 ((𝐹 “ {𝑘}) ∈ dom vol → (vol‘(𝐹 “ {𝑘})) = (vol*‘(𝐹 “ {𝑘})))
2512, 24syl 17 . . . . . . . . . 10 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘(𝐹 “ {𝑘})) = (vol*‘(𝐹 “ {𝑘})))
26 i1fima2sn 23353 . . . . . . . . . . . 12 ((𝐹 ∈ dom ∫1𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(𝐹 “ {𝑘})) ∈ ℝ)
273, 26sylan 488 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(𝐹 “ {𝑘})) ∈ ℝ)
2827adantr 481 . . . . . . . . . 10 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘(𝐹 “ {𝑘})) ∈ ℝ)
2925, 28eqeltrrd 2699 . . . . . . . . 9 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol*‘(𝐹 “ {𝑘})) ∈ ℝ)
30 ovolsscl 23161 . . . . . . . . 9 ((((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ (𝐹 “ {𝑘}) ∧ (𝐹 “ {𝑘}) ⊆ ℝ ∧ (vol*‘(𝐹 “ {𝑘})) ∈ ℝ) → (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ∈ ℝ)
3121, 23, 29, 30syl3anc 1323 . . . . . . . 8 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ∈ ℝ)
3219, 31eqeltrd 2698 . . . . . . 7 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ∈ ℝ)
33 eqid 2621 . . . . . . 7 (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
3432, 33fmptd 6340 . . . . . 6 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))):ℕ⟶ℝ)
35 itg1climres.2 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ⊆ (𝐴‘(𝑛 + 1)))
3635adantlr 750 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (𝐴𝑛) ⊆ (𝐴‘(𝑛 + 1)))
37 sslin 3817 . . . . . . . . . . . 12 ((𝐴𝑛) ⊆ (𝐴‘(𝑛 + 1)) → ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))))
3836, 37syl 17 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))))
3913adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝐴:ℕ⟶dom vol)
40 peano2nn 10976 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ)
41 ffvelrn 6313 . . . . . . . . . . . . . 14 ((𝐴:ℕ⟶dom vol ∧ (𝑛 + 1) ∈ ℕ) → (𝐴‘(𝑛 + 1)) ∈ dom vol)
4239, 40, 41syl2an 494 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (𝐴‘(𝑛 + 1)) ∈ dom vol)
43 inmbl 23217 . . . . . . . . . . . . 13 (((𝐹 “ {𝑘}) ∈ dom vol ∧ (𝐴‘(𝑛 + 1)) ∈ dom vol) → ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ∈ dom vol)
4412, 42, 43syl2anc 692 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ∈ dom vol)
45 mblss 23206 . . . . . . . . . . . 12 (((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ∈ dom vol → ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ⊆ ℝ)
4644, 45syl 17 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ⊆ ℝ)
47 ovolss 23160 . . . . . . . . . . 11 ((((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ∧ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ⊆ ℝ) → (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))))
4838, 46, 47syl2anc 692 . . . . . . . . . 10 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))))
49 mblvol 23205 . . . . . . . . . . 11 (((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ∈ dom vol → (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) = (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))))
5044, 49syl 17 . . . . . . . . . 10 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) = (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))))
5148, 19, 503brtr4d 4645 . . . . . . . . 9 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))))
5251ralrimiva 2960 . . . . . . . 8 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑛 ∈ ℕ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))))
53 fveq2 6148 . . . . . . . . . . . . . 14 (𝑛 = 𝑗 → (𝐴𝑛) = (𝐴𝑗))
5453ineq2d 3792 . . . . . . . . . . . . 13 (𝑛 = 𝑗 → ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) = ((𝐹 “ {𝑘}) ∩ (𝐴𝑗)))
5554fveq2d 6152 . . . . . . . . . . . 12 (𝑛 = 𝑗 → (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) = (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))))
56 fvex 6158 . . . . . . . . . . . 12 (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))) ∈ V
5755, 33, 56fvmpt 6239 . . . . . . . . . . 11 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) = (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))))
58 peano2nn 10976 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℕ)
59 fveq2 6148 . . . . . . . . . . . . . . 15 (𝑛 = (𝑗 + 1) → (𝐴𝑛) = (𝐴‘(𝑗 + 1)))
6059ineq2d 3792 . . . . . . . . . . . . . 14 (𝑛 = (𝑗 + 1) → ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) = ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))
6160fveq2d 6152 . . . . . . . . . . . . 13 (𝑛 = (𝑗 + 1) → (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) = (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))))
62 fvex 6158 . . . . . . . . . . . . 13 (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))) ∈ V
6361, 33, 62fvmpt 6239 . . . . . . . . . . . 12 ((𝑗 + 1) ∈ ℕ → ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘(𝑗 + 1)) = (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))))
6458, 63syl 17 . . . . . . . . . . 11 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘(𝑗 + 1)) = (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))))
6557, 64breq12d 4626 . . . . . . . . . 10 (𝑗 ∈ ℕ → (((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘(𝑗 + 1)) ↔ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))) ≤ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))))
6665ralbiia 2973 . . . . . . . . 9 (∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘(𝑗 + 1)) ↔ ∀𝑗 ∈ ℕ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))) ≤ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))))
67 oveq1 6611 . . . . . . . . . . . . . 14 (𝑛 = 𝑗 → (𝑛 + 1) = (𝑗 + 1))
6867fveq2d 6152 . . . . . . . . . . . . 13 (𝑛 = 𝑗 → (𝐴‘(𝑛 + 1)) = (𝐴‘(𝑗 + 1)))
6968ineq2d 3792 . . . . . . . . . . . 12 (𝑛 = 𝑗 → ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) = ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))
7069fveq2d 6152 . . . . . . . . . . 11 (𝑛 = 𝑗 → (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) = (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))))
7155, 70breq12d 4626 . . . . . . . . . 10 (𝑛 = 𝑗 → ((vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) ↔ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))) ≤ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))))
7271cbvralv 3159 . . . . . . . . 9 (∀𝑛 ∈ ℕ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) ↔ ∀𝑗 ∈ ℕ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))) ≤ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))))
7366, 72bitr4i 267 . . . . . . . 8 (∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘(𝑗 + 1)) ↔ ∀𝑛 ∈ ℕ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))))
7452, 73sylibr 224 . . . . . . 7 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘(𝑗 + 1)))
7574r19.21bi 2927 . . . . . 6 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘(𝑗 + 1)))
76 ovolss 23160 . . . . . . . . . . 11 ((((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ (𝐹 “ {𝑘}) ∧ (𝐹 “ {𝑘}) ⊆ ℝ) → (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol*‘(𝐹 “ {𝑘})))
7720, 23, 76sylancr 694 . . . . . . . . . 10 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol*‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol*‘(𝐹 “ {𝑘})))
7877, 19, 253brtr4d 4645 . . . . . . . . 9 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol‘(𝐹 “ {𝑘})))
7978ralrimiva 2960 . . . . . . . 8 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑛 ∈ ℕ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol‘(𝐹 “ {𝑘})))
8057breq1d 4623 . . . . . . . . . 10 (𝑗 ∈ ℕ → (((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ (vol‘(𝐹 “ {𝑘})) ↔ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))) ≤ (vol‘(𝐹 “ {𝑘}))))
8180ralbiia 2973 . . . . . . . . 9 (∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ (vol‘(𝐹 “ {𝑘})) ↔ ∀𝑗 ∈ ℕ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))) ≤ (vol‘(𝐹 “ {𝑘})))
8255breq1d 4623 . . . . . . . . . 10 (𝑛 = 𝑗 → ((vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol‘(𝐹 “ {𝑘})) ↔ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))) ≤ (vol‘(𝐹 “ {𝑘}))))
8382cbvralv 3159 . . . . . . . . 9 (∀𝑛 ∈ ℕ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol‘(𝐹 “ {𝑘})) ↔ ∀𝑗 ∈ ℕ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗))) ≤ (vol‘(𝐹 “ {𝑘})))
8481, 83bitr4i 267 . . . . . . . 8 (∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ (vol‘(𝐹 “ {𝑘})) ↔ ∀𝑛 ∈ ℕ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) ≤ (vol‘(𝐹 “ {𝑘})))
8579, 84sylibr 224 . . . . . . 7 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ (vol‘(𝐹 “ {𝑘})))
86 breq2 4617 . . . . . . . . 9 (𝑥 = (vol‘(𝐹 “ {𝑘})) → (((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ 𝑥 ↔ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ (vol‘(𝐹 “ {𝑘}))))
8786ralbidv 2980 . . . . . . . 8 (𝑥 = (vol‘(𝐹 “ {𝑘})) → (∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ (vol‘(𝐹 “ {𝑘}))))
8887rspcev 3295 . . . . . . 7 (((vol‘(𝐹 “ {𝑘})) ∈ ℝ ∧ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ (vol‘(𝐹 “ {𝑘}))) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ 𝑥)
8927, 85, 88syl2anc 692 . . . . . 6 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ 𝑥)
901, 9, 34, 75, 89climsup 14334 . . . . 5 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) ⇝ sup(ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ, < ))
91 eqid 2621 . . . . . . . 8 (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) = (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))
9217, 91fmptd 6340 . . . . . . 7 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))):ℕ⟶dom vol)
9338ralrimiva 2960 . . . . . . . 8 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑛 ∈ ℕ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))))
94 fvex 6158 . . . . . . . . . . . . 13 (𝐴𝑗) ∈ V
9594inex2 4760 . . . . . . . . . . . 12 ((𝐹 “ {𝑘}) ∩ (𝐴𝑗)) ∈ V
9654, 91, 95fvmpt 6239 . . . . . . . . . . 11 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) = ((𝐹 “ {𝑘}) ∩ (𝐴𝑗)))
97 fvex 6158 . . . . . . . . . . . . . 14 (𝐴‘(𝑗 + 1)) ∈ V
9897inex2 4760 . . . . . . . . . . . . 13 ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))) ∈ V
9960, 91, 98fvmpt 6239 . . . . . . . . . . . 12 ((𝑗 + 1) ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘(𝑗 + 1)) = ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))
10058, 99syl 17 . . . . . . . . . . 11 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘(𝑗 + 1)) = ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))
10196, 100sseq12d 3613 . . . . . . . . . 10 (𝑗 ∈ ℕ → (((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) ⊆ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘(𝑗 + 1)) ↔ ((𝐹 “ {𝑘}) ∩ (𝐴𝑗)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))))
102101ralbiia 2973 . . . . . . . . 9 (∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) ⊆ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘(𝑗 + 1)) ↔ ∀𝑗 ∈ ℕ ((𝐹 “ {𝑘}) ∩ (𝐴𝑗)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))
10354, 69sseq12d 3613 . . . . . . . . . 10 (𝑛 = 𝑗 → (((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ↔ ((𝐹 “ {𝑘}) ∩ (𝐴𝑗)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))))
104103cbvralv 3159 . . . . . . . . 9 (∀𝑛 ∈ ℕ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ↔ ∀𝑗 ∈ ℕ ((𝐹 “ {𝑘}) ∩ (𝐴𝑗)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))
105102, 104bitr4i 267 . . . . . . . 8 (∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) ⊆ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘(𝑗 + 1)) ↔ ∀𝑛 ∈ ℕ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ⊆ ((𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))))
10693, 105sylibr 224 . . . . . . 7 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) ⊆ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘(𝑗 + 1)))
107 volsup 23231 . . . . . . 7 (((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))):ℕ⟶dom vol ∧ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) ⊆ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘(𝑗 + 1))) → (vol‘ ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = sup((vol “ ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ*, < ))
10892, 106, 107syl2anc 692 . . . . . 6 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘ ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = sup((vol “ ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ*, < ))
10996iuneq2i 4505 . . . . . . . . . 10 𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) = 𝑗 ∈ ℕ ((𝐹 “ {𝑘}) ∩ (𝐴𝑗))
11054cbviunv 4525 . . . . . . . . . 10 𝑛 ∈ ℕ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) = 𝑗 ∈ ℕ ((𝐹 “ {𝑘}) ∩ (𝐴𝑗))
111 iunin2 4550 . . . . . . . . . 10 𝑛 ∈ ℕ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) = ((𝐹 “ {𝑘}) ∩ 𝑛 ∈ ℕ (𝐴𝑛))
112109, 110, 1113eqtr2i 2649 . . . . . . . . 9 𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) = ((𝐹 “ {𝑘}) ∩ 𝑛 ∈ ℕ (𝐴𝑛))
113 ffn 6002 . . . . . . . . . . . . . 14 (𝐴:ℕ⟶dom vol → 𝐴 Fn ℕ)
114 fniunfv 6459 . . . . . . . . . . . . . 14 (𝐴 Fn ℕ → 𝑛 ∈ ℕ (𝐴𝑛) = ran 𝐴)
11513, 113, 1143syl 18 . . . . . . . . . . . . 13 (𝜑 𝑛 ∈ ℕ (𝐴𝑛) = ran 𝐴)
116 itg1climres.3 . . . . . . . . . . . . 13 (𝜑 ran 𝐴 = ℝ)
117115, 116eqtrd 2655 . . . . . . . . . . . 12 (𝜑 𝑛 ∈ ℕ (𝐴𝑛) = ℝ)
118117adantr 481 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑛 ∈ ℕ (𝐴𝑛) = ℝ)
119118ineq2d 3792 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ((𝐹 “ {𝑘}) ∩ 𝑛 ∈ ℕ (𝐴𝑛)) = ((𝐹 “ {𝑘}) ∩ ℝ))
12011adantr 481 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝐹 “ {𝑘}) ∈ dom vol)
121120, 22syl 17 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝐹 “ {𝑘}) ⊆ ℝ)
122 df-ss 3569 . . . . . . . . . . 11 ((𝐹 “ {𝑘}) ⊆ ℝ ↔ ((𝐹 “ {𝑘}) ∩ ℝ) = (𝐹 “ {𝑘}))
123121, 122sylib 208 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ((𝐹 “ {𝑘}) ∩ ℝ) = (𝐹 “ {𝑘}))
124119, 123eqtrd 2655 . . . . . . . . 9 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ((𝐹 “ {𝑘}) ∩ 𝑛 ∈ ℕ (𝐴𝑛)) = (𝐹 “ {𝑘}))
125112, 124syl5eq 2667 . . . . . . . 8 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) = (𝐹 “ {𝑘}))
126 ffn 6002 . . . . . . . . 9 ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))):ℕ⟶dom vol → (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) Fn ℕ)
127 fniunfv 6459 . . . . . . . . 9 ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) Fn ℕ → 𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) = ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
12892, 126, 1273syl 18 . . . . . . . 8 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))‘𝑗) = ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
129125, 128eqtr3d 2657 . . . . . . 7 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝐹 “ {𝑘}) = ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
130129fveq2d 6152 . . . . . 6 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(𝐹 “ {𝑘})) = (vol‘ ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))
131 frn 6010 . . . . . . . . 9 ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))):ℕ⟶ℝ → ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) ⊆ ℝ)
13234, 131syl 17 . . . . . . . 8 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) ⊆ ℝ)
133 fdm 6008 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))):ℕ⟶ℝ → dom (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = ℕ)
13434, 133syl 17 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → dom (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = ℕ)
135 1nn 10975 . . . . . . . . . . 11 1 ∈ ℕ
136 ne0i 3897 . . . . . . . . . . 11 (1 ∈ ℕ → ℕ ≠ ∅)
137135, 136mp1i 13 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ℕ ≠ ∅)
138134, 137eqnetrd 2857 . . . . . . . . 9 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → dom (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) ≠ ∅)
139 dm0rn0 5302 . . . . . . . . . 10 (dom (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = ∅ ↔ ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = ∅)
140139necon3bii 2842 . . . . . . . . 9 (dom (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) ≠ ∅ ↔ ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) ≠ ∅)
141138, 140sylib 208 . . . . . . . 8 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) ≠ ∅)
142 ffn 6002 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))):ℕ⟶ℝ → (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) Fn ℕ)
143 breq1 4616 . . . . . . . . . . . 12 (𝑧 = ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) → (𝑧𝑥 ↔ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ 𝑥))
144143ralrn 6318 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) Fn ℕ → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))𝑧𝑥 ↔ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ 𝑥))
14534, 142, 1443syl 18 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))𝑧𝑥 ↔ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ 𝑥))
146145rexbidv 3045 . . . . . . . . 9 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))𝑧𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ≤ 𝑥))
14789, 146mpbird 247 . . . . . . . 8 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))𝑧𝑥)
148 supxrre 12100 . . . . . . . 8 ((ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))𝑧𝑥) → sup(ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ*, < ) = sup(ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ, < ))
149132, 141, 147, 148syl3anc 1323 . . . . . . 7 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → sup(ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ*, < ) = sup(ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ, < ))
150 rnco2 5601 . . . . . . . . 9 ran (vol ∘ (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = (vol “ ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
151 eqidd 2622 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))) = (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
152 volf 23204 . . . . . . . . . . . . 13 vol:dom vol⟶(0[,]+∞)
153152a1i 11 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → vol:dom vol⟶(0[,]+∞))
154153feqmptd 6206 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → vol = (𝑦 ∈ dom vol ↦ (vol‘𝑦)))
155 fveq2 6148 . . . . . . . . . . 11 (𝑦 = ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) → (vol‘𝑦) = (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
15617, 151, 154, 155fmptco 6351 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol ∘ (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))
157156rneqd 5313 . . . . . . . . 9 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ran (vol ∘ (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))
158150, 157syl5reqr 2670 . . . . . . . 8 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = (vol “ ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))
159158supeq1d 8296 . . . . . . 7 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → sup(ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ*, < ) = sup((vol “ ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ*, < ))
160149, 159eqtr3d 2657 . . . . . 6 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → sup(ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ, < ) = sup((vol “ ran (𝑛 ∈ ℕ ↦ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ*, < ))
161108, 130, 1603eqtr4d 2665 . . . . 5 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(𝐹 “ {𝑘})) = sup(ran (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))), ℝ, < ))
16290, 161breqtrrd 4641 . . . 4 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) ⇝ (vol‘(𝐹 “ {𝑘})))
163 i1ff 23349 . . . . . . . 8 (𝐹 ∈ dom ∫1𝐹:ℝ⟶ℝ)
164 frn 6010 . . . . . . . 8 (𝐹:ℝ⟶ℝ → ran 𝐹 ⊆ ℝ)
1653, 163, 1643syl 18 . . . . . . 7 (𝜑 → ran 𝐹 ⊆ ℝ)
166165ssdifssd 3726 . . . . . 6 (𝜑 → (ran 𝐹 ∖ {0}) ⊆ ℝ)
167166sselda 3583 . . . . 5 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑘 ∈ ℝ)
168167recnd 10012 . . . 4 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑘 ∈ ℂ)
169 nnex 10970 . . . . . 6 ℕ ∈ V
170169mptex 6440 . . . . 5 (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))) ∈ V
171170a1i 11 . . . 4 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))) ∈ V)
17234ffvelrnda 6315 . . . . 5 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ∈ ℝ)
173172recnd 10012 . . . 4 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗) ∈ ℂ)
17455oveq2d 6620 . . . . . . 7 (𝑛 = 𝑗 → (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗)))))
175 eqid 2621 . . . . . . 7 (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))) = (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))
176 ovex 6632 . . . . . . 7 (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗)))) ∈ V
177174, 175, 176fvmpt 6239 . . . . . 6 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗) = (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗)))))
17857oveq2d 6620 . . . . . 6 (𝑗 ∈ ℕ → (𝑘 · ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗)) = (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗)))))
179177, 178eqtr4d 2658 . . . . 5 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗) = (𝑘 · ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗)))
180179adantl 482 . . . 4 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗) = (𝑘 · ((𝑛 ∈ ℕ ↦ (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))‘𝑗)))
1811, 9, 162, 168, 171, 173, 180climmulc2 14301 . . 3 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))) ⇝ (𝑘 · (vol‘(𝐹 “ {𝑘}))))
182169mptex 6440 . . . 4 (𝑛 ∈ ℕ ↦ (∫1𝐺)) ∈ V
183182a1i 11 . . 3 (𝜑 → (𝑛 ∈ ℕ ↦ (∫1𝐺)) ∈ V)
184167adantr 481 . . . . . . . 8 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → 𝑘 ∈ ℝ)
185184, 32remulcld 10014 . . . . . . 7 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) ∈ ℝ)
186185, 175fmptd 6340 . . . . . 6 ((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))):ℕ⟶ℝ)
187186ffvelrnda 6315 . . . . 5 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗) ∈ ℝ)
188187recnd 10012 . . . 4 (((𝜑𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗) ∈ ℂ)
189188anasss 678 . . 3 ((𝜑 ∧ (𝑘 ∈ (ran 𝐹 ∖ {0}) ∧ 𝑗 ∈ ℕ)) → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗) ∈ ℂ)
1903adantr 481 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝐹 ∈ dom ∫1)
191 itg1climres.5 . . . . . . . . . 10 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0))
192191i1fres 23378 . . . . . . . . 9 ((𝐹 ∈ dom ∫1 ∧ (𝐴𝑛) ∈ dom vol) → 𝐺 ∈ dom ∫1)
193190, 14, 192syl2anc 692 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝐺 ∈ dom ∫1)
1948adantr 481 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (ran 𝐹 ∖ {0}) ∈ Fin)
195 ffn 6002 . . . . . . . . . . . . . 14 (𝐹:ℝ⟶ℝ → 𝐹 Fn ℝ)
1963, 163, 1953syl 18 . . . . . . . . . . . . 13 (𝜑𝐹 Fn ℝ)
197196adantr 481 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → 𝐹 Fn ℝ)
198 fnfvelrn 6312 . . . . . . . . . . . 12 ((𝐹 Fn ℝ ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ran 𝐹)
199197, 198sylan 488 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ran 𝐹)
200 i1f0rn 23355 . . . . . . . . . . . . 13 (𝐹 ∈ dom ∫1 → 0 ∈ ran 𝐹)
2013, 200syl 17 . . . . . . . . . . . 12 (𝜑 → 0 ∈ ran 𝐹)
202201ad2antrr 761 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ∈ ran 𝐹)
203199, 202ifcld 4103 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) ∈ ran 𝐹)
204203, 191fmptd 6340 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝐺:ℝ⟶ran 𝐹)
205 frn 6010 . . . . . . . . 9 (𝐺:ℝ⟶ran 𝐹 → ran 𝐺 ⊆ ran 𝐹)
206 ssdif 3723 . . . . . . . . 9 (ran 𝐺 ⊆ ran 𝐹 → (ran 𝐺 ∖ {0}) ⊆ (ran 𝐹 ∖ {0}))
207204, 205, 2063syl 18 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (ran 𝐺 ∖ {0}) ⊆ (ran 𝐹 ∖ {0}))
208165adantr 481 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ran 𝐹 ⊆ ℝ)
209208ssdifd 3724 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (ran 𝐹 ∖ {0}) ⊆ (ℝ ∖ {0}))
210 itg1val2 23357 . . . . . . . 8 ((𝐺 ∈ dom ∫1 ∧ ((ran 𝐹 ∖ {0}) ∈ Fin ∧ (ran 𝐺 ∖ {0}) ⊆ (ran 𝐹 ∖ {0}) ∧ (ran 𝐹 ∖ {0}) ⊆ (ℝ ∖ {0}))) → (∫1𝐺) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(𝐺 “ {𝑘}))))
211193, 194, 207, 209, 210syl13anc 1325 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (∫1𝐺) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(𝐺 “ {𝑘}))))
212 fvex 6158 . . . . . . . . . . . . . . . . . . . . 21 (𝐹𝑥) ∈ V
213 c0ex 9978 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ V
214212, 213ifex 4128 . . . . . . . . . . . . . . . . . . . 20 if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) ∈ V
215191fvmpt2 6248 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) ∈ V) → (𝐺𝑥) = if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0))
216214, 215mpan2 706 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ → (𝐺𝑥) = if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0))
217216adantl 482 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝐺𝑥) = if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0))
218217eqeq1d 2623 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑥) = 𝑘 ↔ if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 𝑘))
219 eldifsni 4289 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ (ran 𝐹 ∖ {0}) → 𝑘 ≠ 0)
220219ad2antlr 762 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ≠ 0)
221 neeq1 2852 . . . . . . . . . . . . . . . . . . . 20 (if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 𝑘 → (if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) ≠ 0 ↔ 𝑘 ≠ 0))
222220, 221syl5ibrcom 237 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 𝑘 → if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) ≠ 0))
223 iffalse 4067 . . . . . . . . . . . . . . . . . . . 20 𝑥 ∈ (𝐴𝑛) → if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 0)
224223necon1ai 2817 . . . . . . . . . . . . . . . . . . 19 (if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) ≠ 0 → 𝑥 ∈ (𝐴𝑛))
225222, 224syl6 35 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 𝑘𝑥 ∈ (𝐴𝑛)))
226225pm4.71rd 666 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 𝑘 ↔ (𝑥 ∈ (𝐴𝑛) ∧ if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 𝑘)))
227218, 226bitrd 268 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑥) = 𝑘 ↔ (𝑥 ∈ (𝐴𝑛) ∧ if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 𝑘)))
228 iftrue 4064 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝐴𝑛) → if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = (𝐹𝑥))
229228eqeq1d 2623 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴𝑛) → (if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 𝑘 ↔ (𝐹𝑥) = 𝑘))
230229pm5.32i 668 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (𝐴𝑛) ∧ if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 𝑘) ↔ (𝑥 ∈ (𝐴𝑛) ∧ (𝐹𝑥) = 𝑘))
231 ancom 466 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (𝐴𝑛) ∧ (𝐹𝑥) = 𝑘) ↔ ((𝐹𝑥) = 𝑘𝑥 ∈ (𝐴𝑛)))
232230, 231bitri 264 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (𝐴𝑛) ∧ if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0) = 𝑘) ↔ ((𝐹𝑥) = 𝑘𝑥 ∈ (𝐴𝑛)))
233227, 232syl6bb 276 . . . . . . . . . . . . . . 15 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑥) = 𝑘 ↔ ((𝐹𝑥) = 𝑘𝑥 ∈ (𝐴𝑛))))
234233pm5.32da 672 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ((𝑥 ∈ ℝ ∧ (𝐺𝑥) = 𝑘) ↔ (𝑥 ∈ ℝ ∧ ((𝐹𝑥) = 𝑘𝑥 ∈ (𝐴𝑛)))))
235 anass 680 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℝ ∧ (𝐹𝑥) = 𝑘) ∧ 𝑥 ∈ (𝐴𝑛)) ↔ (𝑥 ∈ ℝ ∧ ((𝐹𝑥) = 𝑘𝑥 ∈ (𝐴𝑛))))
236234, 235syl6bbr 278 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ((𝑥 ∈ ℝ ∧ (𝐺𝑥) = 𝑘) ↔ ((𝑥 ∈ ℝ ∧ (𝐹𝑥) = 𝑘) ∧ 𝑥 ∈ (𝐴𝑛))))
237 i1ff 23349 . . . . . . . . . . . . . . . 16 (𝐺 ∈ dom ∫1𝐺:ℝ⟶ℝ)
238 ffn 6002 . . . . . . . . . . . . . . . 16 (𝐺:ℝ⟶ℝ → 𝐺 Fn ℝ)
239193, 237, 2383syl 18 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → 𝐺 Fn ℝ)
240239adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝐺 Fn ℝ)
241 fniniseg 6294 . . . . . . . . . . . . . 14 (𝐺 Fn ℝ → (𝑥 ∈ (𝐺 “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ (𝐺𝑥) = 𝑘)))
242240, 241syl 17 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑥 ∈ (𝐺 “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ (𝐺𝑥) = 𝑘)))
243 elin 3774 . . . . . . . . . . . . . 14 (𝑥 ∈ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ↔ (𝑥 ∈ (𝐹 “ {𝑘}) ∧ 𝑥 ∈ (𝐴𝑛)))
244197adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝐹 Fn ℝ)
245 fniniseg 6294 . . . . . . . . . . . . . . . 16 (𝐹 Fn ℝ → (𝑥 ∈ (𝐹 “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ (𝐹𝑥) = 𝑘)))
246244, 245syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑥 ∈ (𝐹 “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ (𝐹𝑥) = 𝑘)))
247246anbi1d 740 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ((𝑥 ∈ (𝐹 “ {𝑘}) ∧ 𝑥 ∈ (𝐴𝑛)) ↔ ((𝑥 ∈ ℝ ∧ (𝐹𝑥) = 𝑘) ∧ 𝑥 ∈ (𝐴𝑛))))
248243, 247syl5bb 272 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑥 ∈ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ↔ ((𝑥 ∈ ℝ ∧ (𝐹𝑥) = 𝑘) ∧ 𝑥 ∈ (𝐴𝑛))))
249236, 242, 2483bitr4d 300 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑥 ∈ (𝐺 “ {𝑘}) ↔ 𝑥 ∈ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
250249alrimiv 1852 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑥(𝑥 ∈ (𝐺 “ {𝑘}) ↔ 𝑥 ∈ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
251 nfmpt1 4707 . . . . . . . . . . . . . . 15 𝑥(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴𝑛), (𝐹𝑥), 0))
252191, 251nfcxfr 2759 . . . . . . . . . . . . . 14 𝑥𝐺
253252nfcnv 5261 . . . . . . . . . . . . 13 𝑥𝐺
254 nfcv 2761 . . . . . . . . . . . . 13 𝑥{𝑘}
255253, 254nfima 5433 . . . . . . . . . . . 12 𝑥(𝐺 “ {𝑘})
256 nfcv 2761 . . . . . . . . . . . 12 𝑥((𝐹 “ {𝑘}) ∩ (𝐴𝑛))
257255, 256cleqf 2786 . . . . . . . . . . 11 ((𝐺 “ {𝑘}) = ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)) ↔ ∀𝑥(𝑥 ∈ (𝐺 “ {𝑘}) ↔ 𝑥 ∈ ((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
258250, 257sylibr 224 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝐺 “ {𝑘}) = ((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))
259258fveq2d 6152 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(𝐺 “ {𝑘})) = (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))
260259oveq2d 6620 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑘 · (vol‘(𝐺 “ {𝑘}))) = (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))
261260sumeq2dv 14367 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(𝐺 “ {𝑘}))) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))
262211, 261eqtrd 2655 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (∫1𝐺) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))
263262mpteq2dva 4704 . . . . 5 (𝜑 → (𝑛 ∈ ℕ ↦ (∫1𝐺)) = (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))))
264263fveq1d 6150 . . . 4 (𝜑 → ((𝑛 ∈ ℕ ↦ (∫1𝐺))‘𝑗) = ((𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗))
265174sumeq2sdv 14368 . . . . . 6 (𝑛 = 𝑗 → Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗)))))
266 eqid 2621 . . . . . 6 (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛))))) = (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))
267 sumex 14352 . . . . . 6 Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗)))) ∈ V
268265, 266, 267fvmpt 6239 . . . . 5 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗)))))
269177sumeq2sdv 14368 . . . . 5 (𝑗 ∈ ℕ → Σ𝑘 ∈ (ran 𝐹 ∖ {0})((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑗)))))
270268, 269eqtr4d 2658 . . . 4 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗))
271264, 270sylan9eq 2675 . . 3 ((𝜑𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (∫1𝐺))‘𝑗) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((𝐹 “ {𝑘}) ∩ (𝐴𝑛)))))‘𝑗))
2721, 2, 8, 181, 183, 189, 271climfsum 14479 . 2 (𝜑 → (𝑛 ∈ ℕ ↦ (∫1𝐺)) ⇝ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(𝐹 “ {𝑘}))))
273 itg1val 23356 . . 3 (𝐹 ∈ dom ∫1 → (∫1𝐹) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(𝐹 “ {𝑘}))))
2743, 273syl 17 . 2 (𝜑 → (∫1𝐹) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(𝐹 “ {𝑘}))))
275272, 274breqtrrd 4641 1 (𝜑 → (𝑛 ∈ ℕ ↦ (∫1𝐺)) ⇝ (∫1𝐹))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384  ∀wal 1478   = wceq 1480   ∈ wcel 1987   ≠ wne 2790  ∀wral 2907  ∃wrex 2908  Vcvv 3186   ∖ cdif 3552   ∩ cin 3554   ⊆ wss 3555  ∅c0 3891  ifcif 4058  {csn 4148  ∪ cuni 4402  ∪ ciun 4485   class class class wbr 4613   ↦ cmpt 4673  ◡ccnv 5073  dom cdm 5074  ran crn 5075   “ cima 5077   ∘ ccom 5078   Fn wfn 5842  ⟶wf 5843  ‘cfv 5847  (class class class)co 6604  Fincfn 7899  supcsup 8290  ℂcc 9878  ℝcr 9879  0cc0 9880  1c1 9881   + caddc 9883   · cmul 9885  +∞cpnf 10015  ℝ*cxr 10017   < clt 10018   ≤ cle 10019  ℕcn 10964  [,]cicc 12120   ⇝ cli 14149  Σcsu 14350  vol*covol 23138  volcvol 23139  ∫1citg1 23290 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-inf2 8482  ax-cc 9201  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957  ax-pre-sup 9958  ax-addf 9959 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-disj 4584  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-se 5034  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-isom 5856  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-of 6850  df-om 7013  df-1st 7113  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-2o 7506  df-oadd 7509  df-er 7687  df-map 7804  df-pm 7805  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-fi 8261  df-sup 8292  df-inf 8293  df-oi 8359  df-card 8709  df-cda 8934  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-div 10629  df-nn 10965  df-2 11023  df-3 11024  df-n0 11237  df-z 11322  df-uz 11632  df-q 11733  df-rp 11777  df-xneg 11890  df-xadd 11891  df-xmul 11892  df-ioo 12121  df-ico 12123  df-icc 12124  df-fz 12269  df-fzo 12407  df-fl 12533  df-seq 12742  df-exp 12801  df-hash 13058  df-cj 13773  df-re 13774  df-im 13775  df-sqrt 13909  df-abs 13910  df-clim 14153  df-rlim 14154  df-sum 14351  df-rest 16004  df-topgen 16025  df-psmet 19657  df-xmet 19658  df-met 19659  df-bl 19660  df-mopn 19661  df-top 20621  df-bases 20622  df-topon 20623  df-cmp 21100  df-ovol 23140  df-vol 23141  df-mbf 23294  df-itg1 23295 This theorem is referenced by:  itg2monolem1  23423
 Copyright terms: Public domain W3C validator