Metamath Proof Explorer


Theorem itg2i1fseq

Description: Subject to the conditions coming from mbfi1fseq , the integral of the sequence of simple functions converges to the integral of the target function. (Contributed by Mario Carneiro, 17-Aug-2014)

Ref Expression
Hypotheses itg2i1fseq.1 ( 𝜑𝐹 ∈ MblFn )
itg2i1fseq.2 ( 𝜑𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
itg2i1fseq.3 ( 𝜑𝑃 : ℕ ⟶ dom ∫1 )
itg2i1fseq.4 ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 0𝑝r ≤ ( 𝑃𝑛 ) ∧ ( 𝑃𝑛 ) ∘r ≤ ( 𝑃 ‘ ( 𝑛 + 1 ) ) ) )
itg2i1fseq.5 ( 𝜑 → ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹𝑥 ) )
itg2i1fseq.6 𝑆 = ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑃𝑚 ) ) )
Assertion itg2i1fseq ( 𝜑 → ( ∫2𝐹 ) = sup ( ran 𝑆 , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 itg2i1fseq.1 ( 𝜑𝐹 ∈ MblFn )
2 itg2i1fseq.2 ( 𝜑𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
3 itg2i1fseq.3 ( 𝜑𝑃 : ℕ ⟶ dom ∫1 )
4 itg2i1fseq.4 ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 0𝑝r ≤ ( 𝑃𝑛 ) ∧ ( 𝑃𝑛 ) ∘r ≤ ( 𝑃 ‘ ( 𝑛 + 1 ) ) ) )
5 itg2i1fseq.5 ( 𝜑 → ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹𝑥 ) )
6 itg2i1fseq.6 𝑆 = ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑃𝑚 ) ) )
7 fveq2 ( 𝑛 = 𝑚 → ( 𝑃𝑛 ) = ( 𝑃𝑚 ) )
8 7 fveq1d ( 𝑛 = 𝑚 → ( ( 𝑃𝑛 ) ‘ 𝑥 ) = ( ( 𝑃𝑚 ) ‘ 𝑥 ) )
9 8 cbvmptv ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ ℕ ↦ ( ( 𝑃𝑚 ) ‘ 𝑥 ) )
10 fveq2 ( 𝑥 = 𝑦 → ( ( 𝑃𝑚 ) ‘ 𝑥 ) = ( ( 𝑃𝑚 ) ‘ 𝑦 ) )
11 10 mpteq2dv ( 𝑥 = 𝑦 → ( 𝑚 ∈ ℕ ↦ ( ( 𝑃𝑚 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ ℕ ↦ ( ( 𝑃𝑚 ) ‘ 𝑦 ) ) )
12 9 11 syl5eq ( 𝑥 = 𝑦 → ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ ℕ ↦ ( ( 𝑃𝑚 ) ‘ 𝑦 ) ) )
13 12 rneqd ( 𝑥 = 𝑦 → ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑥 ) ) = ran ( 𝑚 ∈ ℕ ↦ ( ( 𝑃𝑚 ) ‘ 𝑦 ) ) )
14 13 supeq1d ( 𝑥 = 𝑦 → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) = sup ( ran ( 𝑚 ∈ ℕ ↦ ( ( 𝑃𝑚 ) ‘ 𝑦 ) ) , ℝ , < ) )
15 14 cbvmptv ( 𝑥 ∈ ℝ ↦ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ) = ( 𝑦 ∈ ℝ ↦ sup ( ran ( 𝑚 ∈ ℕ ↦ ( ( 𝑃𝑚 ) ‘ 𝑦 ) ) , ℝ , < ) )
16 3 ffvelrnda ( ( 𝜑𝑚 ∈ ℕ ) → ( 𝑃𝑚 ) ∈ dom ∫1 )
17 i1fmbf ( ( 𝑃𝑚 ) ∈ dom ∫1 → ( 𝑃𝑚 ) ∈ MblFn )
18 16 17 syl ( ( 𝜑𝑚 ∈ ℕ ) → ( 𝑃𝑚 ) ∈ MblFn )
19 i1ff ( ( 𝑃𝑚 ) ∈ dom ∫1 → ( 𝑃𝑚 ) : ℝ ⟶ ℝ )
20 16 19 syl ( ( 𝜑𝑚 ∈ ℕ ) → ( 𝑃𝑚 ) : ℝ ⟶ ℝ )
21 7 breq2d ( 𝑛 = 𝑚 → ( 0𝑝r ≤ ( 𝑃𝑛 ) ↔ 0𝑝r ≤ ( 𝑃𝑚 ) ) )
22 fvoveq1 ( 𝑛 = 𝑚 → ( 𝑃 ‘ ( 𝑛 + 1 ) ) = ( 𝑃 ‘ ( 𝑚 + 1 ) ) )
23 7 22 breq12d ( 𝑛 = 𝑚 → ( ( 𝑃𝑛 ) ∘r ≤ ( 𝑃 ‘ ( 𝑛 + 1 ) ) ↔ ( 𝑃𝑚 ) ∘r ≤ ( 𝑃 ‘ ( 𝑚 + 1 ) ) ) )
24 21 23 anbi12d ( 𝑛 = 𝑚 → ( ( 0𝑝r ≤ ( 𝑃𝑛 ) ∧ ( 𝑃𝑛 ) ∘r ≤ ( 𝑃 ‘ ( 𝑛 + 1 ) ) ) ↔ ( 0𝑝r ≤ ( 𝑃𝑚 ) ∧ ( 𝑃𝑚 ) ∘r ≤ ( 𝑃 ‘ ( 𝑚 + 1 ) ) ) ) )
25 24 rspccva ( ( ∀ 𝑛 ∈ ℕ ( 0𝑝r ≤ ( 𝑃𝑛 ) ∧ ( 𝑃𝑛 ) ∘r ≤ ( 𝑃 ‘ ( 𝑛 + 1 ) ) ) ∧ 𝑚 ∈ ℕ ) → ( 0𝑝r ≤ ( 𝑃𝑚 ) ∧ ( 𝑃𝑚 ) ∘r ≤ ( 𝑃 ‘ ( 𝑚 + 1 ) ) ) )
26 4 25 sylan ( ( 𝜑𝑚 ∈ ℕ ) → ( 0𝑝r ≤ ( 𝑃𝑚 ) ∧ ( 𝑃𝑚 ) ∘r ≤ ( 𝑃 ‘ ( 𝑚 + 1 ) ) ) )
27 26 simpld ( ( 𝜑𝑚 ∈ ℕ ) → 0𝑝r ≤ ( 𝑃𝑚 ) )
28 0plef ( ( 𝑃𝑚 ) : ℝ ⟶ ( 0 [,) +∞ ) ↔ ( ( 𝑃𝑚 ) : ℝ ⟶ ℝ ∧ 0𝑝r ≤ ( 𝑃𝑚 ) ) )
29 20 27 28 sylanbrc ( ( 𝜑𝑚 ∈ ℕ ) → ( 𝑃𝑚 ) : ℝ ⟶ ( 0 [,) +∞ ) )
30 26 simprd ( ( 𝜑𝑚 ∈ ℕ ) → ( 𝑃𝑚 ) ∘r ≤ ( 𝑃 ‘ ( 𝑚 + 1 ) ) )
31 rge0ssre ( 0 [,) +∞ ) ⊆ ℝ
32 2 ffvelrnda ( ( 𝜑𝑦 ∈ ℝ ) → ( 𝐹𝑦 ) ∈ ( 0 [,) +∞ ) )
33 31 32 sselid ( ( 𝜑𝑦 ∈ ℝ ) → ( 𝐹𝑦 ) ∈ ℝ )
34 1 2 3 4 5 itg2i1fseqle ( ( 𝜑𝑚 ∈ ℕ ) → ( 𝑃𝑚 ) ∘r𝐹 )
35 20 ffnd ( ( 𝜑𝑚 ∈ ℕ ) → ( 𝑃𝑚 ) Fn ℝ )
36 2 ffnd ( 𝜑𝐹 Fn ℝ )
37 36 adantr ( ( 𝜑𝑚 ∈ ℕ ) → 𝐹 Fn ℝ )
38 reex ℝ ∈ V
39 38 a1i ( ( 𝜑𝑚 ∈ ℕ ) → ℝ ∈ V )
40 inidm ( ℝ ∩ ℝ ) = ℝ
41 eqidd ( ( ( 𝜑𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑃𝑚 ) ‘ 𝑦 ) = ( ( 𝑃𝑚 ) ‘ 𝑦 ) )
42 eqidd ( ( ( 𝜑𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( 𝐹𝑦 ) = ( 𝐹𝑦 ) )
43 35 37 39 39 40 41 42 ofrfval ( ( 𝜑𝑚 ∈ ℕ ) → ( ( 𝑃𝑚 ) ∘r𝐹 ↔ ∀ 𝑦 ∈ ℝ ( ( 𝑃𝑚 ) ‘ 𝑦 ) ≤ ( 𝐹𝑦 ) ) )
44 34 43 mpbid ( ( 𝜑𝑚 ∈ ℕ ) → ∀ 𝑦 ∈ ℝ ( ( 𝑃𝑚 ) ‘ 𝑦 ) ≤ ( 𝐹𝑦 ) )
45 44 r19.21bi ( ( ( 𝜑𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑃𝑚 ) ‘ 𝑦 ) ≤ ( 𝐹𝑦 ) )
46 45 an32s ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑃𝑚 ) ‘ 𝑦 ) ≤ ( 𝐹𝑦 ) )
47 46 ralrimiva ( ( 𝜑𝑦 ∈ ℝ ) → ∀ 𝑚 ∈ ℕ ( ( 𝑃𝑚 ) ‘ 𝑦 ) ≤ ( 𝐹𝑦 ) )
48 brralrspcev ( ( ( 𝐹𝑦 ) ∈ ℝ ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑃𝑚 ) ‘ 𝑦 ) ≤ ( 𝐹𝑦 ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ ℕ ( ( 𝑃𝑚 ) ‘ 𝑦 ) ≤ 𝑧 )
49 33 47 48 syl2anc ( ( 𝜑𝑦 ∈ ℝ ) → ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ ℕ ( ( 𝑃𝑚 ) ‘ 𝑦 ) ≤ 𝑧 )
50 7 fveq2d ( 𝑛 = 𝑚 → ( ∫2 ‘ ( 𝑃𝑛 ) ) = ( ∫2 ‘ ( 𝑃𝑚 ) ) )
51 50 cbvmptv ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑃𝑛 ) ) ) = ( 𝑚 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑃𝑚 ) ) )
52 51 rneqi ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑃𝑛 ) ) ) = ran ( 𝑚 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑃𝑚 ) ) )
53 52 supeq1i sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑃𝑛 ) ) ) , ℝ* , < ) = sup ( ran ( 𝑚 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑃𝑚 ) ) ) , ℝ* , < )
54 15 18 29 30 49 53 itg2mono ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ) ) = sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑃𝑛 ) ) ) , ℝ* , < ) )
55 2 feqmptd ( 𝜑𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝐹𝑦 ) ) )
56 7 fveq1d ( 𝑛 = 𝑚 → ( ( 𝑃𝑛 ) ‘ 𝑦 ) = ( ( 𝑃𝑚 ) ‘ 𝑦 ) )
57 56 cbvmptv ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) = ( 𝑚 ∈ ℕ ↦ ( ( 𝑃𝑚 ) ‘ 𝑦 ) )
58 57 rneqi ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) = ran ( 𝑚 ∈ ℕ ↦ ( ( 𝑃𝑚 ) ‘ 𝑦 ) )
59 58 supeq1i sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) , ℝ , < ) = sup ( ran ( 𝑚 ∈ ℕ ↦ ( ( 𝑃𝑚 ) ‘ 𝑦 ) ) , ℝ , < )
60 nnuz ℕ = ( ℤ ‘ 1 )
61 1zzd ( ( 𝜑𝑦 ∈ ℝ ) → 1 ∈ ℤ )
62 20 ffvelrnda ( ( ( 𝜑𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑃𝑚 ) ‘ 𝑦 ) ∈ ℝ )
63 62 an32s ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑃𝑚 ) ‘ 𝑦 ) ∈ ℝ )
64 63 57 fmptd ( ( 𝜑𝑦 ∈ ℝ ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) : ℕ ⟶ ℝ )
65 peano2nn ( 𝑚 ∈ ℕ → ( 𝑚 + 1 ) ∈ ℕ )
66 ffvelrn ( ( 𝑃 : ℕ ⟶ dom ∫1 ∧ ( 𝑚 + 1 ) ∈ ℕ ) → ( 𝑃 ‘ ( 𝑚 + 1 ) ) ∈ dom ∫1 )
67 3 65 66 syl2an ( ( 𝜑𝑚 ∈ ℕ ) → ( 𝑃 ‘ ( 𝑚 + 1 ) ) ∈ dom ∫1 )
68 i1ff ( ( 𝑃 ‘ ( 𝑚 + 1 ) ) ∈ dom ∫1 → ( 𝑃 ‘ ( 𝑚 + 1 ) ) : ℝ ⟶ ℝ )
69 67 68 syl ( ( 𝜑𝑚 ∈ ℕ ) → ( 𝑃 ‘ ( 𝑚 + 1 ) ) : ℝ ⟶ ℝ )
70 69 ffnd ( ( 𝜑𝑚 ∈ ℕ ) → ( 𝑃 ‘ ( 𝑚 + 1 ) ) Fn ℝ )
71 eqidd ( ( ( 𝜑𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑃 ‘ ( 𝑚 + 1 ) ) ‘ 𝑦 ) = ( ( 𝑃 ‘ ( 𝑚 + 1 ) ) ‘ 𝑦 ) )
72 35 70 39 39 40 41 71 ofrfval ( ( 𝜑𝑚 ∈ ℕ ) → ( ( 𝑃𝑚 ) ∘r ≤ ( 𝑃 ‘ ( 𝑚 + 1 ) ) ↔ ∀ 𝑦 ∈ ℝ ( ( 𝑃𝑚 ) ‘ 𝑦 ) ≤ ( ( 𝑃 ‘ ( 𝑚 + 1 ) ) ‘ 𝑦 ) ) )
73 30 72 mpbid ( ( 𝜑𝑚 ∈ ℕ ) → ∀ 𝑦 ∈ ℝ ( ( 𝑃𝑚 ) ‘ 𝑦 ) ≤ ( ( 𝑃 ‘ ( 𝑚 + 1 ) ) ‘ 𝑦 ) )
74 73 r19.21bi ( ( ( 𝜑𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑃𝑚 ) ‘ 𝑦 ) ≤ ( ( 𝑃 ‘ ( 𝑚 + 1 ) ) ‘ 𝑦 ) )
75 74 an32s ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑃𝑚 ) ‘ 𝑦 ) ≤ ( ( 𝑃 ‘ ( 𝑚 + 1 ) ) ‘ 𝑦 ) )
76 eqid ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) )
77 fvex ( ( 𝑃𝑚 ) ‘ 𝑦 ) ∈ V
78 56 76 77 fvmpt ( 𝑚 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ‘ 𝑚 ) = ( ( 𝑃𝑚 ) ‘ 𝑦 ) )
79 78 adantl ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ‘ 𝑚 ) = ( ( 𝑃𝑚 ) ‘ 𝑦 ) )
80 fveq2 ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑃𝑛 ) = ( 𝑃 ‘ ( 𝑚 + 1 ) ) )
81 80 fveq1d ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝑃𝑛 ) ‘ 𝑦 ) = ( ( 𝑃 ‘ ( 𝑚 + 1 ) ) ‘ 𝑦 ) )
82 fvex ( ( 𝑃 ‘ ( 𝑚 + 1 ) ) ‘ 𝑦 ) ∈ V
83 81 76 82 fvmpt ( ( 𝑚 + 1 ) ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ‘ ( 𝑚 + 1 ) ) = ( ( 𝑃 ‘ ( 𝑚 + 1 ) ) ‘ 𝑦 ) )
84 65 83 syl ( 𝑚 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ‘ ( 𝑚 + 1 ) ) = ( ( 𝑃 ‘ ( 𝑚 + 1 ) ) ‘ 𝑦 ) )
85 84 adantl ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ‘ ( 𝑚 + 1 ) ) = ( ( 𝑃 ‘ ( 𝑚 + 1 ) ) ‘ 𝑦 ) )
86 75 79 85 3brtr4d ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ‘ 𝑚 ) ≤ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ‘ ( 𝑚 + 1 ) ) )
87 78 breq1d ( 𝑚 ∈ ℕ → ( ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ‘ 𝑚 ) ≤ 𝑧 ↔ ( ( 𝑃𝑚 ) ‘ 𝑦 ) ≤ 𝑧 ) )
88 87 ralbiia ( ∀ 𝑚 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ‘ 𝑚 ) ≤ 𝑧 ↔ ∀ 𝑚 ∈ ℕ ( ( 𝑃𝑚 ) ‘ 𝑦 ) ≤ 𝑧 )
89 88 rexbii ( ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ‘ 𝑚 ) ≤ 𝑧 ↔ ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ ℕ ( ( 𝑃𝑚 ) ‘ 𝑦 ) ≤ 𝑧 )
90 49 89 sylibr ( ( 𝜑𝑦 ∈ ℝ ) → ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ‘ 𝑚 ) ≤ 𝑧 )
91 60 61 64 86 90 climsup ( ( 𝜑𝑦 ∈ ℝ ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ⇝ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) , ℝ , < ) )
92 fveq2 ( 𝑥 = 𝑦 → ( ( 𝑃𝑛 ) ‘ 𝑥 ) = ( ( 𝑃𝑛 ) ‘ 𝑦 ) )
93 92 mpteq2dv ( 𝑥 = 𝑦 → ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑥 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) )
94 fveq2 ( 𝑥 = 𝑦 → ( 𝐹𝑥 ) = ( 𝐹𝑦 ) )
95 93 94 breq12d ( 𝑥 = 𝑦 → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹𝑥 ) ↔ ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ⇝ ( 𝐹𝑦 ) ) )
96 95 rspccva ( ( ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹𝑥 ) ∧ 𝑦 ∈ ℝ ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ⇝ ( 𝐹𝑦 ) )
97 5 96 sylan ( ( 𝜑𝑦 ∈ ℝ ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ⇝ ( 𝐹𝑦 ) )
98 climuni ( ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ⇝ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) , ℝ , < ) ∧ ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ⇝ ( 𝐹𝑦 ) ) → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) , ℝ , < ) = ( 𝐹𝑦 ) )
99 91 97 98 syl2anc ( ( 𝜑𝑦 ∈ ℝ ) → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) , ℝ , < ) = ( 𝐹𝑦 ) )
100 59 99 eqtr3id ( ( 𝜑𝑦 ∈ ℝ ) → sup ( ran ( 𝑚 ∈ ℕ ↦ ( ( 𝑃𝑚 ) ‘ 𝑦 ) ) , ℝ , < ) = ( 𝐹𝑦 ) )
101 100 mpteq2dva ( 𝜑 → ( 𝑦 ∈ ℝ ↦ sup ( ran ( 𝑚 ∈ ℕ ↦ ( ( 𝑃𝑚 ) ‘ 𝑦 ) ) , ℝ , < ) ) = ( 𝑦 ∈ ℝ ↦ ( 𝐹𝑦 ) ) )
102 55 101 eqtr4d ( 𝜑𝐹 = ( 𝑦 ∈ ℝ ↦ sup ( ran ( 𝑚 ∈ ℕ ↦ ( ( 𝑃𝑚 ) ‘ 𝑦 ) ) , ℝ , < ) ) )
103 102 15 eqtr4di ( 𝜑𝐹 = ( 𝑥 ∈ ℝ ↦ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ) )
104 103 fveq2d ( 𝜑 → ( ∫2𝐹 ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ) ) )
105 itg2itg1 ( ( ( 𝑃𝑚 ) ∈ dom ∫1 ∧ 0𝑝r ≤ ( 𝑃𝑚 ) ) → ( ∫2 ‘ ( 𝑃𝑚 ) ) = ( ∫1 ‘ ( 𝑃𝑚 ) ) )
106 16 27 105 syl2anc ( ( 𝜑𝑚 ∈ ℕ ) → ( ∫2 ‘ ( 𝑃𝑚 ) ) = ( ∫1 ‘ ( 𝑃𝑚 ) ) )
107 106 mpteq2dva ( 𝜑 → ( 𝑚 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑃𝑚 ) ) ) = ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑃𝑚 ) ) ) )
108 6 107 eqtr4id ( 𝜑𝑆 = ( 𝑚 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑃𝑚 ) ) ) )
109 108 51 eqtr4di ( 𝜑𝑆 = ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑃𝑛 ) ) ) )
110 109 rneqd ( 𝜑 → ran 𝑆 = ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑃𝑛 ) ) ) )
111 110 supeq1d ( 𝜑 → sup ( ran 𝑆 , ℝ* , < ) = sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑃𝑛 ) ) ) , ℝ* , < ) )
112 54 104 111 3eqtr4d ( 𝜑 → ( ∫2𝐹 ) = sup ( ran 𝑆 , ℝ* , < ) )