Metamath Proof Explorer

Theorem itg2mono

Description: The Monotone Convergence Theorem for nonnegative functions. If { ( Fn ) : n e. NN } is a monotone increasing sequence of positive, measurable, real-valued functions, and G is the pointwise limit of the sequence, then ( S.2G ) is the limit of the sequence { ( S.2( Fn ) ) : n e. NN } . (Contributed by Mario Carneiro, 16-Aug-2014)

Ref Expression
Hypotheses itg2mono.1 
|- G = ( x e. RR |-> sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) )
itg2mono.2 
|- ( ( ph /\ n e. NN ) -> ( F ` n ) e. MblFn )
itg2mono.3 
|- ( ( ph /\ n e. NN ) -> ( F ` n ) : RR --> ( 0 [,) +oo ) )
itg2mono.4 
|- ( ( ph /\ n e. NN ) -> ( F ` n ) oR <_ ( F ` ( n + 1 ) ) )
itg2mono.5 
|- ( ( ph /\ x e. RR ) -> E. y e. RR A. n e. NN ( ( F ` n ) ` x ) <_ y )
itg2mono.6 
|- S = sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < )
Assertion itg2mono 
|- ( ph -> ( S.2 ` G ) = S )

Proof

Step Hyp Ref Expression
1 itg2mono.1 
 |-  G = ( x e. RR |-> sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) )
2 itg2mono.2 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) e. MblFn )
3 itg2mono.3 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) : RR --> ( 0 [,) +oo ) )
4 itg2mono.4 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) oR <_ ( F ` ( n + 1 ) ) )
5 itg2mono.5 
 |-  ( ( ph /\ x e. RR ) -> E. y e. RR A. n e. NN ( ( F ` n ) ` x ) <_ y )
6 itg2mono.6 
 |-  S = sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < )
7 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
8 fss 
 |-  ( ( ( F ` n ) : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ RR ) -> ( F ` n ) : RR --> RR )
9 3 7 8 sylancl 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) : RR --> RR )
10 9 ffvelrnda 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( F ` n ) ` x ) e. RR )
11 10 an32s 
 |-  ( ( ( ph /\ x e. RR ) /\ n e. NN ) -> ( ( F ` n ) ` x ) e. RR )
12 11 fmpttd 
 |-  ( ( ph /\ x e. RR ) -> ( n e. NN |-> ( ( F ` n ) ` x ) ) : NN --> RR )
13 12 frnd 
 |-  ( ( ph /\ x e. RR ) -> ran ( n e. NN |-> ( ( F ` n ) ` x ) ) C_ RR )
14 1nn 
 |-  1 e. NN
15 eqid 
 |-  ( n e. NN |-> ( ( F ` n ) ` x ) ) = ( n e. NN |-> ( ( F ` n ) ` x ) )
16 15 11 dmmptd 
 |-  ( ( ph /\ x e. RR ) -> dom ( n e. NN |-> ( ( F ` n ) ` x ) ) = NN )
17 14 16 eleqtrrid 
 |-  ( ( ph /\ x e. RR ) -> 1 e. dom ( n e. NN |-> ( ( F ` n ) ` x ) ) )
18 17 ne0d 
 |-  ( ( ph /\ x e. RR ) -> dom ( n e. NN |-> ( ( F ` n ) ` x ) ) =/= (/) )
19 dm0rn0 
 |-  ( dom ( n e. NN |-> ( ( F ` n ) ` x ) ) = (/) <-> ran ( n e. NN |-> ( ( F ` n ) ` x ) ) = (/) )
20 19 necon3bii 
 |-  ( dom ( n e. NN |-> ( ( F ` n ) ` x ) ) =/= (/) <-> ran ( n e. NN |-> ( ( F ` n ) ` x ) ) =/= (/) )
21 18 20 sylib 
 |-  ( ( ph /\ x e. RR ) -> ran ( n e. NN |-> ( ( F ` n ) ` x ) ) =/= (/) )
22 12 ffnd 
 |-  ( ( ph /\ x e. RR ) -> ( n e. NN |-> ( ( F ` n ) ` x ) ) Fn NN )
23 breq1 
 |-  ( z = ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` m ) -> ( z <_ y <-> ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` m ) <_ y ) )
24 23 ralrn 
 |-  ( ( n e. NN |-> ( ( F ` n ) ` x ) ) Fn NN -> ( A. z e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) z <_ y <-> A. m e. NN ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` m ) <_ y ) )
25 22 24 syl 
 |-  ( ( ph /\ x e. RR ) -> ( A. z e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) z <_ y <-> A. m e. NN ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` m ) <_ y ) )
26 fveq2 
 |-  ( n = m -> ( F ` n ) = ( F ` m ) )
27 26 fveq1d 
 |-  ( n = m -> ( ( F ` n ) ` x ) = ( ( F ` m ) ` x ) )
28 fvex 
 |-  ( ( F ` m ) ` x ) e. _V
29 27 15 28 fvmpt 
 |-  ( m e. NN -> ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` m ) = ( ( F ` m ) ` x ) )
30 29 breq1d 
 |-  ( m e. NN -> ( ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` m ) <_ y <-> ( ( F ` m ) ` x ) <_ y ) )
31 30 ralbiia 
 |-  ( A. m e. NN ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` m ) <_ y <-> A. m e. NN ( ( F ` m ) ` x ) <_ y )
32 27 breq1d 
 |-  ( n = m -> ( ( ( F ` n ) ` x ) <_ y <-> ( ( F ` m ) ` x ) <_ y ) )
33 32 cbvralvw 
 |-  ( A. n e. NN ( ( F ` n ) ` x ) <_ y <-> A. m e. NN ( ( F ` m ) ` x ) <_ y )
34 31 33 bitr4i 
 |-  ( A. m e. NN ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` m ) <_ y <-> A. n e. NN ( ( F ` n ) ` x ) <_ y )
35 25 34 bitrdi 
 |-  ( ( ph /\ x e. RR ) -> ( A. z e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) z <_ y <-> A. n e. NN ( ( F ` n ) ` x ) <_ y ) )
36 35 rexbidv 
 |-  ( ( ph /\ x e. RR ) -> ( E. y e. RR A. z e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) z <_ y <-> E. y e. RR A. n e. NN ( ( F ` n ) ` x ) <_ y ) )
37 5 36 mpbird 
 |-  ( ( ph /\ x e. RR ) -> E. y e. RR A. z e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) z <_ y )
38 13 21 37 suprcld 
 |-  ( ( ph /\ x e. RR ) -> sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) e. RR )
39 38 rexrd 
 |-  ( ( ph /\ x e. RR ) -> sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) e. RR* )
40 0red 
 |-  ( ( ph /\ x e. RR ) -> 0 e. RR )
41 fveq2 
 |-  ( n = 1 -> ( F ` n ) = ( F ` 1 ) )
42 41 feq1d 
 |-  ( n = 1 -> ( ( F ` n ) : RR --> ( 0 [,) +oo ) <-> ( F ` 1 ) : RR --> ( 0 [,) +oo ) ) )
43 3 ralrimiva 
 |-  ( ph -> A. n e. NN ( F ` n ) : RR --> ( 0 [,) +oo ) )
44 14 a1i 
 |-  ( ph -> 1 e. NN )
45 42 43 44 rspcdva 
 |-  ( ph -> ( F ` 1 ) : RR --> ( 0 [,) +oo ) )
46 45 ffvelrnda 
 |-  ( ( ph /\ x e. RR ) -> ( ( F ` 1 ) ` x ) e. ( 0 [,) +oo ) )
47 elrege0 
 |-  ( ( ( F ` 1 ) ` x ) e. ( 0 [,) +oo ) <-> ( ( ( F ` 1 ) ` x ) e. RR /\ 0 <_ ( ( F ` 1 ) ` x ) ) )
48 46 47 sylib 
 |-  ( ( ph /\ x e. RR ) -> ( ( ( F ` 1 ) ` x ) e. RR /\ 0 <_ ( ( F ` 1 ) ` x ) ) )
49 48 simpld 
 |-  ( ( ph /\ x e. RR ) -> ( ( F ` 1 ) ` x ) e. RR )
50 48 simprd 
 |-  ( ( ph /\ x e. RR ) -> 0 <_ ( ( F ` 1 ) ` x ) )
51 41 fveq1d 
 |-  ( n = 1 -> ( ( F ` n ) ` x ) = ( ( F ` 1 ) ` x ) )
52 fvex 
 |-  ( ( F ` 1 ) ` x ) e. _V
53 51 15 52 fvmpt 
 |-  ( 1 e. NN -> ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` 1 ) = ( ( F ` 1 ) ` x ) )
54 14 53 ax-mp 
 |-  ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` 1 ) = ( ( F ` 1 ) ` x )
55 fnfvelrn 
 |-  ( ( ( n e. NN |-> ( ( F ` n ) ` x ) ) Fn NN /\ 1 e. NN ) -> ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` 1 ) e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) )
56 22 14 55 sylancl 
 |-  ( ( ph /\ x e. RR ) -> ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` 1 ) e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) )
57 54 56 eqeltrrid 
 |-  ( ( ph /\ x e. RR ) -> ( ( F ` 1 ) ` x ) e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) )
58 13 21 37 57 suprubd 
 |-  ( ( ph /\ x e. RR ) -> ( ( F ` 1 ) ` x ) <_ sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) )
59 40 49 38 50 58 letrd 
 |-  ( ( ph /\ x e. RR ) -> 0 <_ sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) )
60 elxrge0 
 |-  ( sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) e. ( 0 [,] +oo ) <-> ( sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) e. RR* /\ 0 <_ sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) ) )
61 39 59 60 sylanbrc 
 |-  ( ( ph /\ x e. RR ) -> sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) e. ( 0 [,] +oo ) )
62 61 1 fmptd 
 |-  ( ph -> G : RR --> ( 0 [,] +oo ) )
63 itg2cl 
 |-  ( G : RR --> ( 0 [,] +oo ) -> ( S.2 ` G ) e. RR* )
64 62 63 syl 
 |-  ( ph -> ( S.2 ` G ) e. RR* )
65 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
66 fss 
 |-  ( ( ( F ` n ) : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ ( 0 [,] +oo ) ) -> ( F ` n ) : RR --> ( 0 [,] +oo ) )
67 3 65 66 sylancl 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) : RR --> ( 0 [,] +oo ) )
68 itg2cl 
 |-  ( ( F ` n ) : RR --> ( 0 [,] +oo ) -> ( S.2 ` ( F ` n ) ) e. RR* )
69 67 68 syl 
 |-  ( ( ph /\ n e. NN ) -> ( S.2 ` ( F ` n ) ) e. RR* )
70 69 fmpttd 
 |-  ( ph -> ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) : NN --> RR* )
71 70 frnd 
 |-  ( ph -> ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) C_ RR* )
72 supxrcl 
 |-  ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) C_ RR* -> sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < ) e. RR* )
73 71 72 syl 
 |-  ( ph -> sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < ) e. RR* )
74 6 73 eqeltrid 
 |-  ( ph -> S e. RR* )
75 2 adantlr 
 |-  ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ G ) /\ -. ( S.1 ` f ) <_ S ) ) /\ n e. NN ) -> ( F ` n ) e. MblFn )
76 3 adantlr 
 |-  ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ G ) /\ -. ( S.1 ` f ) <_ S ) ) /\ n e. NN ) -> ( F ` n ) : RR --> ( 0 [,) +oo ) )
77 4 adantlr 
 |-  ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ G ) /\ -. ( S.1 ` f ) <_ S ) ) /\ n e. NN ) -> ( F ` n ) oR <_ ( F ` ( n + 1 ) ) )
78 5 adantlr 
 |-  ( ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ G ) /\ -. ( S.1 ` f ) <_ S ) ) /\ x e. RR ) -> E. y e. RR A. n e. NN ( ( F ` n ) ` x ) <_ y )
79 simprll 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ G ) /\ -. ( S.1 ` f ) <_ S ) ) -> f e. dom S.1 )
80 simprlr 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ G ) /\ -. ( S.1 ` f ) <_ S ) ) -> f oR <_ G )
81 simprr 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ G ) /\ -. ( S.1 ` f ) <_ S ) ) -> -. ( S.1 ` f ) <_ S )
82 1 75 76 77 78 6 79 80 81 itg2monolem3 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ f oR <_ G ) /\ -. ( S.1 ` f ) <_ S ) ) -> ( S.1 ` f ) <_ S )
83 82 expr 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ G ) ) -> ( -. ( S.1 ` f ) <_ S -> ( S.1 ` f ) <_ S ) )
84 83 pm2.18d 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ G ) ) -> ( S.1 ` f ) <_ S )
85 84 expr 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( f oR <_ G -> ( S.1 ` f ) <_ S ) )
86 85 ralrimiva 
 |-  ( ph -> A. f e. dom S.1 ( f oR <_ G -> ( S.1 ` f ) <_ S ) )
87 itg2leub 
 |-  ( ( G : RR --> ( 0 [,] +oo ) /\ S e. RR* ) -> ( ( S.2 ` G ) <_ S <-> A. f e. dom S.1 ( f oR <_ G -> ( S.1 ` f ) <_ S ) ) )
88 62 74 87 syl2anc 
 |-  ( ph -> ( ( S.2 ` G ) <_ S <-> A. f e. dom S.1 ( f oR <_ G -> ( S.1 ` f ) <_ S ) ) )
89 86 88 mpbird 
 |-  ( ph -> ( S.2 ` G ) <_ S )
90 26 feq1d 
 |-  ( n = m -> ( ( F ` n ) : RR --> ( 0 [,) +oo ) <-> ( F ` m ) : RR --> ( 0 [,) +oo ) ) )
91 90 cbvralvw 
 |-  ( A. n e. NN ( F ` n ) : RR --> ( 0 [,) +oo ) <-> A. m e. NN ( F ` m ) : RR --> ( 0 [,) +oo ) )
92 43 91 sylib 
 |-  ( ph -> A. m e. NN ( F ` m ) : RR --> ( 0 [,) +oo ) )
93 92 r19.21bi 
 |-  ( ( ph /\ m e. NN ) -> ( F ` m ) : RR --> ( 0 [,) +oo ) )
94 fss 
 |-  ( ( ( F ` m ) : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ ( 0 [,] +oo ) ) -> ( F ` m ) : RR --> ( 0 [,] +oo ) )
95 93 65 94 sylancl 
 |-  ( ( ph /\ m e. NN ) -> ( F ` m ) : RR --> ( 0 [,] +oo ) )
96 62 adantr 
 |-  ( ( ph /\ m e. NN ) -> G : RR --> ( 0 [,] +oo ) )
97 13 21 37 3jca 
 |-  ( ( ph /\ x e. RR ) -> ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) C_ RR /\ ran ( n e. NN |-> ( ( F ` n ) ` x ) ) =/= (/) /\ E. y e. RR A. z e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) z <_ y ) )
98 97 adantlr 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. RR ) -> ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) C_ RR /\ ran ( n e. NN |-> ( ( F ` n ) ` x ) ) =/= (/) /\ E. y e. RR A. z e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) z <_ y ) )
99 29 ad2antlr 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. RR ) -> ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` m ) = ( ( F ` m ) ` x ) )
100 22 adantlr 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. RR ) -> ( n e. NN |-> ( ( F ` n ) ` x ) ) Fn NN )
101 simplr 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. RR ) -> m e. NN )
102 fnfvelrn 
 |-  ( ( ( n e. NN |-> ( ( F ` n ) ` x ) ) Fn NN /\ m e. NN ) -> ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` m ) e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) )
103 100 101 102 syl2anc 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. RR ) -> ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` m ) e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) )
104 99 103 eqeltrrd 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. RR ) -> ( ( F ` m ) ` x ) e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) )
105 suprub 
 |-  ( ( ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) C_ RR /\ ran ( n e. NN |-> ( ( F ` n ) ` x ) ) =/= (/) /\ E. y e. RR A. z e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) z <_ y ) /\ ( ( F ` m ) ` x ) e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) ) -> ( ( F ` m ) ` x ) <_ sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) )
106 98 104 105 syl2anc 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. RR ) -> ( ( F ` m ) ` x ) <_ sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) )
107 simpr 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. RR ) -> x e. RR )
108 ltso 
 |-  < Or RR
109 108 supex 
 |-  sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) e. _V
110 1 fvmpt2 
 |-  ( ( x e. RR /\ sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) e. _V ) -> ( G ` x ) = sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) )
111 107 109 110 sylancl 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. RR ) -> ( G ` x ) = sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) )
112 106 111 breqtrrd 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. RR ) -> ( ( F ` m ) ` x ) <_ ( G ` x ) )
113 112 ralrimiva 
 |-  ( ( ph /\ m e. NN ) -> A. x e. RR ( ( F ` m ) ` x ) <_ ( G ` x ) )
114 fveq2 
 |-  ( x = z -> ( ( F ` m ) ` x ) = ( ( F ` m ) ` z ) )
115 fveq2 
 |-  ( x = z -> ( G ` x ) = ( G ` z ) )
116 114 115 breq12d 
 |-  ( x = z -> ( ( ( F ` m ) ` x ) <_ ( G ` x ) <-> ( ( F ` m ) ` z ) <_ ( G ` z ) ) )
117 116 cbvralvw 
 |-  ( A. x e. RR ( ( F ` m ) ` x ) <_ ( G ` x ) <-> A. z e. RR ( ( F ` m ) ` z ) <_ ( G ` z ) )
118 113 117 sylib 
 |-  ( ( ph /\ m e. NN ) -> A. z e. RR ( ( F ` m ) ` z ) <_ ( G ` z ) )
119 93 ffnd 
 |-  ( ( ph /\ m e. NN ) -> ( F ` m ) Fn RR )
120 38 1 fmptd 
 |-  ( ph -> G : RR --> RR )
121 120 ffnd 
 |-  ( ph -> G Fn RR )
122 121 adantr 
 |-  ( ( ph /\ m e. NN ) -> G Fn RR )
123 reex 
 |-  RR e. _V
124 123 a1i 
 |-  ( ( ph /\ m e. NN ) -> RR e. _V )
125 inidm 
 |-  ( RR i^i RR ) = RR
126 eqidd 
 |-  ( ( ( ph /\ m e. NN ) /\ z e. RR ) -> ( ( F ` m ) ` z ) = ( ( F ` m ) ` z ) )
127 eqidd 
 |-  ( ( ( ph /\ m e. NN ) /\ z e. RR ) -> ( G ` z ) = ( G ` z ) )
128 119 122 124 124 125 126 127 ofrfval 
 |-  ( ( ph /\ m e. NN ) -> ( ( F ` m ) oR <_ G <-> A. z e. RR ( ( F ` m ) ` z ) <_ ( G ` z ) ) )
129 118 128 mpbird 
 |-  ( ( ph /\ m e. NN ) -> ( F ` m ) oR <_ G )
130 itg2le 
 |-  ( ( ( F ` m ) : RR --> ( 0 [,] +oo ) /\ G : RR --> ( 0 [,] +oo ) /\ ( F ` m ) oR <_ G ) -> ( S.2 ` ( F ` m ) ) <_ ( S.2 ` G ) )
131 95 96 129 130 syl3anc 
 |-  ( ( ph /\ m e. NN ) -> ( S.2 ` ( F ` m ) ) <_ ( S.2 ` G ) )
132 131 ralrimiva 
 |-  ( ph -> A. m e. NN ( S.2 ` ( F ` m ) ) <_ ( S.2 ` G ) )
133 70 ffnd 
 |-  ( ph -> ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) Fn NN )
134 breq1 
 |-  ( z = ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` m ) -> ( z <_ ( S.2 ` G ) <-> ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` m ) <_ ( S.2 ` G ) ) )
135 134 ralrn 
 |-  ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) Fn NN -> ( A. z e. ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) z <_ ( S.2 ` G ) <-> A. m e. NN ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` m ) <_ ( S.2 ` G ) ) )
136 133 135 syl 
 |-  ( ph -> ( A. z e. ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) z <_ ( S.2 ` G ) <-> A. m e. NN ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` m ) <_ ( S.2 ` G ) ) )
137 2fveq3 
 |-  ( n = m -> ( S.2 ` ( F ` n ) ) = ( S.2 ` ( F ` m ) ) )
138 eqid 
 |-  ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) = ( n e. NN |-> ( S.2 ` ( F ` n ) ) )
139 fvex 
 |-  ( S.2 ` ( F ` m ) ) e. _V
140 137 138 139 fvmpt 
 |-  ( m e. NN -> ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` m ) = ( S.2 ` ( F ` m ) ) )
141 140 breq1d 
 |-  ( m e. NN -> ( ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` m ) <_ ( S.2 ` G ) <-> ( S.2 ` ( F ` m ) ) <_ ( S.2 ` G ) ) )
142 141 ralbiia 
 |-  ( A. m e. NN ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` m ) <_ ( S.2 ` G ) <-> A. m e. NN ( S.2 ` ( F ` m ) ) <_ ( S.2 ` G ) )
143 136 142 bitrdi 
 |-  ( ph -> ( A. z e. ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) z <_ ( S.2 ` G ) <-> A. m e. NN ( S.2 ` ( F ` m ) ) <_ ( S.2 ` G ) ) )
144 132 143 mpbird 
 |-  ( ph -> A. z e. ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) z <_ ( S.2 ` G ) )
145 supxrleub 
 |-  ( ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) C_ RR* /\ ( S.2 ` G ) e. RR* ) -> ( sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < ) <_ ( S.2 ` G ) <-> A. z e. ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) z <_ ( S.2 ` G ) ) )
146 71 64 145 syl2anc 
 |-  ( ph -> ( sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < ) <_ ( S.2 ` G ) <-> A. z e. ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) z <_ ( S.2 ` G ) ) )
147 144 146 mpbird 
 |-  ( ph -> sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < ) <_ ( S.2 ` G ) )
148 6 147 eqbrtrid 
 |-  ( ph -> S <_ ( S.2 ` G ) )
149 64 74 89 148 xrletrid 
 |-  ( ph -> ( S.2 ` G ) = S )