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 ffvelrn
 |-  ( ( 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 syl5bb
 |-  ( ( 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) ) )