Theorem opf2

Description: The morphism part of the op functor on functor categories. Lemma for fucoppc . (Contributed by Zhi Wang, 18-Nov-2025)

	Ref	Expression
Hypotheses	opf2fval.f	$$⊢\phi \to F=\left(x\in A,y\in B⟼{\mathrm{I}\upharpoonright }_{\left(yNx\right)}\right)$$
	opf2fval.x	$$⊢\phi \to X\in A$$
	opf2fval.y	$$⊢\phi \to Y\in B$$
	opf2.c	$$⊢\phi \to C=D$$
	opf2.d	$$⊢\phi \to D\in \left(YNX\right)$$
Assertion	opf2	$$⊢\phi \to \left(XFY\right)\left(C\right)=D$$

Proof

Step	Hyp	Ref	Expression
1		opf2fval.f	$$⊢\phi \to F=\left(x\in A,y\in B⟼{\mathrm{I}\upharpoonright }_{\left(yNx\right)}\right)$$
2		opf2fval.x	$$⊢\phi \to X\in A$$
3		opf2fval.y	$$⊢\phi \to Y\in B$$
4		opf2.c	$$⊢\phi \to C=D$$
5		opf2.d	$$⊢\phi \to D\in \left(YNX\right)$$
6	1 2 3	opf2fval	$$⊢\phi \to XFY={\mathrm{I}\upharpoonright }_{\left(YNX\right)}$$
7	6 4	fveq12d	$$⊢\phi \to \left(XFY\right)\left(C\right)=\left({\mathrm{I}\upharpoonright }_{\left(YNX\right)}\right)\left(D\right)$$
8		fvresi	$$⊢D\in \left(YNX\right)\to \left({\mathrm{I}\upharpoonright }_{\left(YNX\right)}\right)\left(D\right)=D$$
9	5 8	syl	$$⊢\phi \to \left({\mathrm{I}\upharpoonright }_{\left(YNX\right)}\right)\left(D\right)=D$$
10	7 9	eqtrd	$$⊢\phi \to \left(XFY\right)\left(C\right)=D$$