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 ffvelrnda ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝐴𝑛 ) ∈ 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 ffvelrn ( ( 𝐴 : ℕ ⟶ 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 df-ss ( ( 𝐹 “ { 𝑘 } ) ⊆ ℝ ↔ ( ( 𝐹 “ { 𝑘 } ) ∩ ℝ ) = ( 𝐹 “ { 𝑘 } ) )
121 119 120 sylib ( ( 𝜑𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ( 𝐹 “ { 𝑘 } ) ∩ ℝ ) = ( 𝐹 “ { 𝑘 } ) )
122 117 121 eqtrd ( ( 𝜑𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ( 𝐹 “ { 𝑘 } ) ∩ 𝑛 ∈ ℕ ( 𝐴𝑛 ) ) = ( 𝐹 “ { 𝑘 } ) )
123 111 122 syl5eq ( ( 𝜑𝑘 ∈ ( 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 ffvelrnda ( ( ( 𝜑𝑘 ∈ ( 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 ffvelrnda ( ( ( 𝜑𝑘 ∈ ( 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 syl5bb ( ( ( 𝜑𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 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𝐹 ) )