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