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	$$⊢\phi \to A\subseteq B$$
	o1res2.2	$$⊢\phi \to \left(x\in B⟼C\right)\in 𝑂\left(1\right)$$
Assertion	o1res2	$$⊢\phi \to \left(x\in A⟼C\right)\in 𝑂\left(1\right)$$

Proof

Step	Hyp	Ref	Expression
1		rlimres2.1	$$⊢\phi \to A\subseteq B$$
2		o1res2.2	$$⊢\phi \to \left(x\in B⟼C\right)\in 𝑂\left(1\right)$$
3	1	resmptd	$$⊢\phi \to {\left(x\in B⟼C\right)\upharpoonright }_A=\left(x\in A⟼C\right)$$
4		o1res	$$⊢\left(x\in B⟼C\right)\in 𝑂\left(1\right)\to {\left(x\in B⟼C\right)\upharpoonright }_A\in 𝑂\left(1\right)$$
5	2 4	syl	$$⊢\phi \to {\left(x\in B⟼C\right)\upharpoonright }_A\in 𝑂\left(1\right)$$
6	3 5	eqeltrrd	$$⊢\phi \to \left(x\in A⟼C\right)\in 𝑂\left(1\right)$$