This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem itg1climres

Description: Restricting the simple function F to the increasing sequence A ( n ) of measurable sets whose union is RR yields a sequence of simple functions whose integrals approach the integral of F . (Contributed by Mario Carneiro, 15-Aug-2014)

Ref Expression
Hypotheses itg1climres.1 ⊢ ( 𝜑 → 𝐴 : ℕ ⟶ dom vol )
itg1climres.2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ‘ 𝑛 ) ⊆ ( 𝐴 ‘ ( 𝑛 + 1 ) ) )
itg1climres.3 ⊢ ( 𝜑 → ∪ ran 𝐴 = ℝ )
itg1climres.4 ⊢ ( 𝜑 → 𝐹 ∈ dom ∫1 )
itg1climres.5 ⊢ 𝐺 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
Assertion itg1climres ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ 𝐺 ) ) ⇝ ( ∫1 ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 itg1climres.1 ⊢ ( 𝜑 → 𝐴 : ℕ ⟶ dom vol )
2 itg1climres.2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ‘ 𝑛 ) ⊆ ( 𝐴 ‘ ( 𝑛 + 1 ) ) )
3 itg1climres.3 ⊢ ( 𝜑 → ∪ ran 𝐴 = ℝ )
4 itg1climres.4 ⊢ ( 𝜑 → 𝐹 ∈ dom ∫1 )
5 itg1climres.5 ⊢ 𝐺 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
6 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
7 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
8 i1frn ⊢ ( 𝐹 ∈ dom ∫1 → ran 𝐹 ∈ Fin )
9 4 8 syl ⊢ ( 𝜑 → ran 𝐹 ∈ Fin )
10 difss ⊢ ( ran 𝐹 ∖ { 0 } ) ⊆ ran 𝐹
11 ssfi ⊢ ( ( ran 𝐹 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ ran 𝐹 ) → ( ran 𝐹 ∖ { 0 } ) ∈ Fin )
12 9 10 11 sylancl ⊢ ( 𝜑 → ( ran 𝐹 ∖ { 0 } ) ∈ Fin )
13 1zzd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 1 ∈ ℤ )
14 i1fima ⊢ ( 𝐹 ∈ dom ∫1 → ( ◡ 𝐹 “ { 𝑘 } ) ∈ dom vol )
15 4 14 syl ⊢ ( 𝜑 → ( ◡ 𝐹 “ { 𝑘 } ) ∈ dom vol )
16 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑛 ∈ ℕ ) → ( ◡ 𝐹 “ { 𝑘 } ) ∈ dom vol )
17 1 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ‘ 𝑛 ) ∈ dom vol )
18 17 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ‘ 𝑛 ) ∈ dom vol )
19 inmbl ⊢ ( ( ( ◡ 𝐹 “ { 𝑘 } ) ∈ dom vol ∧ ( 𝐴 ‘ 𝑛 ) ∈ dom vol ) → ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ∈ dom vol )
20 16 18 19 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ∈ dom vol )
21 mblvol ⊢ ( ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ∈ dom vol → ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) = ( vol* ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) )
22 20 21 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) = ( vol* ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) )
23 inss1 ⊢ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ⊆ ( ◡ 𝐹 “ { 𝑘 } )
24 23 a1i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ⊆ ( ◡ 𝐹 “ { 𝑘 } ) )
25 mblss ⊢ ( ( ◡ 𝐹 “ { 𝑘 } ) ∈ dom vol → ( ◡ 𝐹 “ { 𝑘 } ) ⊆ ℝ )
26 16 25 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑛 ∈ ℕ ) → ( ◡ 𝐹 “ { 𝑘 } ) ⊆ ℝ )
27 mblvol ⊢ ( ( ◡ 𝐹 “ { 𝑘 } ) ∈ dom vol → ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) = ( vol* ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) )
28 16 27 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) = ( vol* ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) )
29 i1fima2sn ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ∈ ℝ )
30 4 29 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ∈ ℝ )
31 30 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ∈ ℝ )
32 28 31 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑛 ∈ ℕ ) → ( vol* ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ∈ ℝ )
33 ovolsscl ⊢ ( ( ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ⊆ ( ◡ 𝐹 “ { 𝑘 } ) ∧ ( ◡ 𝐹 “ { 𝑘 } ) ⊆ ℝ ∧ ( vol* ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ∈ ℝ ) → ( vol* ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ∈ ℝ )
34 24 26 32 33 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑛 ∈ ℕ ) → ( vol* ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ∈ ℝ )
35 22 34 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ∈ ℝ )
36 35 fmpttd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) : ℕ ⟶ ℝ )
37 2 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ‘ 𝑛 ) ⊆ ( 𝐴 ‘ ( 𝑛 + 1 ) ) )
38 sslin ⊢ ( ( 𝐴 ‘ 𝑛 ) ⊆ ( 𝐴 ‘ ( 𝑛 + 1 ) ) → ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ⊆ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) )
39 37 38 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ⊆ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) )
40 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 𝐴 : ℕ ⟶ dom vol )
41 peano2nn ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 + 1 ) ∈ ℕ )
42 ffvelcdm ⊢ ( ( 𝐴 : ℕ ⟶ dom vol ∧ ( 𝑛 + 1 ) ∈ ℕ ) → ( 𝐴 ‘ ( 𝑛 + 1 ) ) ∈ dom vol )
43 40 41 42 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ‘ ( 𝑛 + 1 ) ) ∈ dom vol )
44 inmbl ⊢ ( ( ( ◡ 𝐹 “ { 𝑘 } ) ∈ dom vol ∧ ( 𝐴 ‘ ( 𝑛 + 1 ) ) ∈ dom vol ) → ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) ∈ dom vol )
45 16 43 44 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) ∈ dom vol )
46 mblss ⊢ ( ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) ∈ dom vol → ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) ⊆ ℝ )
47 45 46 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) ⊆ ℝ )
48 ovolss ⊢ ( ( ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ⊆ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) ∧ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) ⊆ ℝ ) → ( vol* ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ≤ ( vol* ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) ) )
49 39 47 48 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑛 ∈ ℕ ) → ( vol* ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ≤ ( vol* ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) ) )
50 mblvol ⊢ ( ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) ∈ dom vol → ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) ) = ( vol* ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) ) )
51 45 50 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) ) = ( vol* ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) ) )
52 49 22 51 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ≤ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) ) )
53 52 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ∀ 𝑛 ∈ ℕ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ≤ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) ) )
54 fveq2 ⊢ ( 𝑛 = 𝑗 → ( 𝐴 ‘ 𝑛 ) = ( 𝐴 ‘ 𝑗 ) )
55 54 ineq2d ⊢ ( 𝑛 = 𝑗 → ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) = ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑗 ) ) )
56 55 fveq2d ⊢ ( 𝑛 = 𝑗 → ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) = ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑗 ) ) ) )
57 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) )
58 fvex ⊢ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑗 ) ) ) ∈ V
59 56 57 58 fvmpt ⊢ ( 𝑗 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) = ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑗 ) ) ) )
60 peano2nn ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 + 1 ) ∈ ℕ )
61 fveq2 ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( 𝐴 ‘ 𝑛 ) = ( 𝐴 ‘ ( 𝑗 + 1 ) ) )
62 61 ineq2d ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) = ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) )
63 62 fveq2d ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) = ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) ) )
64 fvex ⊢ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) ) ∈ V
65 63 57 64 fvmpt ⊢ ( ( 𝑗 + 1 ) ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ‘ ( 𝑗 + 1 ) ) = ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) ) )
66 60 65 syl ⊢ ( 𝑗 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ‘ ( 𝑗 + 1 ) ) = ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) ) )
67 59 66 breq12d ⊢ ( 𝑗 ∈ ℕ → ( ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) ≤ ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ‘ ( 𝑗 + 1 ) ) ↔ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑗 ) ) ) ≤ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) ) ) )
68 67 ralbiia ⊢ ( ∀ 𝑗 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) ≤ ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ‘ ( 𝑗 + 1 ) ) ↔ ∀ 𝑗 ∈ ℕ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑗 ) ) ) ≤ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) ) )
69 fvoveq1 ⊢ ( 𝑛 = 𝑗 → ( 𝐴 ‘ ( 𝑛 + 1 ) ) = ( 𝐴 ‘ ( 𝑗 + 1 ) ) )
70 69 ineq2d ⊢ ( 𝑛 = 𝑗 → ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) = ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) )
71 70 fveq2d ⊢ ( 𝑛 = 𝑗 → ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) ) = ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) ) )
72 56 71 breq12d ⊢ ( 𝑛 = 𝑗 → ( ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ≤ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) ) ↔ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑗 ) ) ) ≤ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) ) ) )
73 72 cbvralvw ⊢ ( ∀ 𝑛 ∈ ℕ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ≤ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) ) ↔ ∀ 𝑗 ∈ ℕ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑗 ) ) ) ≤ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) ) )
74 68 73 bitr4i ⊢ ( ∀ 𝑗 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) ≤ ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ‘ ( 𝑗 + 1 ) ) ↔ ∀ 𝑛 ∈ ℕ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ≤ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) ) )
75 53 74 sylibr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ∀ 𝑗 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) ≤ ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ‘ ( 𝑗 + 1 ) ) )
76 75 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) ≤ ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ‘ ( 𝑗 + 1 ) ) )
77 ovolss ⊢ ( ( ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ⊆ ( ◡ 𝐹 “ { 𝑘 } ) ∧ ( ◡ 𝐹 “ { 𝑘 } ) ⊆ ℝ ) → ( vol* ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ≤ ( vol* ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) )
78 23 26 77 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑛 ∈ ℕ ) → ( vol* ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ≤ ( vol* ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) )
79 78 22 28 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ≤ ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) )
80 79 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ∀ 𝑛 ∈ ℕ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ≤ ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) )
81 59 breq1d ⊢ ( 𝑗 ∈ ℕ → ( ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) ≤ ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ↔ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑗 ) ) ) ≤ ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ) )
82 81 ralbiia ⊢ ( ∀ 𝑗 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) ≤ ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ↔ ∀ 𝑗 ∈ ℕ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑗 ) ) ) ≤ ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) )
83 56 breq1d ⊢ ( 𝑛 = 𝑗 → ( ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ≤ ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ↔ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑗 ) ) ) ≤ ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ) )
84 83 cbvralvw ⊢ ( ∀ 𝑛 ∈ ℕ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ≤ ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ↔ ∀ 𝑗 ∈ ℕ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑗 ) ) ) ≤ ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) )
85 82 84 bitr4i ⊢ ( ∀ 𝑗 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) ≤ ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ↔ ∀ 𝑛 ∈ ℕ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ≤ ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) )
86 80 85 sylibr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ∀ 𝑗 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) ≤ ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) )
87 brralrspcev ⊢ ( ( ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ∈ ℝ ∧ ∀ 𝑗 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) ≤ ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) ≤ 𝑥 )
88 30 86 87 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) ≤ 𝑥 )
89 6 13 36 76 88 climsup ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ⇝ sup ( ran ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) , ℝ , < ) )
90 20 fmpttd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) : ℕ ⟶ dom vol )
91 39 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ∀ 𝑛 ∈ ℕ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ⊆ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) )
92 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) )
93 fvex ⊢ ( 𝐴 ‘ 𝑗 ) ∈ V
94 93 inex2 ⊢ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑗 ) ) ∈ V
95 55 92 94 fvmpt ⊢ ( 𝑗 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ‘ 𝑗 ) = ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑗 ) ) )
96 fvex ⊢ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ∈ V
97 96 inex2 ⊢ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) ∈ V
98 62 92 97 fvmpt ⊢ ( ( 𝑗 + 1 ) ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ‘ ( 𝑗 + 1 ) ) = ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) )
99 60 98 syl ⊢ ( 𝑗 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ‘ ( 𝑗 + 1 ) ) = ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) )
100 95 99 sseq12d ⊢ ( 𝑗 ∈ ℕ → ( ( ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ‘ 𝑗 ) ⊆ ( ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ‘ ( 𝑗 + 1 ) ) ↔ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑗 ) ) ⊆ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) ) )
101 100 ralbiia ⊢ ( ∀ 𝑗 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ‘ 𝑗 ) ⊆ ( ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ‘ ( 𝑗 + 1 ) ) ↔ ∀ 𝑗 ∈ ℕ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑗 ) ) ⊆ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) )
102 55 70 sseq12d ⊢ ( 𝑛 = 𝑗 → ( ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ⊆ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) ↔ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑗 ) ) ⊆ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) ) )
103 102 cbvralvw ⊢ ( ∀ 𝑛 ∈ ℕ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ⊆ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) ↔ ∀ 𝑗 ∈ ℕ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑗 ) ) ⊆ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) )
104 101 103 bitr4i ⊢ ( ∀ 𝑗 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ‘ 𝑗 ) ⊆ ( ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ‘ ( 𝑗 + 1 ) ) ↔ ∀ 𝑛 ∈ ℕ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ⊆ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) )
105 91 104 sylibr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ∀ 𝑗 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ‘ 𝑗 ) ⊆ ( ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ‘ ( 𝑗 + 1 ) ) )
106 volsup ⊢ ( ( ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) : ℕ ⟶ dom vol ∧ ∀ 𝑗 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ‘ 𝑗 ) ⊆ ( ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ‘ ( 𝑗 + 1 ) ) ) → ( vol ‘ ∪ ran ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) = sup ( ( vol “ ran ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) , ℝ* , < ) )
107 90 105 106 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol ‘ ∪ ran ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) = sup ( ( vol “ ran ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) , ℝ* , < ) )
108 95 iuneq2i ⊢ ∪ 𝑗 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ‘ 𝑗 ) = ∪ 𝑗 ∈ ℕ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑗 ) )
109 55 cbviunv ⊢ ∪ 𝑛 ∈ ℕ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) = ∪ 𝑗 ∈ ℕ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑗 ) )
110 iunin2 ⊢ ∪ 𝑛 ∈ ℕ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) = ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) )
111 108 109 110 3eqtr2i ⊢ ∪ 𝑗 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ‘ 𝑗 ) = ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) )
112 ffn ⊢ ( 𝐴 : ℕ ⟶ dom vol → 𝐴 Fn ℕ )
113 fniunfv ⊢ ( 𝐴 Fn ℕ → ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) = ∪ ran 𝐴 )
114 1 112 113 3syl ⊢ ( 𝜑 → ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) = ∪ ran 𝐴 )
115 114 3 eqtrd ⊢ ( 𝜑 → ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) = ℝ )
116 115 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) = ℝ )
117 116 ineq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) = ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ℝ ) )
118 15 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ◡ 𝐹 “ { 𝑘 } ) ∈ dom vol )
119 118 25 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ◡ 𝐹 “ { 𝑘 } ) ⊆ ℝ )
120 dfss2 ⊢ ( ( ◡ 𝐹 “ { 𝑘 } ) ⊆ ℝ ↔ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ℝ ) = ( ◡ 𝐹 “ { 𝑘 } ) )
121 119 120 sylib ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ℝ ) = ( ◡ 𝐹 “ { 𝑘 } ) )
122 117 121 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) = ( ◡ 𝐹 “ { 𝑘 } ) )
123 111 122 eqtrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ∪ 𝑗 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ‘ 𝑗 ) = ( ◡ 𝐹 “ { 𝑘 } ) )
124 ffn ⊢ ( ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) : ℕ ⟶ dom vol → ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) Fn ℕ )
125 fniunfv ⊢ ( ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) Fn ℕ → ∪ 𝑗 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ‘ 𝑗 ) = ∪ ran ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) )
126 90 124 125 3syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ∪ 𝑗 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ‘ 𝑗 ) = ∪ ran ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) )
127 123 126 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ◡ 𝐹 “ { 𝑘 } ) = ∪ ran ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) )
128 127 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) = ( vol ‘ ∪ ran ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) )
129 36 frnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ran ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ⊆ ℝ )
130 36 fdmd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → dom ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) = ℕ )
131 1nn ⊢ 1 ∈ ℕ
132 ne0i ⊢ ( 1 ∈ ℕ → ℕ ≠ ∅ )
133 131 132 mp1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ℕ ≠ ∅ )
134 130 133 eqnetrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → dom ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ≠ ∅ )
135 dm0rn0 ⊢ ( dom ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) = ∅ ↔ ran ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) = ∅ )
136 135 necon3bii ⊢ ( dom ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ≠ ∅ ↔ ran ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ≠ ∅ )
137 134 136 sylib ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ran ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ≠ ∅ )
138 ffn ⊢ ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) : ℕ ⟶ ℝ → ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) Fn ℕ )
139 breq1 ⊢ ( 𝑧 = ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) → ( 𝑧 ≤ 𝑥 ↔ ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) ≤ 𝑥 ) )
140 139 ralrn ⊢ ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) Fn ℕ → ( ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) 𝑧 ≤ 𝑥 ↔ ∀ 𝑗 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) ≤ 𝑥 ) )
141 36 138 140 3syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) 𝑧 ≤ 𝑥 ↔ ∀ 𝑗 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) ≤ 𝑥 ) )
142 141 rexbidv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) 𝑧 ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) ≤ 𝑥 ) )
143 88 142 mpbird ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) 𝑧 ≤ 𝑥 )
144 supxrre ⊢ ( ( ran ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ⊆ ℝ ∧ ran ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) 𝑧 ≤ 𝑥 ) → sup ( ran ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) , ℝ* , < ) = sup ( ran ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) , ℝ , < ) )
145 129 137 143 144 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → sup ( ran ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) , ℝ* , < ) = sup ( ran ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) , ℝ , < ) )
146 volf ⊢ vol : dom vol ⟶ ( 0 [,] +∞ )
147 146 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → vol : dom vol ⟶ ( 0 [,] +∞ ) )
148 147 20 cofmpt ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol ∘ ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) )
149 148 rneqd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ran ( vol ∘ ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) = ran ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) )
150 rnco2 ⊢ ran ( vol ∘ ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) = ( vol “ ran ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) )
151 149 150 eqtr3di ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ran ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) = ( vol “ ran ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) )
152 151 supeq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → sup ( ran ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) , ℝ* , < ) = sup ( ( vol “ ran ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) , ℝ* , < ) )
153 145 152 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → sup ( ran ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) , ℝ , < ) = sup ( ( vol “ ran ( 𝑛 ∈ ℕ ↦ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) , ℝ* , < ) )
154 107 128 153 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) = sup ( ran ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) , ℝ , < ) )
155 89 154 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ⇝ ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) )
156 i1ff ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℝ )
157 frn ⊢ ( 𝐹 : ℝ ⟶ ℝ → ran 𝐹 ⊆ ℝ )
158 4 156 157 3syl ⊢ ( 𝜑 → ran 𝐹 ⊆ ℝ )
159 158 ssdifssd ⊢ ( 𝜑 → ( ran 𝐹 ∖ { 0 } ) ⊆ ℝ )
160 159 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 𝑘 ∈ ℝ )
161 160 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 𝑘 ∈ ℂ )
162 nnex ⊢ ℕ ∈ V
163 162 mptex ⊢ ( 𝑛 ∈ ℕ ↦ ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ) ∈ V
164 163 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝑛 ∈ ℕ ↦ ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ) ∈ V )
165 36 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) ∈ ℝ )
166 165 recnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) ∈ ℂ )
167 56 oveq2d ⊢ ( 𝑛 = 𝑗 → ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) = ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑗 ) ) ) ) )
168 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) )
169 ovex ⊢ ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑗 ) ) ) ) ∈ V
170 167 168 169 fvmpt ⊢ ( 𝑗 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ) ‘ 𝑗 ) = ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑗 ) ) ) ) )
171 59 oveq2d ⊢ ( 𝑗 ∈ ℕ → ( 𝑘 · ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) ) = ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑗 ) ) ) ) )
172 170 171 eqtr4d ⊢ ( 𝑗 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ) ‘ 𝑗 ) = ( 𝑘 · ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) ) )
173 172 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ) ‘ 𝑗 ) = ( 𝑘 · ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) ) )
174 6 13 155 161 164 166 173 climmulc2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝑛 ∈ ℕ ↦ ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ) ⇝ ( 𝑘 · ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ) )
175 162 mptex ⊢ ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ 𝐺 ) ) ∈ V
176 175 a1i ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ 𝐺 ) ) ∈ V )
177 160 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑛 ∈ ℕ ) → 𝑘 ∈ ℝ )
178 177 35 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ∈ ℝ )
179 178 fmpttd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝑛 ∈ ℕ ↦ ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ) : ℕ ⟶ ℝ )
180 179 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ) ‘ 𝑗 ) ∈ ℝ )
181 180 recnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ) ‘ 𝑗 ) ∈ ℂ )
182 181 anasss ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ∧ 𝑗 ∈ ℕ ) ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ) ‘ 𝑗 ) ∈ ℂ )
183 4 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐹 ∈ dom ∫1 )
184 5 i1fres ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ‘ 𝑛 ) ∈ dom vol ) → 𝐺 ∈ dom ∫1 )
185 183 17 184 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐺 ∈ dom ∫1 )
186 12 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ran 𝐹 ∖ { 0 } ) ∈ Fin )
187 ffn ⊢ ( 𝐹 : ℝ ⟶ ℝ → 𝐹 Fn ℝ )
188 4 156 187 3syl ⊢ ( 𝜑 → 𝐹 Fn ℝ )
189 188 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐹 Fn ℝ )
190 fnfvelrn ⊢ ( ( 𝐹 Fn ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 )
191 189 190 sylan ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 )
192 i1f0rn ⊢ ( 𝐹 ∈ dom ∫1 → 0 ∈ ran 𝐹 )
193 4 192 syl ⊢ ( 𝜑 → 0 ∈ ran 𝐹 )
194 193 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 0 ∈ ran 𝐹 )
195 191 194 ifcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ran 𝐹 )
196 195 5 fmptd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐺 : ℝ ⟶ ran 𝐹 )
197 frn ⊢ ( 𝐺 : ℝ ⟶ ran 𝐹 → ran 𝐺 ⊆ ran 𝐹 )
198 ssdif ⊢ ( ran 𝐺 ⊆ ran 𝐹 → ( ran 𝐺 ∖ { 0 } ) ⊆ ( ran 𝐹 ∖ { 0 } ) )
199 196 197 198 3syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ran 𝐺 ∖ { 0 } ) ⊆ ( ran 𝐹 ∖ { 0 } ) )
200 158 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ran 𝐹 ⊆ ℝ )
201 200 ssdifd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ran 𝐹 ∖ { 0 } ) ⊆ ( ℝ ∖ { 0 } ) )
202 itg1val2 ⊢ ( ( 𝐺 ∈ dom ∫1 ∧ ( ( ran 𝐹 ∖ { 0 } ) ∈ Fin ∧ ( ran 𝐺 ∖ { 0 } ) ⊆ ( ran 𝐹 ∖ { 0 } ) ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ ( ℝ ∖ { 0 } ) ) ) → ( ∫1 ‘ 𝐺 ) = Σ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑘 · ( vol ‘ ( ◡ 𝐺 “ { 𝑘 } ) ) ) )
203 185 186 199 201 202 syl13anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∫1 ‘ 𝐺 ) = Σ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑘 · ( vol ‘ ( ◡ 𝐺 “ { 𝑘 } ) ) ) )
204 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
205 c0ex ⊢ 0 ∈ V
206 204 205 ifex ⊢ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ V
207 5 fvmpt2 ⊢ ( ( 𝑥 ∈ ℝ ∧ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ V ) → ( 𝐺 ‘ 𝑥 ) = if ( 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
208 206 207 mpan2 ⊢ ( 𝑥 ∈ ℝ → ( 𝐺 ‘ 𝑥 ) = if ( 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
209 208 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝐺 ‘ 𝑥 ) = if ( 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
210 209 eqeq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐺 ‘ 𝑥 ) = 𝑘 ↔ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) = 𝑘 ) )
211 eldifsni ⊢ ( 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) → 𝑘 ≠ 0 )
212 211 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → 𝑘 ≠ 0 )
213 neeq1 ⊢ ( if ( 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) = 𝑘 → ( if ( 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≠ 0 ↔ 𝑘 ≠ 0 ) )
214 212 213 syl5ibrcom ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( if ( 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) = 𝑘 → if ( 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≠ 0 ) )
215 iffalse ⊢ ( ¬ 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) → if ( 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) = 0 )
216 215 necon1ai ⊢ ( if ( 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≠ 0 → 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) )
217 214 216 syl6 ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( if ( 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) = 𝑘 → 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) ) )
218 217 pm4.71rd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( if ( 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) = 𝑘 ↔ ( 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) ∧ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) = 𝑘 ) ) )
219 210 218 bitrd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐺 ‘ 𝑥 ) = 𝑘 ↔ ( 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) ∧ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) = 𝑘 ) ) )
220 iftrue ⊢ ( 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) → if ( 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) = ( 𝐹 ‘ 𝑥 ) )
221 220 eqeq1d ⊢ ( 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) → ( if ( 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) = 𝑘 ↔ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) )
222 221 pm5.32i ⊢ ( ( 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) ∧ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) = 𝑘 ) ↔ ( 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) )
223 222 biancomi ⊢ ( ( 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) ∧ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) = 𝑘 ) ↔ ( ( 𝐹 ‘ 𝑥 ) = 𝑘 ∧ 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) ) )
224 219 223 bitrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐺 ‘ 𝑥 ) = 𝑘 ↔ ( ( 𝐹 ‘ 𝑥 ) = 𝑘 ∧ 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) ) ) )
225 224 pm5.32da ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ( 𝑥 ∈ ℝ ∧ ( 𝐺 ‘ 𝑥 ) = 𝑘 ) ↔ ( 𝑥 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑘 ∧ 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) ) ) ) )
226 anass ⊢ ( ( ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ∧ 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑘 ∧ 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) ) ) )
227 225 226 bitr4di ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ( 𝑥 ∈ ℝ ∧ ( 𝐺 ‘ 𝑥 ) = 𝑘 ) ↔ ( ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ∧ 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) ) ) )
228 i1ff ⊢ ( 𝐺 ∈ dom ∫1 → 𝐺 : ℝ ⟶ ℝ )
229 ffn ⊢ ( 𝐺 : ℝ ⟶ ℝ → 𝐺 Fn ℝ )
230 185 228 229 3syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐺 Fn ℝ )
231 230 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 𝐺 Fn ℝ )
232 fniniseg ⊢ ( 𝐺 Fn ℝ → ( 𝑥 ∈ ( ◡ 𝐺 “ { 𝑘 } ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐺 ‘ 𝑥 ) = 𝑘 ) ) )
233 231 232 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝑥 ∈ ( ◡ 𝐺 “ { 𝑘 } ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐺 ‘ 𝑥 ) = 𝑘 ) ) )
234 elin ⊢ ( 𝑥 ∈ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ↔ ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑘 } ) ∧ 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) ) )
235 189 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 𝐹 Fn ℝ )
236 fniniseg ⊢ ( 𝐹 Fn ℝ → ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑘 } ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ) )
237 235 236 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑘 } ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ) )
238 237 anbi1d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑘 } ) ∧ 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) ) ↔ ( ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ∧ 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) ) ) )
239 234 238 bitrid ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝑥 ∈ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ↔ ( ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ∧ 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) ) ) )
240 227 233 239 3bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝑥 ∈ ( ◡ 𝐺 “ { 𝑘 } ) ↔ 𝑥 ∈ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) )
241 240 alrimiv ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ∀ 𝑥 ( 𝑥 ∈ ( ◡ 𝐺 “ { 𝑘 } ) ↔ 𝑥 ∈ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) )
242 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑛 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
243 5 242 nfcxfr ⊢ Ⅎ 𝑥 𝐺
244 243 nfcnv ⊢ Ⅎ 𝑥 ◡ 𝐺
245 nfcv ⊢ Ⅎ 𝑥 { 𝑘 }
246 244 245 nfima ⊢ Ⅎ 𝑥 ( ◡ 𝐺 “ { 𝑘 } )
247 nfcv ⊢ Ⅎ 𝑥 ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) )
248 246 247 cleqf ⊢ ( ( ◡ 𝐺 “ { 𝑘 } ) = ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ ( ◡ 𝐺 “ { 𝑘 } ) ↔ 𝑥 ∈ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) )
249 241 248 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ◡ 𝐺 “ { 𝑘 } ) = ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) )
250 249 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐺 “ { 𝑘 } ) ) = ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) )
251 250 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝑘 · ( vol ‘ ( ◡ 𝐺 “ { 𝑘 } ) ) ) = ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) )
252 251 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑘 · ( vol ‘ ( ◡ 𝐺 “ { 𝑘 } ) ) ) = Σ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) )
253 203 252 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∫1 ‘ 𝐺 ) = Σ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) )
254 253 mpteq2dva ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ 𝐺 ) ) = ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ) )
255 254 fveq1d ⊢ ( 𝜑 → ( ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ 𝐺 ) ) ‘ 𝑗 ) = ( ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ) ‘ 𝑗 ) )
256 167 sumeq2sdv ⊢ ( 𝑛 = 𝑗 → Σ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) = Σ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑗 ) ) ) ) )
257 eqid ⊢ ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ) = ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) )
258 sumex ⊢ Σ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑗 ) ) ) ) ∈ V
259 256 257 258 fvmpt ⊢ ( 𝑗 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ) ‘ 𝑗 ) = Σ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑗 ) ) ) ) )
260 170 sumeq2sdv ⊢ ( 𝑗 ∈ ℕ → Σ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ( ( 𝑛 ∈ ℕ ↦ ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ) ‘ 𝑗 ) = Σ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑗 ) ) ) ) )
261 259 260 eqtr4d ⊢ ( 𝑗 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ) ‘ 𝑗 ) = Σ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ( ( 𝑛 ∈ ℕ ↦ ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ) ‘ 𝑗 ) )
262 255 261 sylan9eq ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ 𝐺 ) ) ‘ 𝑗 ) = Σ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ( ( 𝑛 ∈ ℕ ↦ ( 𝑘 · ( vol ‘ ( ( ◡ 𝐹 “ { 𝑘 } ) ∩ ( 𝐴 ‘ 𝑛 ) ) ) ) ) ‘ 𝑗 ) )
263 6 7 12 174 176 182 262 climfsum ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ 𝐺 ) ) ⇝ Σ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑘 · ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ) )
264 itg1val ⊢ ( 𝐹 ∈ dom ∫1 → ( ∫1 ‘ 𝐹 ) = Σ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑘 · ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ) )
265 4 264 syl ⊢ ( 𝜑 → ( ∫1 ‘ 𝐹 ) = Σ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑘 · ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ) )
266 263 265 breqtrrd ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ 𝐺 ) ) ⇝ ( ∫1 ‘ 𝐹 ) )