Theorem ofresid

Description: Applying an operation restricted to the range of the functions does not change the function operation. (Contributed by Thierry Arnoux, 14-Feb-2018)

	Ref	Expression
Hypotheses	ofresid.1	$$⊢\phi \to F:A⟶B$$
	ofresid.2	$$⊢\phi \to G:A⟶B$$
	ofresid.3	$$⊢\phi \to A\in V$$
Assertion	ofresid	$$⊢\phi \to F{R}_{f}G=F{\left({R\upharpoonright }_{\left(B\times B\right)}\right)}_{f}G$$

Proof

Step	Hyp	Ref	Expression
1		ofresid.1	$$⊢\phi \to F:A⟶B$$
2		ofresid.2	$$⊢\phi \to G:A⟶B$$
3		ofresid.3	$$⊢\phi \to A\in V$$
4	1	ffvelcdmda	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)\in B$$
5	2	ffvelcdmda	$$⊢\left(\phi \wedge x\in A\right)\to G\left(x\right)\in B$$
6	4 5	opelxpd	$$⊢\left(\phi \wedge x\in A\right)\to ⟨F\left(x\right),G\left(x\right)⟩\in \left(B\times B\right)$$
7	6	fvresd	$$⊢\left(\phi \wedge x\in A\right)\to \left({R\upharpoonright }_{\left(B\times B\right)}\right)\left(⟨F\left(x\right),G\left(x\right)⟩\right)=R\left(⟨F\left(x\right),G\left(x\right)⟩\right)$$
8	7	eqcomd	$$⊢\left(\phi \wedge x\in A\right)\to R\left(⟨F\left(x\right),G\left(x\right)⟩\right)=\left({R\upharpoonright }_{\left(B\times B\right)}\right)\left(⟨F\left(x\right),G\left(x\right)⟩\right)$$
9		df-ov	$$⊢F\left(x\right)RG\left(x\right)=R\left(⟨F\left(x\right),G\left(x\right)⟩\right)$$
10		df-ov	$$⊢F\left(x\right)\left({R\upharpoonright }_{\left(B\times B\right)}\right)G\left(x\right)=\left({R\upharpoonright }_{\left(B\times B\right)}\right)\left(⟨F\left(x\right),G\left(x\right)⟩\right)$$
11	8 9 10	3eqtr4g	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)RG\left(x\right)=F\left(x\right)\left({R\upharpoonright }_{\left(B\times B\right)}\right)G\left(x\right)$$
12	11	mpteq2dva	$$⊢\phi \to \left(x\in A⟼F\left(x\right)RG\left(x\right)\right)=\left(x\in A⟼F\left(x\right)\left({R\upharpoonright }_{\left(B\times B\right)}\right)G\left(x\right)\right)$$
13	1	ffnd	$$⊢\phi \to FFnA$$
14	2	ffnd	$$⊢\phi \to GFnA$$
15		inidm	$$⊢A\cap A=A$$
16		eqidd	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)=F\left(x\right)$$
17		eqidd	$$⊢\left(\phi \wedge x\in A\right)\to G\left(x\right)=G\left(x\right)$$
18	13 14 3 3 15 16 17	offval	$$⊢\phi \to F{R}_{f}G=\left(x\in A⟼F\left(x\right)RG\left(x\right)\right)$$
19	13 14 3 3 15 16 17	offval	$$⊢\phi \to F{\left({R\upharpoonright }_{\left(B\times B\right)}\right)}_{f}G=\left(x\in A⟼F\left(x\right)\left({R\upharpoonright }_{\left(B\times B\right)}\right)G\left(x\right)\right)$$
20	12 18 19	3eqtr4d	$$⊢\phi \to F{R}_{f}G=F{\left({R\upharpoonright }_{\left(B\times B\right)}\right)}_{f}G$$