Theorem opf2fval

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$$
Assertion	opf2fval	$$⊢\phi \to XFY={\mathrm{I}\upharpoonright }_{\left(YNX\right)}$$

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		simprr	$$⊢\left(\phi \wedge \left(x=X\wedge y=Y\right)\right)\to y=Y$$
5		simprl	$$⊢\left(\phi \wedge \left(x=X\wedge y=Y\right)\right)\to x=X$$
6	4 5	oveq12d	$$⊢\left(\phi \wedge \left(x=X\wedge y=Y\right)\right)\to yNx=YNX$$
7	6	reseq2d	$$⊢\left(\phi \wedge \left(x=X\wedge y=Y\right)\right)\to {\mathrm{I}\upharpoonright }_{\left(yNx\right)}={\mathrm{I}\upharpoonright }_{\left(YNX\right)}$$
8		ovexd	$$⊢\phi \to YNX\in \mathrm{V}$$
9		resiexg	$$⊢YNX\in \mathrm{V}\to {\mathrm{I}\upharpoonright }_{\left(YNX\right)}\in \mathrm{V}$$
10	8 9	syl	$$⊢\phi \to {\mathrm{I}\upharpoonright }_{\left(YNX\right)}\in \mathrm{V}$$
11	1 7 2 3 10	ovmpod	$$⊢\phi \to XFY={\mathrm{I}\upharpoonright }_{\left(YNX\right)}$$