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

Metamath Proof Explorer

Theorem o1res

Description: The restriction of an eventually bounded function is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014) (Proof shortened by Mario Carneiro, 26-May-2016)

Ref Expression
Assertion o1res 
|- ( F e. O(1) -> ( F |` A ) e. O(1) )

Proof

Step Hyp Ref Expression
1 resco 
 |-  ( ( abs o. F ) |` A ) = ( abs o. ( F |` A ) )
2 o1f 
 |-  ( F e. O(1) -> F : dom F --> CC )
3 lo1o1 
 |-  ( F : dom F --> CC -> ( F e. O(1) <-> ( abs o. F ) e. <_O(1) ) )
4 2 3 syl 
 |-  ( F e. O(1) -> ( F e. O(1) <-> ( abs o. F ) e. <_O(1) ) )
5 4 ibi 
 |-  ( F e. O(1) -> ( abs o. F ) e. <_O(1) )
6 lo1res 
 |-  ( ( abs o. F ) e. <_O(1) -> ( ( abs o. F ) |` A ) e. <_O(1) )
7 5 6 syl 
 |-  ( F e. O(1) -> ( ( abs o. F ) |` A ) e. <_O(1) )
8 1 7 eqeltrrid 
 |-  ( F e. O(1) -> ( abs o. ( F |` A ) ) e. <_O(1) )
9 fresin 
 |-  ( F : dom F --> CC -> ( F |` A ) : ( dom F i^i A ) --> CC )
10 lo1o1 
 |-  ( ( F |` A ) : ( dom F i^i A ) --> CC -> ( ( F |` A ) e. O(1) <-> ( abs o. ( F |` A ) ) e. <_O(1) ) )
11 2 9 10 3syl 
 |-  ( F e. O(1) -> ( ( F |` A ) e. O(1) <-> ( abs o. ( F |` A ) ) e. <_O(1) ) )
12 8 11 mpbird 
 |-  ( F e. O(1) -> ( F |` A ) e. O(1) )