Metamath Proof Explorer


Theorem o1res2

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

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

Proof

Step Hyp Ref Expression
1 rlimres2.1
 |-  ( ph -> A C_ B )
2 o1res2.2
 |-  ( ph -> ( x e. B |-> C ) e. O(1) )
3 1 resmptd
 |-  ( ph -> ( ( x e. B |-> C ) |` A ) = ( x e. A |-> C ) )
4 o1res
 |-  ( ( 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) )