Metamath Proof Explorer

Theorem limsuple

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 limsuple 
|- ( ( B C_ RR /\ F : B --> RR* /\ A e. RR* ) -> ( A <_ ( limsup ` F ) <-> A. j e. RR A <_ ( G ` j ) ) )

Proof

Step Hyp Ref Expression
1 limsupval.1 
 |-  G = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
2 simp2 
 |-  ( ( B C_ RR /\ F : B --> RR* /\ A e. RR* ) -> F : B --> RR* )
3 reex 
 |-  RR e. _V
4 3 ssex 
 |-  ( B C_ RR -> B e. _V )
5 4 3ad2ant1 
 |-  ( ( B C_ RR /\ F : B --> RR* /\ A e. RR* ) -> B e. _V )
6 xrex 
 |-  RR* e. _V
7 6 a1i 
 |-  ( ( B C_ RR /\ F : B --> RR* /\ A e. RR* ) -> RR* e. _V )
8 fex2 
 |-  ( ( F : B --> RR* /\ B e. _V /\ RR* e. _V ) -> F e. _V )
9 2 5 7 8 syl3anc 
 |-  ( ( B C_ RR /\ F : B --> RR* /\ A e. RR* ) -> F e. _V )
10 1 limsupval 
 |-  ( F e. _V -> ( limsup ` F ) = inf ( ran G , RR* , < ) )
11 9 10 syl 
 |-  ( ( B C_ RR /\ F : B --> RR* /\ A e. RR* ) -> ( limsup ` F ) = inf ( ran G , RR* , < ) )
12 11 breq2d 
 |-  ( ( B C_ RR /\ F : B --> RR* /\ A e. RR* ) -> ( A <_ ( limsup ` F ) <-> A <_ inf ( ran G , RR* , < ) ) )
13 1 limsupgf 
 |-  G : RR --> RR*
14 frn 
 |-  ( G : RR --> RR* -> ran G C_ RR* )
15 13 14 ax-mp 
 |-  ran G C_ RR*
16 simp3 
 |-  ( ( B C_ RR /\ F : B --> RR* /\ A e. RR* ) -> A e. RR* )
17 infxrgelb 
 |-  ( ( ran G C_ RR* /\ A e. RR* ) -> ( A <_ inf ( ran G , RR* , < ) <-> A. x e. ran G A <_ x ) )
18 15 16 17 sylancr 
 |-  ( ( B C_ RR /\ F : B --> RR* /\ A e. RR* ) -> ( A <_ inf ( ran G , RR* , < ) <-> A. x e. ran G A <_ x ) )
19 ffn 
 |-  ( G : RR --> RR* -> G Fn RR )
20 13 19 ax-mp 
 |-  G Fn RR
21 breq2 
 |-  ( x = ( G ` j ) -> ( A <_ x <-> A <_ ( G ` j ) ) )
22 21 ralrn 
 |-  ( G Fn RR -> ( A. x e. ran G A <_ x <-> A. j e. RR A <_ ( G ` j ) ) )
23 20 22 ax-mp 
 |-  ( A. x e. ran G A <_ x <-> A. j e. RR A <_ ( G ` j ) )
24 18 23 bitrdi 
 |-  ( ( B C_ RR /\ F : B --> RR* /\ A e. RR* ) -> ( A <_ inf ( ran G , RR* , < ) <-> A. j e. RR A <_ ( G ` j ) ) )
25 12 24 bitrd 
 |-  ( ( B C_ RR /\ F : B --> RR* /\ A e. RR* ) -> ( A <_ ( limsup ` F ) <-> A. j e. RR A <_ ( G ` j ) ) )