Theorem oprres

Description: The restriction of an operation is an operation. (Contributed by NM, 1-Feb-2008) (Revised by AV, 19-Oct-2021)

	Ref	Expression
Hypotheses	oprres.v	$$⊢\left(\phi \wedge x\in Y\wedge y\in Y\right)\to xFy=xGy$$
	oprres.s	$$⊢\phi \to Y\subseteq X$$
	oprres.f	$$⊢\phi \to F:Y\times Y⟶R$$
	oprres.g	$$⊢\phi \to G:X\times X⟶S$$
Assertion	oprres	$$⊢\phi \to F={G\upharpoonright }_{\left(Y\times Y\right)}$$

Proof

Step	Hyp	Ref	Expression
1		oprres.v	$$⊢\left(\phi \wedge x\in Y\wedge y\in Y\right)\to xFy=xGy$$
2		oprres.s	$$⊢\phi \to Y\subseteq X$$
3		oprres.f	$$⊢\phi \to F:Y\times Y⟶R$$
4		oprres.g	$$⊢\phi \to G:X\times X⟶S$$
5	1	3expb	$$⊢\left(\phi \wedge \left(x\in Y\wedge y\in Y\right)\right)\to xFy=xGy$$
6		ovres	$$⊢\left(x\in Y\wedge y\in Y\right)\to x\left({G\upharpoonright }_{\left(Y\times Y\right)}\right)y=xGy$$
7	6	adantl	$$⊢\left(\phi \wedge \left(x\in Y\wedge y\in Y\right)\right)\to x\left({G\upharpoonright }_{\left(Y\times Y\right)}\right)y=xGy$$
8	5 7	eqtr4d	$$⊢\left(\phi \wedge \left(x\in Y\wedge y\in Y\right)\right)\to xFy=x\left({G\upharpoonright }_{\left(Y\times Y\right)}\right)y$$
9	8	ralrimivva	$$⊢\phi \to \forall x\in Y\forall y\in YxFy=x\left({G\upharpoonright }_{\left(Y\times Y\right)}\right)y$$
10		eqid	$$⊢Y\times Y=Y\times Y$$
11	9 10	jctil	$$⊢\phi \to \left(Y\times Y=Y\times Y\wedge \forall x\in Y\forall y\in YxFy=x\left({G\upharpoonright }_{\left(Y\times Y\right)}\right)y\right)$$
12	3	ffnd	$$⊢\phi \to FFn\left(Y\times Y\right)$$
13	4	ffnd	$$⊢\phi \to GFn\left(X\times X\right)$$
14		xpss12	$$⊢\left(Y\subseteq X\wedge Y\subseteq X\right)\to Y\times Y\subseteq X\times X$$
15	2 2 14	syl2anc	$$⊢\phi \to Y\times Y\subseteq X\times X$$
16		fnssres	$$⊢\left(GFn\left(X\times X\right)\wedge Y\times Y\subseteq X\times X\right)\to \left({G\upharpoonright }_{\left(Y\times Y\right)}\right)Fn\left(Y\times Y\right)$$
17	13 15 16	syl2anc	$$⊢\phi \to \left({G\upharpoonright }_{\left(Y\times Y\right)}\right)Fn\left(Y\times Y\right)$$
18		eqfnov	$$⊢\left(FFn\left(Y\times Y\right)\wedge \left({G\upharpoonright }_{\left(Y\times Y\right)}\right)Fn\left(Y\times Y\right)\right)\to \left(F={G\upharpoonright }_{\left(Y\times Y\right)}\leftrightarrow \left(Y\times Y=Y\times Y\wedge \forall x\in Y\forall y\in YxFy=x\left({G\upharpoonright }_{\left(Y\times Y\right)}\right)y\right)\right)$$
19	12 17 18	syl2anc	$$⊢\phi \to \left(F={G\upharpoonright }_{\left(Y\times Y\right)}\leftrightarrow \left(Y\times Y=Y\times Y\wedge \forall x\in Y\forall y\in YxFy=x\left({G\upharpoonright }_{\left(Y\times Y\right)}\right)y\right)\right)$$
20	11 19	mpbird	$$⊢\phi \to F={G\upharpoonright }_{\left(Y\times Y\right)}$$