Metamath Proof Explorer


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 φAB
lo1res2.2 φxBC𝑂1
Assertion lo1res2 φxAC𝑂1

Proof

Step Hyp Ref Expression
1 rlimres2.1 φAB
2 lo1res2.2 φxBC𝑂1
3 1 resmptd φxBCA=xAC
4 lo1res xBC𝑂1xBCA𝑂1
5 2 4 syl φxBCA𝑂1
6 3 5 eqeltrrd φxAC𝑂1