This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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