Step |
Hyp |
Ref |
Expression |
1 |
|
limsupre.1 |
|- ( ph -> B C_ RR ) |
2 |
|
limsupre.2 |
|- ( ph -> sup ( B , RR* , < ) = +oo ) |
3 |
|
limsupre.f |
|- ( ph -> F : B --> RR ) |
4 |
|
limsupre.bnd |
|- ( ph -> E. b e. RR E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) |
5 |
|
mnfxr |
|- -oo e. RR* |
6 |
5
|
a1i |
|- ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> -oo e. RR* ) |
7 |
|
renegcl |
|- ( b e. RR -> -u b e. RR ) |
8 |
7
|
rexrd |
|- ( b e. RR -> -u b e. RR* ) |
9 |
8
|
ad2antlr |
|- ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> -u b e. RR* ) |
10 |
|
reex |
|- RR e. _V |
11 |
10
|
a1i |
|- ( ph -> RR e. _V ) |
12 |
11 1
|
ssexd |
|- ( ph -> B e. _V ) |
13 |
|
fex |
|- ( ( F : B --> RR /\ B e. _V ) -> F e. _V ) |
14 |
3 12 13
|
syl2anc |
|- ( ph -> F e. _V ) |
15 |
|
limsupcl |
|- ( F e. _V -> ( limsup ` F ) e. RR* ) |
16 |
14 15
|
syl |
|- ( ph -> ( limsup ` F ) e. RR* ) |
17 |
16
|
ad2antrr |
|- ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> ( limsup ` F ) e. RR* ) |
18 |
7
|
mnfltd |
|- ( b e. RR -> -oo < -u b ) |
19 |
18
|
ad2antlr |
|- ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> -oo < -u b ) |
20 |
1
|
ad2antrr |
|- ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> B C_ RR ) |
21 |
|
ressxr |
|- RR C_ RR* |
22 |
21
|
a1i |
|- ( ph -> RR C_ RR* ) |
23 |
3 22
|
fssd |
|- ( ph -> F : B --> RR* ) |
24 |
23
|
ad2antrr |
|- ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> F : B --> RR* ) |
25 |
2
|
ad2antrr |
|- ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> sup ( B , RR* , < ) = +oo ) |
26 |
|
simpr |
|- ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) |
27 |
|
nfv |
|- F/ k ( ph /\ b e. RR ) |
28 |
|
nfre1 |
|- F/ k E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) |
29 |
27 28
|
nfan |
|- F/ k ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) |
30 |
|
nfv |
|- F/ j ( ph /\ b e. RR ) |
31 |
|
nfv |
|- F/ j k e. RR |
32 |
|
nfra1 |
|- F/ j A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) |
33 |
30 31 32
|
nf3an |
|- F/ j ( ( ph /\ b e. RR ) /\ k e. RR /\ A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) |
34 |
|
simp13 |
|- ( ( ( ( ph /\ b e. RR ) /\ k e. RR /\ A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) /\ j e. B /\ k <_ j ) -> A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) |
35 |
|
simp2 |
|- ( ( ( ( ph /\ b e. RR ) /\ k e. RR /\ A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) /\ j e. B /\ k <_ j ) -> j e. B ) |
36 |
|
simp3 |
|- ( ( ( ( ph /\ b e. RR ) /\ k e. RR /\ A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) /\ j e. B /\ k <_ j ) -> k <_ j ) |
37 |
|
rspa |
|- ( ( A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) /\ j e. B ) -> ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) |
38 |
37
|
imp |
|- ( ( ( A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) /\ j e. B ) /\ k <_ j ) -> ( abs ` ( F ` j ) ) <_ b ) |
39 |
34 35 36 38
|
syl21anc |
|- ( ( ( ( ph /\ b e. RR ) /\ k e. RR /\ A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) /\ j e. B /\ k <_ j ) -> ( abs ` ( F ` j ) ) <_ b ) |
40 |
|
simp11l |
|- ( ( ( ( ph /\ b e. RR ) /\ k e. RR /\ A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) /\ j e. B /\ k <_ j ) -> ph ) |
41 |
3
|
ffvelrnda |
|- ( ( ph /\ j e. B ) -> ( F ` j ) e. RR ) |
42 |
40 35 41
|
syl2anc |
|- ( ( ( ( ph /\ b e. RR ) /\ k e. RR /\ A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) /\ j e. B /\ k <_ j ) -> ( F ` j ) e. RR ) |
43 |
|
simp11r |
|- ( ( ( ( ph /\ b e. RR ) /\ k e. RR /\ A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) /\ j e. B /\ k <_ j ) -> b e. RR ) |
44 |
42 43
|
absled |
|- ( ( ( ( ph /\ b e. RR ) /\ k e. RR /\ A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) /\ j e. B /\ k <_ j ) -> ( ( abs ` ( F ` j ) ) <_ b <-> ( -u b <_ ( F ` j ) /\ ( F ` j ) <_ b ) ) ) |
45 |
39 44
|
mpbid |
|- ( ( ( ( ph /\ b e. RR ) /\ k e. RR /\ A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) /\ j e. B /\ k <_ j ) -> ( -u b <_ ( F ` j ) /\ ( F ` j ) <_ b ) ) |
46 |
45
|
simpld |
|- ( ( ( ( ph /\ b e. RR ) /\ k e. RR /\ A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) /\ j e. B /\ k <_ j ) -> -u b <_ ( F ` j ) ) |
47 |
46
|
3exp |
|- ( ( ( ph /\ b e. RR ) /\ k e. RR /\ A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> ( j e. B -> ( k <_ j -> -u b <_ ( F ` j ) ) ) ) |
48 |
33 47
|
ralrimi |
|- ( ( ( ph /\ b e. RR ) /\ k e. RR /\ A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> A. j e. B ( k <_ j -> -u b <_ ( F ` j ) ) ) |
49 |
48
|
3exp |
|- ( ( ph /\ b e. RR ) -> ( k e. RR -> ( A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) -> A. j e. B ( k <_ j -> -u b <_ ( F ` j ) ) ) ) ) |
50 |
49
|
adantr |
|- ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> ( k e. RR -> ( A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) -> A. j e. B ( k <_ j -> -u b <_ ( F ` j ) ) ) ) ) |
51 |
29 50
|
reximdai |
|- ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> ( E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) -> E. k e. RR A. j e. B ( k <_ j -> -u b <_ ( F ` j ) ) ) ) |
52 |
26 51
|
mpd |
|- ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> E. k e. RR A. j e. B ( k <_ j -> -u b <_ ( F ` j ) ) ) |
53 |
|
breq2 |
|- ( i = j -> ( h <_ i <-> h <_ j ) ) |
54 |
|
fveq2 |
|- ( i = j -> ( F ` i ) = ( F ` j ) ) |
55 |
54
|
breq2d |
|- ( i = j -> ( -u b <_ ( F ` i ) <-> -u b <_ ( F ` j ) ) ) |
56 |
53 55
|
imbi12d |
|- ( i = j -> ( ( h <_ i -> -u b <_ ( F ` i ) ) <-> ( h <_ j -> -u b <_ ( F ` j ) ) ) ) |
57 |
56
|
cbvralvw |
|- ( A. i e. B ( h <_ i -> -u b <_ ( F ` i ) ) <-> A. j e. B ( h <_ j -> -u b <_ ( F ` j ) ) ) |
58 |
|
breq1 |
|- ( h = k -> ( h <_ j <-> k <_ j ) ) |
59 |
58
|
imbi1d |
|- ( h = k -> ( ( h <_ j -> -u b <_ ( F ` j ) ) <-> ( k <_ j -> -u b <_ ( F ` j ) ) ) ) |
60 |
59
|
ralbidv |
|- ( h = k -> ( A. j e. B ( h <_ j -> -u b <_ ( F ` j ) ) <-> A. j e. B ( k <_ j -> -u b <_ ( F ` j ) ) ) ) |
61 |
57 60
|
syl5bb |
|- ( h = k -> ( A. i e. B ( h <_ i -> -u b <_ ( F ` i ) ) <-> A. j e. B ( k <_ j -> -u b <_ ( F ` j ) ) ) ) |
62 |
61
|
cbvrexvw |
|- ( E. h e. RR A. i e. B ( h <_ i -> -u b <_ ( F ` i ) ) <-> E. k e. RR A. j e. B ( k <_ j -> -u b <_ ( F ` j ) ) ) |
63 |
52 62
|
sylibr |
|- ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> E. h e. RR A. i e. B ( h <_ i -> -u b <_ ( F ` i ) ) ) |
64 |
20 24 9 25 63
|
limsupbnd2 |
|- ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> -u b <_ ( limsup ` F ) ) |
65 |
6 9 17 19 64
|
xrltletrd |
|- ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> -oo < ( limsup ` F ) ) |
66 |
65 4
|
r19.29a |
|- ( ph -> -oo < ( limsup ` F ) ) |
67 |
|
rexr |
|- ( b e. RR -> b e. RR* ) |
68 |
67
|
ad2antlr |
|- ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> b e. RR* ) |
69 |
|
pnfxr |
|- +oo e. RR* |
70 |
69
|
a1i |
|- ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> +oo e. RR* ) |
71 |
45
|
simprd |
|- ( ( ( ( ph /\ b e. RR ) /\ k e. RR /\ A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) /\ j e. B /\ k <_ j ) -> ( F ` j ) <_ b ) |
72 |
71
|
3exp |
|- ( ( ( ph /\ b e. RR ) /\ k e. RR /\ A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> ( j e. B -> ( k <_ j -> ( F ` j ) <_ b ) ) ) |
73 |
33 72
|
ralrimi |
|- ( ( ( ph /\ b e. RR ) /\ k e. RR /\ A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> A. j e. B ( k <_ j -> ( F ` j ) <_ b ) ) |
74 |
73
|
3exp |
|- ( ( ph /\ b e. RR ) -> ( k e. RR -> ( A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) -> A. j e. B ( k <_ j -> ( F ` j ) <_ b ) ) ) ) |
75 |
74
|
adantr |
|- ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> ( k e. RR -> ( A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) -> A. j e. B ( k <_ j -> ( F ` j ) <_ b ) ) ) ) |
76 |
29 75
|
reximdai |
|- ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> ( E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) -> E. k e. RR A. j e. B ( k <_ j -> ( F ` j ) <_ b ) ) ) |
77 |
26 76
|
mpd |
|- ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> E. k e. RR A. j e. B ( k <_ j -> ( F ` j ) <_ b ) ) |
78 |
54
|
breq1d |
|- ( i = j -> ( ( F ` i ) <_ b <-> ( F ` j ) <_ b ) ) |
79 |
53 78
|
imbi12d |
|- ( i = j -> ( ( h <_ i -> ( F ` i ) <_ b ) <-> ( h <_ j -> ( F ` j ) <_ b ) ) ) |
80 |
79
|
cbvralvw |
|- ( A. i e. B ( h <_ i -> ( F ` i ) <_ b ) <-> A. j e. B ( h <_ j -> ( F ` j ) <_ b ) ) |
81 |
58
|
imbi1d |
|- ( h = k -> ( ( h <_ j -> ( F ` j ) <_ b ) <-> ( k <_ j -> ( F ` j ) <_ b ) ) ) |
82 |
81
|
ralbidv |
|- ( h = k -> ( A. j e. B ( h <_ j -> ( F ` j ) <_ b ) <-> A. j e. B ( k <_ j -> ( F ` j ) <_ b ) ) ) |
83 |
80 82
|
syl5bb |
|- ( h = k -> ( A. i e. B ( h <_ i -> ( F ` i ) <_ b ) <-> A. j e. B ( k <_ j -> ( F ` j ) <_ b ) ) ) |
84 |
83
|
cbvrexvw |
|- ( E. h e. RR A. i e. B ( h <_ i -> ( F ` i ) <_ b ) <-> E. k e. RR A. j e. B ( k <_ j -> ( F ` j ) <_ b ) ) |
85 |
77 84
|
sylibr |
|- ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> E. h e. RR A. i e. B ( h <_ i -> ( F ` i ) <_ b ) ) |
86 |
20 24 68 85
|
limsupbnd1 |
|- ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> ( limsup ` F ) <_ b ) |
87 |
|
ltpnf |
|- ( b e. RR -> b < +oo ) |
88 |
87
|
ad2antlr |
|- ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> b < +oo ) |
89 |
17 68 70 86 88
|
xrlelttrd |
|- ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> ( limsup ` F ) < +oo ) |
90 |
89 4
|
r19.29a |
|- ( ph -> ( limsup ` F ) < +oo ) |
91 |
|
xrrebnd |
|- ( ( limsup ` F ) e. RR* -> ( ( limsup ` F ) e. RR <-> ( -oo < ( limsup ` F ) /\ ( limsup ` F ) < +oo ) ) ) |
92 |
16 91
|
syl |
|- ( ph -> ( ( limsup ` F ) e. RR <-> ( -oo < ( limsup ` F ) /\ ( limsup ` F ) < +oo ) ) ) |
93 |
66 90 92
|
mpbir2and |
|- ( ph -> ( limsup ` F ) e. RR ) |