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	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
	o1res2.2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ 𝑂(1) )
Assertion	o1res2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝑂(1) )

Proof

Step	Hyp	Ref	Expression
1		rlimres2.1	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
2		o1res2.2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ 𝑂(1) )
3	1	resmptd	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ↾ 𝐴 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
4		o1res	⊢ ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ 𝑂(1) → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ↾ 𝐴 ) ∈ 𝑂(1) )
5	2 4	syl	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ↾ 𝐴 ) ∈ 𝑂(1) )
6	3 5	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝑂(1) )