Metamath Proof Explorer


Theorem limsuplt

Description: The defining property of the superior limit. (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by AV, 12-Sep-2020)

Ref Expression
Hypothesis limsupval.1
|- G = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
Assertion limsuplt
|- ( ( B C_ RR /\ F : B --> RR* /\ A e. RR* ) -> ( ( limsup ` F ) < A <-> E. j e. RR ( G ` j ) < A ) )

Proof

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