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
|
eqtrid |
|- ( ( 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
|
eqtrid |
|- ( 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 ) |