Step |
Hyp |
Ref |
Expression |
1 |
|
limsupval.1 |
|- G = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) |
2 |
1
|
limsuple |
|- ( ( B C_ RR /\ F : B --> RR* /\ A e. RR* ) -> ( A <_ ( limsup ` F ) <-> A. j e. RR A <_ ( G ` j ) ) ) |
3 |
2
|
notbid |
|- ( ( B C_ RR /\ F : B --> RR* /\ A e. RR* ) -> ( -. A <_ ( limsup ` F ) <-> -. A. j e. RR A <_ ( G ` j ) ) ) |
4 |
|
rexnal |
|- ( E. j e. RR -. A <_ ( G ` j ) <-> -. A. j e. RR A <_ ( G ` j ) ) |
5 |
3 4
|
bitr4di |
|- ( ( B C_ RR /\ F : B --> RR* /\ A e. RR* ) -> ( -. A <_ ( limsup ` F ) <-> E. j e. RR -. A <_ ( G ` j ) ) ) |
6 |
|
simp2 |
|- ( ( B C_ RR /\ F : B --> RR* /\ A e. RR* ) -> F : B --> RR* ) |
7 |
|
reex |
|- RR e. _V |
8 |
7
|
ssex |
|- ( B C_ RR -> B e. _V ) |
9 |
8
|
3ad2ant1 |
|- ( ( B C_ RR /\ F : B --> RR* /\ A e. RR* ) -> B e. _V ) |
10 |
|
xrex |
|- RR* e. _V |
11 |
10
|
a1i |
|- ( ( B C_ RR /\ F : B --> RR* /\ A e. RR* ) -> RR* e. _V ) |
12 |
|
fex2 |
|- ( ( F : B --> RR* /\ B e. _V /\ RR* e. _V ) -> F e. _V ) |
13 |
6 9 11 12
|
syl3anc |
|- ( ( B C_ RR /\ F : B --> RR* /\ A e. RR* ) -> F e. _V ) |
14 |
|
limsupcl |
|- ( F e. _V -> ( limsup ` F ) e. RR* ) |
15 |
13 14
|
syl |
|- ( ( B C_ RR /\ F : B --> RR* /\ A e. RR* ) -> ( limsup ` F ) e. RR* ) |
16 |
|
simp3 |
|- ( ( B C_ RR /\ F : B --> RR* /\ A e. RR* ) -> A e. RR* ) |
17 |
|
xrltnle |
|- ( ( ( limsup ` F ) e. RR* /\ A e. RR* ) -> ( ( limsup ` F ) < A <-> -. A <_ ( limsup ` F ) ) ) |
18 |
15 16 17
|
syl2anc |
|- ( ( B C_ RR /\ F : B --> RR* /\ A e. RR* ) -> ( ( limsup ` F ) < A <-> -. A <_ ( limsup ` F ) ) ) |
19 |
1
|
limsupgf |
|- G : RR --> RR* |
20 |
19
|
ffvelrni |
|- ( j e. RR -> ( G ` j ) e. RR* ) |
21 |
|
xrltnle |
|- ( ( ( G ` j ) e. RR* /\ A e. RR* ) -> ( ( G ` j ) < A <-> -. A <_ ( G ` j ) ) ) |
22 |
20 16 21
|
syl2anr |
|- ( ( ( B C_ RR /\ F : B --> RR* /\ A e. RR* ) /\ j e. RR ) -> ( ( G ` j ) < A <-> -. A <_ ( G ` j ) ) ) |
23 |
22
|
rexbidva |
|- ( ( B C_ RR /\ F : B --> RR* /\ A e. RR* ) -> ( E. j e. RR ( G ` j ) < A <-> E. j e. RR -. A <_ ( G ` j ) ) ) |
24 |
5 18 23
|
3bitr4d |
|- ( ( B C_ RR /\ F : B --> RR* /\ A e. RR* ) -> ( ( limsup ` F ) < A <-> E. j e. RR ( G ` j ) < A ) ) |