Theorem lo1res2

Description: The restriction of a function is eventually bounded if the original is. (Contributed by Mario Carneiro, 26-May-2016)

	Ref	Expression
Hypotheses	rlimres2.1	|- ( ph -> A C_ B )
	lo1res2.2	|- ( ph -> ( x e. B |-> C ) e. <_O(1) )
Assertion	lo1res2	|- ( ph -> ( x e. A |-> C ) e. <_O(1) )

Proof

Step	Hyp	Ref	Expression
1		rlimres2.1	|- ( ph -> A C_ B )
2		lo1res2.2	|- ( ph -> ( x e. B |-> C ) e. <_O(1) )
3	1	resmptd	|- ( ph -> ( ( x e. B |-> C ) |` A ) = ( x e. A |-> C ) )
4		lo1res	|- ( ( x e. B |-> C ) e. <_O(1) -> ( ( x e. B |-> C ) |` A ) e. <_O(1) )
5	2 4	syl	|- ( ph -> ( ( x e. B |-> C ) |` A ) e. <_O(1) )
6	3 5	eqeltrrd	|- ( ph -> ( x e. A |-> C ) e. <_O(1) )