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 ( 𝜑𝐴𝐵 )
lo1res2.2 ( 𝜑 → ( 𝑥𝐵𝐶 ) ∈ ≤𝑂(1) )
Assertion lo1res2 ( 𝜑 → ( 𝑥𝐴𝐶 ) ∈ ≤𝑂(1) )

Proof

Step Hyp Ref Expression
1 rlimres2.1 ( 𝜑𝐴𝐵 )
2 lo1res2.2 ( 𝜑 → ( 𝑥𝐵𝐶 ) ∈ ≤𝑂(1) )
3 1 resmptd ( 𝜑 → ( ( 𝑥𝐵𝐶 ) ↾ 𝐴 ) = ( 𝑥𝐴𝐶 ) )
4 lo1res ( ( 𝑥𝐵𝐶 ) ∈ ≤𝑂(1) → ( ( 𝑥𝐵𝐶 ) ↾ 𝐴 ) ∈ ≤𝑂(1) )
5 2 4 syl ( 𝜑 → ( ( 𝑥𝐵𝐶 ) ↾ 𝐴 ) ∈ ≤𝑂(1) )
6 3 5 eqeltrrd ( 𝜑 → ( 𝑥𝐴𝐶 ) ∈ ≤𝑂(1) )