Metamath Proof Explorer

Theorem limsupgle

Description: The defining property of the superior limit function. (Contributed by Mario Carneiro, 5-Sep-2014) (Revised by Mario Carneiro, 7-May-2016)

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

Proof

Step Hyp Ref Expression
1 limsupval.1 
 |-  G = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
2 1 limsupgval 
 |-  ( C e. RR -> ( G ` C ) = sup ( ( ( F " ( C [,) +oo ) ) i^i RR* ) , RR* , < ) )
3 2 3ad2ant2 
 |-  ( ( ( B C_ RR /\ F : B --> RR* ) /\ C e. RR /\ A e. RR* ) -> ( G ` C ) = sup ( ( ( F " ( C [,) +oo ) ) i^i RR* ) , RR* , < ) )
4 3 breq1d 
 |-  ( ( ( B C_ RR /\ F : B --> RR* ) /\ C e. RR /\ A e. RR* ) -> ( ( G ` C ) <_ A <-> sup ( ( ( F " ( C [,) +oo ) ) i^i RR* ) , RR* , < ) <_ A ) )
5 inss2 
 |-  ( ( F " ( C [,) +oo ) ) i^i RR* ) C_ RR*
6 simp3 
 |-  ( ( ( B C_ RR /\ F : B --> RR* ) /\ C e. RR /\ A e. RR* ) -> A e. RR* )
7 supxrleub 
 |-  ( ( ( ( F " ( C [,) +oo ) ) i^i RR* ) C_ RR* /\ A e. RR* ) -> ( sup ( ( ( F " ( C [,) +oo ) ) i^i RR* ) , RR* , < ) <_ A <-> A. x e. ( ( F " ( C [,) +oo ) ) i^i RR* ) x <_ A ) )
8 5 6 7 sylancr 
 |-  ( ( ( B C_ RR /\ F : B --> RR* ) /\ C e. RR /\ A e. RR* ) -> ( sup ( ( ( F " ( C [,) +oo ) ) i^i RR* ) , RR* , < ) <_ A <-> A. x e. ( ( F " ( C [,) +oo ) ) i^i RR* ) x <_ A ) )
9 imassrn 
 |-  ( F " ( C [,) +oo ) ) C_ ran F
10 simp1r 
 |-  ( ( ( B C_ RR /\ F : B --> RR* ) /\ C e. RR /\ A e. RR* ) -> F : B --> RR* )
11 10 frnd 
 |-  ( ( ( B C_ RR /\ F : B --> RR* ) /\ C e. RR /\ A e. RR* ) -> ran F C_ RR* )
12 9 11 sstrid 
 |-  ( ( ( B C_ RR /\ F : B --> RR* ) /\ C e. RR /\ A e. RR* ) -> ( F " ( C [,) +oo ) ) C_ RR* )
13 df-ss 
 |-  ( ( F " ( C [,) +oo ) ) C_ RR* <-> ( ( F " ( C [,) +oo ) ) i^i RR* ) = ( F " ( C [,) +oo ) ) )
14 12 13 sylib 
 |-  ( ( ( B C_ RR /\ F : B --> RR* ) /\ C e. RR /\ A e. RR* ) -> ( ( F " ( C [,) +oo ) ) i^i RR* ) = ( F " ( C [,) +oo ) ) )
15 imadmres 
 |-  ( F " dom ( F |` ( C [,) +oo ) ) ) = ( F " ( C [,) +oo ) )
16 14 15 eqtr4di 
 |-  ( ( ( B C_ RR /\ F : B --> RR* ) /\ C e. RR /\ A e. RR* ) -> ( ( F " ( C [,) +oo ) ) i^i RR* ) = ( F " dom ( F |` ( C [,) +oo ) ) ) )
17 16 raleqdv 
 |-  ( ( ( B C_ RR /\ F : B --> RR* ) /\ C e. RR /\ A e. RR* ) -> ( A. x e. ( ( F " ( C [,) +oo ) ) i^i RR* ) x <_ A <-> A. x e. ( F " dom ( F |` ( C [,) +oo ) ) ) x <_ A ) )
18 10 ffnd 
 |-  ( ( ( B C_ RR /\ F : B --> RR* ) /\ C e. RR /\ A e. RR* ) -> F Fn B )
19 10 fdmd 
 |-  ( ( ( B C_ RR /\ F : B --> RR* ) /\ C e. RR /\ A e. RR* ) -> dom F = B )
20 19 ineq2d 
 |-  ( ( ( B C_ RR /\ F : B --> RR* ) /\ C e. RR /\ A e. RR* ) -> ( ( C [,) +oo ) i^i dom F ) = ( ( C [,) +oo ) i^i B ) )
21 dmres 
 |-  dom ( F |` ( C [,) +oo ) ) = ( ( C [,) +oo ) i^i dom F )
22 incom 
 |-  ( B i^i ( C [,) +oo ) ) = ( ( C [,) +oo ) i^i B )
23 20 21 22 3eqtr4g 
 |-  ( ( ( B C_ RR /\ F : B --> RR* ) /\ C e. RR /\ A e. RR* ) -> dom ( F |` ( C [,) +oo ) ) = ( B i^i ( C [,) +oo ) ) )
24 inss1 
 |-  ( B i^i ( C [,) +oo ) ) C_ B
25 23 24 eqsstrdi 
 |-  ( ( ( B C_ RR /\ F : B --> RR* ) /\ C e. RR /\ A e. RR* ) -> dom ( F |` ( C [,) +oo ) ) C_ B )
26 breq1 
 |-  ( x = ( F ` j ) -> ( x <_ A <-> ( F ` j ) <_ A ) )
27 26 ralima 
 |-  ( ( F Fn B /\ dom ( F |` ( C [,) +oo ) ) C_ B ) -> ( A. x e. ( F " dom ( F |` ( C [,) +oo ) ) ) x <_ A <-> A. j e. dom ( F |` ( C [,) +oo ) ) ( F ` j ) <_ A ) )
28 18 25 27 syl2anc 
 |-  ( ( ( B C_ RR /\ F : B --> RR* ) /\ C e. RR /\ A e. RR* ) -> ( A. x e. ( F " dom ( F |` ( C [,) +oo ) ) ) x <_ A <-> A. j e. dom ( F |` ( C [,) +oo ) ) ( F ` j ) <_ A ) )
29 23 eleq2d 
 |-  ( ( ( B C_ RR /\ F : B --> RR* ) /\ C e. RR /\ A e. RR* ) -> ( j e. dom ( F |` ( C [,) +oo ) ) <-> j e. ( B i^i ( C [,) +oo ) ) ) )
30 elin 
 |-  ( j e. ( B i^i ( C [,) +oo ) ) <-> ( j e. B /\ j e. ( C [,) +oo ) ) )
31 29 30 bitrdi 
 |-  ( ( ( B C_ RR /\ F : B --> RR* ) /\ C e. RR /\ A e. RR* ) -> ( j e. dom ( F |` ( C [,) +oo ) ) <-> ( j e. B /\ j e. ( C [,) +oo ) ) ) )
32 simpl2 
 |-  ( ( ( ( B C_ RR /\ F : B --> RR* ) /\ C e. RR /\ A e. RR* ) /\ j e. B ) -> C e. RR )
33 simp1l 
 |-  ( ( ( B C_ RR /\ F : B --> RR* ) /\ C e. RR /\ A e. RR* ) -> B C_ RR )
34 33 sselda 
 |-  ( ( ( ( B C_ RR /\ F : B --> RR* ) /\ C e. RR /\ A e. RR* ) /\ j e. B ) -> j e. RR )
35 elicopnf 
 |-  ( C e. RR -> ( j e. ( C [,) +oo ) <-> ( j e. RR /\ C <_ j ) ) )
36 35 baibd 
 |-  ( ( C e. RR /\ j e. RR ) -> ( j e. ( C [,) +oo ) <-> C <_ j ) )
37 32 34 36 syl2anc 
 |-  ( ( ( ( B C_ RR /\ F : B --> RR* ) /\ C e. RR /\ A e. RR* ) /\ j e. B ) -> ( j e. ( C [,) +oo ) <-> C <_ j ) )
38 37 pm5.32da 
 |-  ( ( ( B C_ RR /\ F : B --> RR* ) /\ C e. RR /\ A e. RR* ) -> ( ( j e. B /\ j e. ( C [,) +oo ) ) <-> ( j e. B /\ C <_ j ) ) )
39 31 38 bitrd 
 |-  ( ( ( B C_ RR /\ F : B --> RR* ) /\ C e. RR /\ A e. RR* ) -> ( j e. dom ( F |` ( C [,) +oo ) ) <-> ( j e. B /\ C <_ j ) ) )
40 39 imbi1d 
 |-  ( ( ( B C_ RR /\ F : B --> RR* ) /\ C e. RR /\ A e. RR* ) -> ( ( j e. dom ( F |` ( C [,) +oo ) ) -> ( F ` j ) <_ A ) <-> ( ( j e. B /\ C <_ j ) -> ( F ` j ) <_ A ) ) )
41 impexp 
 |-  ( ( ( j e. B /\ C <_ j ) -> ( F ` j ) <_ A ) <-> ( j e. B -> ( C <_ j -> ( F ` j ) <_ A ) ) )
42 40 41 bitrdi 
 |-  ( ( ( B C_ RR /\ F : B --> RR* ) /\ C e. RR /\ A e. RR* ) -> ( ( j e. dom ( F |` ( C [,) +oo ) ) -> ( F ` j ) <_ A ) <-> ( j e. B -> ( C <_ j -> ( F ` j ) <_ A ) ) ) )
43 42 ralbidv2 
 |-  ( ( ( B C_ RR /\ F : B --> RR* ) /\ C e. RR /\ A e. RR* ) -> ( A. j e. dom ( F |` ( C [,) +oo ) ) ( F ` j ) <_ A <-> A. j e. B ( C <_ j -> ( F ` j ) <_ A ) ) )
44 17 28 43 3bitrd 
 |-  ( ( ( B C_ RR /\ F : B --> RR* ) /\ C e. RR /\ A e. RR* ) -> ( A. x e. ( ( F " ( C [,) +oo ) ) i^i RR* ) x <_ A <-> A. j e. B ( C <_ j -> ( F ` j ) <_ A ) ) )
45 4 8 44 3bitrd 
 |-  ( ( ( B C_ RR /\ F : B --> RR* ) /\ C e. RR /\ A e. RR* ) -> ( ( G ` C ) <_ A <-> A. j e. B ( C <_ j -> ( F ` j ) <_ A ) ) )