Metamath Proof Explorer


Theorem mbflimsup

Description: The limit supremum of a sequence of measurable real-valued functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by AV, 12-Sep-2020)

Ref Expression
Hypotheses mbflimsup.1
|- Z = ( ZZ>= ` M )
mbflimsup.2
|- G = ( x e. A |-> ( limsup ` ( n e. Z |-> B ) ) )
mbflimsup.h
|- H = ( m e. RR |-> sup ( ( ( ( n e. Z |-> B ) " ( m [,) +oo ) ) i^i RR* ) , RR* , < ) )
mbflimsup.3
|- ( ph -> M e. ZZ )
mbflimsup.4
|- ( ( ph /\ x e. A ) -> ( limsup ` ( n e. Z |-> B ) ) e. RR )
mbflimsup.5
|- ( ( ph /\ n e. Z ) -> ( x e. A |-> B ) e. MblFn )
mbflimsup.6
|- ( ( ph /\ ( n e. Z /\ x e. A ) ) -> B e. RR )
Assertion mbflimsup
|- ( ph -> G e. MblFn )

Proof

Step Hyp Ref Expression
1 mbflimsup.1
 |-  Z = ( ZZ>= ` M )
2 mbflimsup.2
 |-  G = ( x e. A |-> ( limsup ` ( n e. Z |-> B ) ) )
3 mbflimsup.h
 |-  H = ( m e. RR |-> sup ( ( ( ( n e. Z |-> B ) " ( m [,) +oo ) ) i^i RR* ) , RR* , < ) )
4 mbflimsup.3
 |-  ( ph -> M e. ZZ )
5 mbflimsup.4
 |-  ( ( ph /\ x e. A ) -> ( limsup ` ( n e. Z |-> B ) ) e. RR )
6 mbflimsup.5
 |-  ( ( ph /\ n e. Z ) -> ( x e. A |-> B ) e. MblFn )
7 mbflimsup.6
 |-  ( ( ph /\ ( n e. Z /\ x e. A ) ) -> B e. RR )
8 1 fvexi
 |-  Z e. _V
9 8 mptex
 |-  ( n e. Z |-> B ) e. _V
10 9 a1i
 |-  ( ( ph /\ x e. A ) -> ( n e. Z |-> B ) e. _V )
11 uzssz
 |-  ( ZZ>= ` M ) C_ ZZ
12 1 11 eqsstri
 |-  Z C_ ZZ
13 zssre
 |-  ZZ C_ RR
14 12 13 sstri
 |-  Z C_ RR
15 14 a1i
 |-  ( ( ph /\ x e. A ) -> Z C_ RR )
16 1 uzsup
 |-  ( M e. ZZ -> sup ( Z , RR* , < ) = +oo )
17 4 16 syl
 |-  ( ph -> sup ( Z , RR* , < ) = +oo )
18 17 adantr
 |-  ( ( ph /\ x e. A ) -> sup ( Z , RR* , < ) = +oo )
19 3 10 15 18 limsupval2
 |-  ( ( ph /\ x e. A ) -> ( limsup ` ( n e. Z |-> B ) ) = inf ( ( H " Z ) , RR* , < ) )
20 imassrn
 |-  ( H " Z ) C_ ran H
21 4 adantr
 |-  ( ( ph /\ x e. A ) -> M e. ZZ )
22 7 anass1rs
 |-  ( ( ( ph /\ x e. A ) /\ n e. Z ) -> B e. RR )
23 22 fmpttd
 |-  ( ( ph /\ x e. A ) -> ( n e. Z |-> B ) : Z --> RR )
24 5 ltpnfd
 |-  ( ( ph /\ x e. A ) -> ( limsup ` ( n e. Z |-> B ) ) < +oo )
25 3 1 limsupgre
 |-  ( ( M e. ZZ /\ ( n e. Z |-> B ) : Z --> RR /\ ( limsup ` ( n e. Z |-> B ) ) < +oo ) -> H : RR --> RR )
26 21 23 24 25 syl3anc
 |-  ( ( ph /\ x e. A ) -> H : RR --> RR )
27 26 frnd
 |-  ( ( ph /\ x e. A ) -> ran H C_ RR )
28 20 27 sstrid
 |-  ( ( ph /\ x e. A ) -> ( H " Z ) C_ RR )
29 26 fdmd
 |-  ( ( ph /\ x e. A ) -> dom H = RR )
30 29 ineq1d
 |-  ( ( ph /\ x e. A ) -> ( dom H i^i Z ) = ( RR i^i Z ) )
31 sseqin2
 |-  ( Z C_ RR <-> ( RR i^i Z ) = Z )
32 14 31 mpbi
 |-  ( RR i^i Z ) = Z
33 30 32 eqtrdi
 |-  ( ( ph /\ x e. A ) -> ( dom H i^i Z ) = Z )
34 uzid
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
35 4 34 syl
 |-  ( ph -> M e. ( ZZ>= ` M ) )
36 35 1 eleqtrrdi
 |-  ( ph -> M e. Z )
37 36 adantr
 |-  ( ( ph /\ x e. A ) -> M e. Z )
38 37 ne0d
 |-  ( ( ph /\ x e. A ) -> Z =/= (/) )
39 33 38 eqnetrd
 |-  ( ( ph /\ x e. A ) -> ( dom H i^i Z ) =/= (/) )
40 imadisj
 |-  ( ( H " Z ) = (/) <-> ( dom H i^i Z ) = (/) )
41 40 necon3bii
 |-  ( ( H " Z ) =/= (/) <-> ( dom H i^i Z ) =/= (/) )
42 39 41 sylibr
 |-  ( ( ph /\ x e. A ) -> ( H " Z ) =/= (/) )
43 5 leidd
 |-  ( ( ph /\ x e. A ) -> ( limsup ` ( n e. Z |-> B ) ) <_ ( limsup ` ( n e. Z |-> B ) ) )
44 22 rexrd
 |-  ( ( ( ph /\ x e. A ) /\ n e. Z ) -> B e. RR* )
45 44 fmpttd
 |-  ( ( ph /\ x e. A ) -> ( n e. Z |-> B ) : Z --> RR* )
46 5 rexrd
 |-  ( ( ph /\ x e. A ) -> ( limsup ` ( n e. Z |-> B ) ) e. RR* )
47 3 limsuple
 |-  ( ( Z C_ RR /\ ( n e. Z |-> B ) : Z --> RR* /\ ( limsup ` ( n e. Z |-> B ) ) e. RR* ) -> ( ( limsup ` ( n e. Z |-> B ) ) <_ ( limsup ` ( n e. Z |-> B ) ) <-> A. y e. RR ( limsup ` ( n e. Z |-> B ) ) <_ ( H ` y ) ) )
48 15 45 46 47 syl3anc
 |-  ( ( ph /\ x e. A ) -> ( ( limsup ` ( n e. Z |-> B ) ) <_ ( limsup ` ( n e. Z |-> B ) ) <-> A. y e. RR ( limsup ` ( n e. Z |-> B ) ) <_ ( H ` y ) ) )
49 43 48 mpbid
 |-  ( ( ph /\ x e. A ) -> A. y e. RR ( limsup ` ( n e. Z |-> B ) ) <_ ( H ` y ) )
50 ssralv
 |-  ( Z C_ RR -> ( A. y e. RR ( limsup ` ( n e. Z |-> B ) ) <_ ( H ` y ) -> A. y e. Z ( limsup ` ( n e. Z |-> B ) ) <_ ( H ` y ) ) )
51 14 49 50 mpsyl
 |-  ( ( ph /\ x e. A ) -> A. y e. Z ( limsup ` ( n e. Z |-> B ) ) <_ ( H ` y ) )
52 3 limsupgf
 |-  H : RR --> RR*
53 ffn
 |-  ( H : RR --> RR* -> H Fn RR )
54 52 53 ax-mp
 |-  H Fn RR
55 breq2
 |-  ( z = ( H ` y ) -> ( ( limsup ` ( n e. Z |-> B ) ) <_ z <-> ( limsup ` ( n e. Z |-> B ) ) <_ ( H ` y ) ) )
56 55 ralima
 |-  ( ( H Fn RR /\ Z C_ RR ) -> ( A. z e. ( H " Z ) ( limsup ` ( n e. Z |-> B ) ) <_ z <-> A. y e. Z ( limsup ` ( n e. Z |-> B ) ) <_ ( H ` y ) ) )
57 54 15 56 sylancr
 |-  ( ( ph /\ x e. A ) -> ( A. z e. ( H " Z ) ( limsup ` ( n e. Z |-> B ) ) <_ z <-> A. y e. Z ( limsup ` ( n e. Z |-> B ) ) <_ ( H ` y ) ) )
58 51 57 mpbird
 |-  ( ( ph /\ x e. A ) -> A. z e. ( H " Z ) ( limsup ` ( n e. Z |-> B ) ) <_ z )
59 breq1
 |-  ( y = ( limsup ` ( n e. Z |-> B ) ) -> ( y <_ z <-> ( limsup ` ( n e. Z |-> B ) ) <_ z ) )
60 59 ralbidv
 |-  ( y = ( limsup ` ( n e. Z |-> B ) ) -> ( A. z e. ( H " Z ) y <_ z <-> A. z e. ( H " Z ) ( limsup ` ( n e. Z |-> B ) ) <_ z ) )
61 60 rspcev
 |-  ( ( ( limsup ` ( n e. Z |-> B ) ) e. RR /\ A. z e. ( H " Z ) ( limsup ` ( n e. Z |-> B ) ) <_ z ) -> E. y e. RR A. z e. ( H " Z ) y <_ z )
62 5 58 61 syl2anc
 |-  ( ( ph /\ x e. A ) -> E. y e. RR A. z e. ( H " Z ) y <_ z )
63 infxrre
 |-  ( ( ( H " Z ) C_ RR /\ ( H " Z ) =/= (/) /\ E. y e. RR A. z e. ( H " Z ) y <_ z ) -> inf ( ( H " Z ) , RR* , < ) = inf ( ( H " Z ) , RR , < ) )
64 28 42 62 63 syl3anc
 |-  ( ( ph /\ x e. A ) -> inf ( ( H " Z ) , RR* , < ) = inf ( ( H " Z ) , RR , < ) )
65 df-ima
 |-  ( H " Z ) = ran ( H |` Z )
66 26 feqmptd
 |-  ( ( ph /\ x e. A ) -> H = ( i e. RR |-> ( H ` i ) ) )
67 66 reseq1d
 |-  ( ( ph /\ x e. A ) -> ( H |` Z ) = ( ( i e. RR |-> ( H ` i ) ) |` Z ) )
68 resmpt
 |-  ( Z C_ RR -> ( ( i e. RR |-> ( H ` i ) ) |` Z ) = ( i e. Z |-> ( H ` i ) ) )
69 14 68 ax-mp
 |-  ( ( i e. RR |-> ( H ` i ) ) |` Z ) = ( i e. Z |-> ( H ` i ) )
70 67 69 eqtrdi
 |-  ( ( ph /\ x e. A ) -> ( H |` Z ) = ( i e. Z |-> ( H ` i ) ) )
71 14 sseli
 |-  ( i e. Z -> i e. RR )
72 ffvelrn
 |-  ( ( H : RR --> RR /\ i e. RR ) -> ( H ` i ) e. RR )
73 26 71 72 syl2an
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> ( H ` i ) e. RR )
74 73 rexrd
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> ( H ` i ) e. RR* )
75 simplll
 |-  ( ( ( ( ph /\ x e. A ) /\ i e. Z ) /\ n e. ( ZZ>= ` i ) ) -> ph )
76 1 uztrn2
 |-  ( ( i e. Z /\ n e. ( ZZ>= ` i ) ) -> n e. Z )
77 76 adantll
 |-  ( ( ( ( ph /\ x e. A ) /\ i e. Z ) /\ n e. ( ZZ>= ` i ) ) -> n e. Z )
78 simpllr
 |-  ( ( ( ( ph /\ x e. A ) /\ i e. Z ) /\ n e. ( ZZ>= ` i ) ) -> x e. A )
79 75 77 78 7 syl12anc
 |-  ( ( ( ( ph /\ x e. A ) /\ i e. Z ) /\ n e. ( ZZ>= ` i ) ) -> B e. RR )
80 79 fmpttd
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> ( n e. ( ZZ>= ` i ) |-> B ) : ( ZZ>= ` i ) --> RR )
81 80 frnd
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> ran ( n e. ( ZZ>= ` i ) |-> B ) C_ RR )
82 eqid
 |-  ( n e. ( ZZ>= ` i ) |-> B ) = ( n e. ( ZZ>= ` i ) |-> B )
83 82 79 dmmptd
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> dom ( n e. ( ZZ>= ` i ) |-> B ) = ( ZZ>= ` i ) )
84 simpr
 |-  ( ( ph /\ i e. Z ) -> i e. Z )
85 84 1 eleqtrdi
 |-  ( ( ph /\ i e. Z ) -> i e. ( ZZ>= ` M ) )
86 eluzelz
 |-  ( i e. ( ZZ>= ` M ) -> i e. ZZ )
87 85 86 syl
 |-  ( ( ph /\ i e. Z ) -> i e. ZZ )
88 87 adantlr
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> i e. ZZ )
89 uzid
 |-  ( i e. ZZ -> i e. ( ZZ>= ` i ) )
90 ne0i
 |-  ( i e. ( ZZ>= ` i ) -> ( ZZ>= ` i ) =/= (/) )
91 88 89 90 3syl
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> ( ZZ>= ` i ) =/= (/) )
92 83 91 eqnetrd
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> dom ( n e. ( ZZ>= ` i ) |-> B ) =/= (/) )
93 dm0rn0
 |-  ( dom ( n e. ( ZZ>= ` i ) |-> B ) = (/) <-> ran ( n e. ( ZZ>= ` i ) |-> B ) = (/) )
94 93 necon3bii
 |-  ( dom ( n e. ( ZZ>= ` i ) |-> B ) =/= (/) <-> ran ( n e. ( ZZ>= ` i ) |-> B ) =/= (/) )
95 92 94 sylib
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> ran ( n e. ( ZZ>= ` i ) |-> B ) =/= (/) )
96 85 adantlr
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> i e. ( ZZ>= ` M ) )
97 uzss
 |-  ( i e. ( ZZ>= ` M ) -> ( ZZ>= ` i ) C_ ( ZZ>= ` M ) )
98 96 97 syl
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> ( ZZ>= ` i ) C_ ( ZZ>= ` M ) )
99 98 1 sseqtrrdi
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> ( ZZ>= ` i ) C_ Z )
100 73 leidd
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> ( H ` i ) <_ ( H ` i ) )
101 14 a1i
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> Z C_ RR )
102 45 adantr
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> ( n e. Z |-> B ) : Z --> RR* )
103 simpr
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> i e. Z )
104 14 103 sselid
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> i e. RR )
105 3 limsupgle
 |-  ( ( ( Z C_ RR /\ ( n e. Z |-> B ) : Z --> RR* ) /\ i e. RR /\ ( H ` i ) e. RR* ) -> ( ( H ` i ) <_ ( H ` i ) <-> A. k e. Z ( i <_ k -> ( ( n e. Z |-> B ) ` k ) <_ ( H ` i ) ) ) )
106 101 102 104 74 105 syl211anc
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> ( ( H ` i ) <_ ( H ` i ) <-> A. k e. Z ( i <_ k -> ( ( n e. Z |-> B ) ` k ) <_ ( H ` i ) ) ) )
107 100 106 mpbid
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> A. k e. Z ( i <_ k -> ( ( n e. Z |-> B ) ` k ) <_ ( H ` i ) ) )
108 ssralv
 |-  ( ( ZZ>= ` i ) C_ Z -> ( A. k e. Z ( i <_ k -> ( ( n e. Z |-> B ) ` k ) <_ ( H ` i ) ) -> A. k e. ( ZZ>= ` i ) ( i <_ k -> ( ( n e. Z |-> B ) ` k ) <_ ( H ` i ) ) ) )
109 99 107 108 sylc
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> A. k e. ( ZZ>= ` i ) ( i <_ k -> ( ( n e. Z |-> B ) ` k ) <_ ( H ` i ) ) )
110 99 adantr
 |-  ( ( ( ( ph /\ x e. A ) /\ i e. Z ) /\ k e. ( ZZ>= ` i ) ) -> ( ZZ>= ` i ) C_ Z )
111 110 resmptd
 |-  ( ( ( ( ph /\ x e. A ) /\ i e. Z ) /\ k e. ( ZZ>= ` i ) ) -> ( ( n e. Z |-> B ) |` ( ZZ>= ` i ) ) = ( n e. ( ZZ>= ` i ) |-> B ) )
112 111 fveq1d
 |-  ( ( ( ( ph /\ x e. A ) /\ i e. Z ) /\ k e. ( ZZ>= ` i ) ) -> ( ( ( n e. Z |-> B ) |` ( ZZ>= ` i ) ) ` k ) = ( ( n e. ( ZZ>= ` i ) |-> B ) ` k ) )
113 fvres
 |-  ( k e. ( ZZ>= ` i ) -> ( ( ( n e. Z |-> B ) |` ( ZZ>= ` i ) ) ` k ) = ( ( n e. Z |-> B ) ` k ) )
114 113 adantl
 |-  ( ( ( ( ph /\ x e. A ) /\ i e. Z ) /\ k e. ( ZZ>= ` i ) ) -> ( ( ( n e. Z |-> B ) |` ( ZZ>= ` i ) ) ` k ) = ( ( n e. Z |-> B ) ` k ) )
115 112 114 eqtr3d
 |-  ( ( ( ( ph /\ x e. A ) /\ i e. Z ) /\ k e. ( ZZ>= ` i ) ) -> ( ( n e. ( ZZ>= ` i ) |-> B ) ` k ) = ( ( n e. Z |-> B ) ` k ) )
116 115 breq1d
 |-  ( ( ( ( ph /\ x e. A ) /\ i e. Z ) /\ k e. ( ZZ>= ` i ) ) -> ( ( ( n e. ( ZZ>= ` i ) |-> B ) ` k ) <_ ( H ` i ) <-> ( ( n e. Z |-> B ) ` k ) <_ ( H ` i ) ) )
117 eluzle
 |-  ( k e. ( ZZ>= ` i ) -> i <_ k )
118 117 adantl
 |-  ( ( ( ( ph /\ x e. A ) /\ i e. Z ) /\ k e. ( ZZ>= ` i ) ) -> i <_ k )
119 biimt
 |-  ( i <_ k -> ( ( ( n e. Z |-> B ) ` k ) <_ ( H ` i ) <-> ( i <_ k -> ( ( n e. Z |-> B ) ` k ) <_ ( H ` i ) ) ) )
120 118 119 syl
 |-  ( ( ( ( ph /\ x e. A ) /\ i e. Z ) /\ k e. ( ZZ>= ` i ) ) -> ( ( ( n e. Z |-> B ) ` k ) <_ ( H ` i ) <-> ( i <_ k -> ( ( n e. Z |-> B ) ` k ) <_ ( H ` i ) ) ) )
121 116 120 bitrd
 |-  ( ( ( ( ph /\ x e. A ) /\ i e. Z ) /\ k e. ( ZZ>= ` i ) ) -> ( ( ( n e. ( ZZ>= ` i ) |-> B ) ` k ) <_ ( H ` i ) <-> ( i <_ k -> ( ( n e. Z |-> B ) ` k ) <_ ( H ` i ) ) ) )
122 121 ralbidva
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> ( A. k e. ( ZZ>= ` i ) ( ( n e. ( ZZ>= ` i ) |-> B ) ` k ) <_ ( H ` i ) <-> A. k e. ( ZZ>= ` i ) ( i <_ k -> ( ( n e. Z |-> B ) ` k ) <_ ( H ` i ) ) ) )
123 109 122 mpbird
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> A. k e. ( ZZ>= ` i ) ( ( n e. ( ZZ>= ` i ) |-> B ) ` k ) <_ ( H ` i ) )
124 ffn
 |-  ( ( n e. ( ZZ>= ` i ) |-> B ) : ( ZZ>= ` i ) --> RR -> ( n e. ( ZZ>= ` i ) |-> B ) Fn ( ZZ>= ` i ) )
125 breq1
 |-  ( z = ( ( n e. ( ZZ>= ` i ) |-> B ) ` k ) -> ( z <_ ( H ` i ) <-> ( ( n e. ( ZZ>= ` i ) |-> B ) ` k ) <_ ( H ` i ) ) )
126 125 ralrn
 |-  ( ( n e. ( ZZ>= ` i ) |-> B ) Fn ( ZZ>= ` i ) -> ( A. z e. ran ( n e. ( ZZ>= ` i ) |-> B ) z <_ ( H ` i ) <-> A. k e. ( ZZ>= ` i ) ( ( n e. ( ZZ>= ` i ) |-> B ) ` k ) <_ ( H ` i ) ) )
127 80 124 126 3syl
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> ( A. z e. ran ( n e. ( ZZ>= ` i ) |-> B ) z <_ ( H ` i ) <-> A. k e. ( ZZ>= ` i ) ( ( n e. ( ZZ>= ` i ) |-> B ) ` k ) <_ ( H ` i ) ) )
128 123 127 mpbird
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> A. z e. ran ( n e. ( ZZ>= ` i ) |-> B ) z <_ ( H ` i ) )
129 brralrspcev
 |-  ( ( ( H ` i ) e. RR /\ A. z e. ran ( n e. ( ZZ>= ` i ) |-> B ) z <_ ( H ` i ) ) -> E. y e. RR A. z e. ran ( n e. ( ZZ>= ` i ) |-> B ) z <_ y )
130 73 128 129 syl2anc
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> E. y e. RR A. z e. ran ( n e. ( ZZ>= ` i ) |-> B ) z <_ y )
131 81 95 130 suprcld
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) e. RR )
132 131 rexrd
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) e. RR* )
133 81 adantr
 |-  ( ( ( ( ph /\ x e. A ) /\ i e. Z ) /\ ( k e. Z /\ i <_ k ) ) -> ran ( n e. ( ZZ>= ` i ) |-> B ) C_ RR )
134 95 adantr
 |-  ( ( ( ( ph /\ x e. A ) /\ i e. Z ) /\ ( k e. Z /\ i <_ k ) ) -> ran ( n e. ( ZZ>= ` i ) |-> B ) =/= (/) )
135 130 adantr
 |-  ( ( ( ( ph /\ x e. A ) /\ i e. Z ) /\ ( k e. Z /\ i <_ k ) ) -> E. y e. RR A. z e. ran ( n e. ( ZZ>= ` i ) |-> B ) z <_ y )
136 12 sseli
 |-  ( k e. Z -> k e. ZZ )
137 eluz
 |-  ( ( i e. ZZ /\ k e. ZZ ) -> ( k e. ( ZZ>= ` i ) <-> i <_ k ) )
138 88 136 137 syl2an
 |-  ( ( ( ( ph /\ x e. A ) /\ i e. Z ) /\ k e. Z ) -> ( k e. ( ZZ>= ` i ) <-> i <_ k ) )
139 138 biimprd
 |-  ( ( ( ( ph /\ x e. A ) /\ i e. Z ) /\ k e. Z ) -> ( i <_ k -> k e. ( ZZ>= ` i ) ) )
140 139 impr
 |-  ( ( ( ( ph /\ x e. A ) /\ i e. Z ) /\ ( k e. Z /\ i <_ k ) ) -> k e. ( ZZ>= ` i ) )
141 140 115 syldan
 |-  ( ( ( ( ph /\ x e. A ) /\ i e. Z ) /\ ( k e. Z /\ i <_ k ) ) -> ( ( n e. ( ZZ>= ` i ) |-> B ) ` k ) = ( ( n e. Z |-> B ) ` k ) )
142 80 adantr
 |-  ( ( ( ( ph /\ x e. A ) /\ i e. Z ) /\ ( k e. Z /\ i <_ k ) ) -> ( n e. ( ZZ>= ` i ) |-> B ) : ( ZZ>= ` i ) --> RR )
143 142 124 syl
 |-  ( ( ( ( ph /\ x e. A ) /\ i e. Z ) /\ ( k e. Z /\ i <_ k ) ) -> ( n e. ( ZZ>= ` i ) |-> B ) Fn ( ZZ>= ` i ) )
144 fnfvelrn
 |-  ( ( ( n e. ( ZZ>= ` i ) |-> B ) Fn ( ZZ>= ` i ) /\ k e. ( ZZ>= ` i ) ) -> ( ( n e. ( ZZ>= ` i ) |-> B ) ` k ) e. ran ( n e. ( ZZ>= ` i ) |-> B ) )
145 143 140 144 syl2anc
 |-  ( ( ( ( ph /\ x e. A ) /\ i e. Z ) /\ ( k e. Z /\ i <_ k ) ) -> ( ( n e. ( ZZ>= ` i ) |-> B ) ` k ) e. ran ( n e. ( ZZ>= ` i ) |-> B ) )
146 141 145 eqeltrrd
 |-  ( ( ( ( ph /\ x e. A ) /\ i e. Z ) /\ ( k e. Z /\ i <_ k ) ) -> ( ( n e. Z |-> B ) ` k ) e. ran ( n e. ( ZZ>= ` i ) |-> B ) )
147 133 134 135 146 suprubd
 |-  ( ( ( ( ph /\ x e. A ) /\ i e. Z ) /\ ( k e. Z /\ i <_ k ) ) -> ( ( n e. Z |-> B ) ` k ) <_ sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) )
148 147 expr
 |-  ( ( ( ( ph /\ x e. A ) /\ i e. Z ) /\ k e. Z ) -> ( i <_ k -> ( ( n e. Z |-> B ) ` k ) <_ sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) ) )
149 148 ralrimiva
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> A. k e. Z ( i <_ k -> ( ( n e. Z |-> B ) ` k ) <_ sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) ) )
150 3 limsupgle
 |-  ( ( ( Z C_ RR /\ ( n e. Z |-> B ) : Z --> RR* ) /\ i e. RR /\ sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) e. RR* ) -> ( ( H ` i ) <_ sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) <-> A. k e. Z ( i <_ k -> ( ( n e. Z |-> B ) ` k ) <_ sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) ) ) )
151 101 102 104 132 150 syl211anc
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> ( ( H ` i ) <_ sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) <-> A. k e. Z ( i <_ k -> ( ( n e. Z |-> B ) ` k ) <_ sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) ) ) )
152 149 151 mpbird
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> ( H ` i ) <_ sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) )
153 suprleub
 |-  ( ( ( ran ( n e. ( ZZ>= ` i ) |-> B ) C_ RR /\ ran ( n e. ( ZZ>= ` i ) |-> B ) =/= (/) /\ E. y e. RR A. z e. ran ( n e. ( ZZ>= ` i ) |-> B ) z <_ y ) /\ ( H ` i ) e. RR ) -> ( sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) <_ ( H ` i ) <-> A. z e. ran ( n e. ( ZZ>= ` i ) |-> B ) z <_ ( H ` i ) ) )
154 81 95 130 73 153 syl31anc
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> ( sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) <_ ( H ` i ) <-> A. z e. ran ( n e. ( ZZ>= ` i ) |-> B ) z <_ ( H ` i ) ) )
155 128 154 mpbird
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) <_ ( H ` i ) )
156 74 132 152 155 xrletrid
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> ( H ` i ) = sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) )
157 156 mpteq2dva
 |-  ( ( ph /\ x e. A ) -> ( i e. Z |-> ( H ` i ) ) = ( i e. Z |-> sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) ) )
158 70 157 eqtrd
 |-  ( ( ph /\ x e. A ) -> ( H |` Z ) = ( i e. Z |-> sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) ) )
159 158 rneqd
 |-  ( ( ph /\ x e. A ) -> ran ( H |` Z ) = ran ( i e. Z |-> sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) ) )
160 65 159 syl5eq
 |-  ( ( ph /\ x e. A ) -> ( H " Z ) = ran ( i e. Z |-> sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) ) )
161 160 infeq1d
 |-  ( ( ph /\ x e. A ) -> inf ( ( H " Z ) , RR , < ) = inf ( ran ( i e. Z |-> sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) ) , RR , < ) )
162 19 64 161 3eqtrd
 |-  ( ( ph /\ x e. A ) -> ( limsup ` ( n e. Z |-> B ) ) = inf ( ran ( i e. Z |-> sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) ) , RR , < ) )
163 162 mpteq2dva
 |-  ( ph -> ( x e. A |-> ( limsup ` ( n e. Z |-> B ) ) ) = ( x e. A |-> inf ( ran ( i e. Z |-> sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) ) , RR , < ) ) )
164 2 163 syl5eq
 |-  ( ph -> G = ( x e. A |-> inf ( ran ( i e. Z |-> sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) ) , RR , < ) ) )
165 eqid
 |-  ( x e. A |-> inf ( ran ( i e. Z |-> sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) ) , RR , < ) ) = ( x e. A |-> inf ( ran ( i e. Z |-> sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) ) , RR , < ) )
166 eqid
 |-  ( ZZ>= ` i ) = ( ZZ>= ` i )
167 eqid
 |-  ( x e. A |-> sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) ) = ( x e. A |-> sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) )
168 simpll
 |-  ( ( ( ph /\ i e. Z ) /\ n e. ( ZZ>= ` i ) ) -> ph )
169 76 adantll
 |-  ( ( ( ph /\ i e. Z ) /\ n e. ( ZZ>= ` i ) ) -> n e. Z )
170 168 169 6 syl2anc
 |-  ( ( ( ph /\ i e. Z ) /\ n e. ( ZZ>= ` i ) ) -> ( x e. A |-> B ) e. MblFn )
171 simpll
 |-  ( ( ( ph /\ i e. Z ) /\ ( n e. ( ZZ>= ` i ) /\ x e. A ) ) -> ph )
172 76 ad2ant2lr
 |-  ( ( ( ph /\ i e. Z ) /\ ( n e. ( ZZ>= ` i ) /\ x e. A ) ) -> n e. Z )
173 simprr
 |-  ( ( ( ph /\ i e. Z ) /\ ( n e. ( ZZ>= ` i ) /\ x e. A ) ) -> x e. A )
174 171 172 173 7 syl12anc
 |-  ( ( ( ph /\ i e. Z ) /\ ( n e. ( ZZ>= ` i ) /\ x e. A ) ) -> B e. RR )
175 79 ralrimiva
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> A. n e. ( ZZ>= ` i ) B e. RR )
176 breq1
 |-  ( z = B -> ( z <_ y <-> B <_ y ) )
177 82 176 ralrnmptw
 |-  ( A. n e. ( ZZ>= ` i ) B e. RR -> ( A. z e. ran ( n e. ( ZZ>= ` i ) |-> B ) z <_ y <-> A. n e. ( ZZ>= ` i ) B <_ y ) )
178 175 177 syl
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> ( A. z e. ran ( n e. ( ZZ>= ` i ) |-> B ) z <_ y <-> A. n e. ( ZZ>= ` i ) B <_ y ) )
179 178 rexbidv
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> ( E. y e. RR A. z e. ran ( n e. ( ZZ>= ` i ) |-> B ) z <_ y <-> E. y e. RR A. n e. ( ZZ>= ` i ) B <_ y ) )
180 130 179 mpbid
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> E. y e. RR A. n e. ( ZZ>= ` i ) B <_ y )
181 180 an32s
 |-  ( ( ( ph /\ i e. Z ) /\ x e. A ) -> E. y e. RR A. n e. ( ZZ>= ` i ) B <_ y )
182 166 167 87 170 174 181 mbfsup
 |-  ( ( ph /\ i e. Z ) -> ( x e. A |-> sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) ) e. MblFn )
183 131 an32s
 |-  ( ( ( ph /\ i e. Z ) /\ x e. A ) -> sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) e. RR )
184 183 anasss
 |-  ( ( ph /\ ( i e. Z /\ x e. A ) ) -> sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) e. RR )
185 3 limsuple
 |-  ( ( Z C_ RR /\ ( n e. Z |-> B ) : Z --> RR* /\ ( limsup ` ( n e. Z |-> B ) ) e. RR* ) -> ( ( limsup ` ( n e. Z |-> B ) ) <_ ( limsup ` ( n e. Z |-> B ) ) <-> A. i e. RR ( limsup ` ( n e. Z |-> B ) ) <_ ( H ` i ) ) )
186 15 45 46 185 syl3anc
 |-  ( ( ph /\ x e. A ) -> ( ( limsup ` ( n e. Z |-> B ) ) <_ ( limsup ` ( n e. Z |-> B ) ) <-> A. i e. RR ( limsup ` ( n e. Z |-> B ) ) <_ ( H ` i ) ) )
187 43 186 mpbid
 |-  ( ( ph /\ x e. A ) -> A. i e. RR ( limsup ` ( n e. Z |-> B ) ) <_ ( H ` i ) )
188 ssralv
 |-  ( Z C_ RR -> ( A. i e. RR ( limsup ` ( n e. Z |-> B ) ) <_ ( H ` i ) -> A. i e. Z ( limsup ` ( n e. Z |-> B ) ) <_ ( H ` i ) ) )
189 14 187 188 mpsyl
 |-  ( ( ph /\ x e. A ) -> A. i e. Z ( limsup ` ( n e. Z |-> B ) ) <_ ( H ` i ) )
190 156 breq2d
 |-  ( ( ( ph /\ x e. A ) /\ i e. Z ) -> ( ( limsup ` ( n e. Z |-> B ) ) <_ ( H ` i ) <-> ( limsup ` ( n e. Z |-> B ) ) <_ sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) ) )
191 190 ralbidva
 |-  ( ( ph /\ x e. A ) -> ( A. i e. Z ( limsup ` ( n e. Z |-> B ) ) <_ ( H ` i ) <-> A. i e. Z ( limsup ` ( n e. Z |-> B ) ) <_ sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) ) )
192 189 191 mpbid
 |-  ( ( ph /\ x e. A ) -> A. i e. Z ( limsup ` ( n e. Z |-> B ) ) <_ sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) )
193 breq1
 |-  ( y = ( limsup ` ( n e. Z |-> B ) ) -> ( y <_ sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) <-> ( limsup ` ( n e. Z |-> B ) ) <_ sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) ) )
194 193 ralbidv
 |-  ( y = ( limsup ` ( n e. Z |-> B ) ) -> ( A. i e. Z y <_ sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) <-> A. i e. Z ( limsup ` ( n e. Z |-> B ) ) <_ sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) ) )
195 194 rspcev
 |-  ( ( ( limsup ` ( n e. Z |-> B ) ) e. RR /\ A. i e. Z ( limsup ` ( n e. Z |-> B ) ) <_ sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) ) -> E. y e. RR A. i e. Z y <_ sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) )
196 5 192 195 syl2anc
 |-  ( ( ph /\ x e. A ) -> E. y e. RR A. i e. Z y <_ sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) )
197 1 165 4 182 184 196 mbfinf
 |-  ( ph -> ( x e. A |-> inf ( ran ( i e. Z |-> sup ( ran ( n e. ( ZZ>= ` i ) |-> B ) , RR , < ) ) , RR , < ) ) e. MblFn )
198 164 197 eqeltrd
 |-  ( ph -> G e. MblFn )