Metamath Proof Explorer

Theorem lo1resb

Description: The restriction of a function to an unbounded-above interval is eventually upper bounded iff the original is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Hypotheses lo1resb.1 
|- ( ph -> F : A --> RR )
lo1resb.2 
|- ( ph -> A C_ RR )
lo1resb.3 
|- ( ph -> B e. RR )
Assertion lo1resb 
|- ( ph -> ( F e. <_O(1) <-> ( F |` ( B [,) +oo ) ) e. <_O(1) ) )

Proof

Step Hyp Ref Expression
1 lo1resb.1 
 |-  ( ph -> F : A --> RR )
2 lo1resb.2 
 |-  ( ph -> A C_ RR )
3 lo1resb.3 
 |-  ( ph -> B e. RR )
4 lo1res 
 |-  ( F e. <_O(1) -> ( F |` ( B [,) +oo ) ) e. <_O(1) )
5 1 feqmptd 
 |-  ( ph -> F = ( x e. A |-> ( F ` x ) ) )
6 5 reseq1d 
 |-  ( ph -> ( F |` ( B [,) +oo ) ) = ( ( x e. A |-> ( F ` x ) ) |` ( B [,) +oo ) ) )
7 resmpt3 
 |-  ( ( x e. A |-> ( F ` x ) ) |` ( B [,) +oo ) ) = ( x e. ( A i^i ( B [,) +oo ) ) |-> ( F ` x ) )
8 6 7 eqtrdi 
 |-  ( ph -> ( F |` ( B [,) +oo ) ) = ( x e. ( A i^i ( B [,) +oo ) ) |-> ( F ` x ) ) )
9 8 eleq1d 
 |-  ( ph -> ( ( F |` ( B [,) +oo ) ) e. <_O(1) <-> ( x e. ( A i^i ( B [,) +oo ) ) |-> ( F ` x ) ) e. <_O(1) ) )
10 inss1 
 |-  ( A i^i ( B [,) +oo ) ) C_ A
11 10 2 sstrid 
 |-  ( ph -> ( A i^i ( B [,) +oo ) ) C_ RR )
12 elinel1 
 |-  ( x e. ( A i^i ( B [,) +oo ) ) -> x e. A )
13 ffvelcdm 
 |-  ( ( F : A --> RR /\ x e. A ) -> ( F ` x ) e. RR )
14 1 12 13 syl2an 
 |-  ( ( ph /\ x e. ( A i^i ( B [,) +oo ) ) ) -> ( F ` x ) e. RR )
15 11 14 ello1mpt 
 |-  ( ph -> ( ( x e. ( A i^i ( B [,) +oo ) ) |-> ( F ` x ) ) e. <_O(1) <-> E. y e. RR E. z e. RR A. x e. ( A i^i ( B [,) +oo ) ) ( y <_ x -> ( F ` x ) <_ z ) ) )
16 elin 
 |-  ( x e. ( A i^i ( B [,) +oo ) ) <-> ( x e. A /\ x e. ( B [,) +oo ) ) )
17 16 imbi1i 
 |-  ( ( x e. ( A i^i ( B [,) +oo ) ) -> ( y <_ x -> ( F ` x ) <_ z ) ) <-> ( ( x e. A /\ x e. ( B [,) +oo ) ) -> ( y <_ x -> ( F ` x ) <_ z ) ) )
18 impexp 
 |-  ( ( ( x e. A /\ x e. ( B [,) +oo ) ) -> ( y <_ x -> ( F ` x ) <_ z ) ) <-> ( x e. A -> ( x e. ( B [,) +oo ) -> ( y <_ x -> ( F ` x ) <_ z ) ) ) )
19 17 18 bitri 
 |-  ( ( x e. ( A i^i ( B [,) +oo ) ) -> ( y <_ x -> ( F ` x ) <_ z ) ) <-> ( x e. A -> ( x e. ( B [,) +oo ) -> ( y <_ x -> ( F ` x ) <_ z ) ) ) )
20 impexp 
 |-  ( ( ( x e. ( B [,) +oo ) /\ y <_ x ) -> ( F ` x ) <_ z ) <-> ( x e. ( B [,) +oo ) -> ( y <_ x -> ( F ` x ) <_ z ) ) )
21 3 ad2antrr 
 |-  ( ( ( ph /\ ( y e. RR /\ z e. RR ) ) /\ x e. A ) -> B e. RR )
22 2 adantr 
 |-  ( ( ph /\ ( y e. RR /\ z e. RR ) ) -> A C_ RR )
23 22 sselda 
 |-  ( ( ( ph /\ ( y e. RR /\ z e. RR ) ) /\ x e. A ) -> x e. RR )
24 elicopnf 
 |-  ( B e. RR -> ( x e. ( B [,) +oo ) <-> ( x e. RR /\ B <_ x ) ) )
25 24 baibd 
 |-  ( ( B e. RR /\ x e. RR ) -> ( x e. ( B [,) +oo ) <-> B <_ x ) )
26 21 23 25 syl2anc 
 |-  ( ( ( ph /\ ( y e. RR /\ z e. RR ) ) /\ x e. A ) -> ( x e. ( B [,) +oo ) <-> B <_ x ) )
27 26 anbi1d 
 |-  ( ( ( ph /\ ( y e. RR /\ z e. RR ) ) /\ x e. A ) -> ( ( x e. ( B [,) +oo ) /\ y <_ x ) <-> ( B <_ x /\ y <_ x ) ) )
28 simplrl 
 |-  ( ( ( ph /\ ( y e. RR /\ z e. RR ) ) /\ x e. A ) -> y e. RR )
29 maxle 
 |-  ( ( B e. RR /\ y e. RR /\ x e. RR ) -> ( if ( B <_ y , y , B ) <_ x <-> ( B <_ x /\ y <_ x ) ) )
30 21 28 23 29 syl3anc 
 |-  ( ( ( ph /\ ( y e. RR /\ z e. RR ) ) /\ x e. A ) -> ( if ( B <_ y , y , B ) <_ x <-> ( B <_ x /\ y <_ x ) ) )
31 27 30 bitr4d 
 |-  ( ( ( ph /\ ( y e. RR /\ z e. RR ) ) /\ x e. A ) -> ( ( x e. ( B [,) +oo ) /\ y <_ x ) <-> if ( B <_ y , y , B ) <_ x ) )
32 31 imbi1d 
 |-  ( ( ( ph /\ ( y e. RR /\ z e. RR ) ) /\ x e. A ) -> ( ( ( x e. ( B [,) +oo ) /\ y <_ x ) -> ( F ` x ) <_ z ) <-> ( if ( B <_ y , y , B ) <_ x -> ( F ` x ) <_ z ) ) )
33 20 32 bitr3id 
 |-  ( ( ( ph /\ ( y e. RR /\ z e. RR ) ) /\ x e. A ) -> ( ( x e. ( B [,) +oo ) -> ( y <_ x -> ( F ` x ) <_ z ) ) <-> ( if ( B <_ y , y , B ) <_ x -> ( F ` x ) <_ z ) ) )
34 33 pm5.74da 
 |-  ( ( ph /\ ( y e. RR /\ z e. RR ) ) -> ( ( x e. A -> ( x e. ( B [,) +oo ) -> ( y <_ x -> ( F ` x ) <_ z ) ) ) <-> ( x e. A -> ( if ( B <_ y , y , B ) <_ x -> ( F ` x ) <_ z ) ) ) )
35 19 34 bitrid 
 |-  ( ( ph /\ ( y e. RR /\ z e. RR ) ) -> ( ( x e. ( A i^i ( B [,) +oo ) ) -> ( y <_ x -> ( F ` x ) <_ z ) ) <-> ( x e. A -> ( if ( B <_ y , y , B ) <_ x -> ( F ` x ) <_ z ) ) ) )
36 35 ralbidv2 
 |-  ( ( ph /\ ( y e. RR /\ z e. RR ) ) -> ( A. x e. ( A i^i ( B [,) +oo ) ) ( y <_ x -> ( F ` x ) <_ z ) <-> A. x e. A ( if ( B <_ y , y , B ) <_ x -> ( F ` x ) <_ z ) ) )
37 1 adantr 
 |-  ( ( ph /\ ( y e. RR /\ z e. RR ) ) -> F : A --> RR )
38 simprl 
 |-  ( ( ph /\ ( y e. RR /\ z e. RR ) ) -> y e. RR )
39 3 adantr 
 |-  ( ( ph /\ ( y e. RR /\ z e. RR ) ) -> B e. RR )
40 38 39 ifcld 
 |-  ( ( ph /\ ( y e. RR /\ z e. RR ) ) -> if ( B <_ y , y , B ) e. RR )
41 simprr 
 |-  ( ( ph /\ ( y e. RR /\ z e. RR ) ) -> z e. RR )
42 ello12r 
 |-  ( ( ( F : A --> RR /\ A C_ RR ) /\ ( if ( B <_ y , y , B ) e. RR /\ z e. RR ) /\ A. x e. A ( if ( B <_ y , y , B ) <_ x -> ( F ` x ) <_ z ) ) -> F e. <_O(1) )
43 42 3expia 
 |-  ( ( ( F : A --> RR /\ A C_ RR ) /\ ( if ( B <_ y , y , B ) e. RR /\ z e. RR ) ) -> ( A. x e. A ( if ( B <_ y , y , B ) <_ x -> ( F ` x ) <_ z ) -> F e. <_O(1) ) )
44 37 22 40 41 43 syl22anc 
 |-  ( ( ph /\ ( y e. RR /\ z e. RR ) ) -> ( A. x e. A ( if ( B <_ y , y , B ) <_ x -> ( F ` x ) <_ z ) -> F e. <_O(1) ) )
45 36 44 sylbid 
 |-  ( ( ph /\ ( y e. RR /\ z e. RR ) ) -> ( A. x e. ( A i^i ( B [,) +oo ) ) ( y <_ x -> ( F ` x ) <_ z ) -> F e. <_O(1) ) )
46 45 rexlimdvva 
 |-  ( ph -> ( E. y e. RR E. z e. RR A. x e. ( A i^i ( B [,) +oo ) ) ( y <_ x -> ( F ` x ) <_ z ) -> F e. <_O(1) ) )
47 15 46 sylbid 
 |-  ( ph -> ( ( x e. ( A i^i ( B [,) +oo ) ) |-> ( F ` x ) ) e. <_O(1) -> F e. <_O(1) ) )
48 9 47 sylbid 
 |-  ( ph -> ( ( F |` ( B [,) +oo ) ) e. <_O(1) -> F e. <_O(1) ) )
49 4 48 impbid2 
 |-  ( ph -> ( F e. <_O(1) <-> ( F |` ( B [,) +oo ) ) e. <_O(1) ) )