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) )