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	|- ( ph -> F = ( x e. A , y e. B |-> ( _I |` ( y N x ) ) ) )
	opf2fval.x	|- ( ph -> X e. A )
	opf2fval.y	|- ( ph -> Y e. B )
	opf2.c	|- ( ph -> C = D )
	opf2.d	|- ( ph -> D e. ( Y N X ) )
Assertion	opf2	|- ( ph -> ( ( X F Y ) ` C ) = D )

Proof

Step	Hyp	Ref	Expression
1		opf2fval.f	|- ( ph -> F = ( x e. A , y e. B |-> ( _I |` ( y N x ) ) ) )
2		opf2fval.x	|- ( ph -> X e. A )
3		opf2fval.y	|- ( ph -> Y e. B )
4		opf2.c	|- ( ph -> C = D )
5		opf2.d	|- ( ph -> D e. ( Y N X ) )
6	1 2 3	opf2fval	|- ( ph -> ( X F Y ) = ( _I |` ( Y N X ) ) )
7	6 4	fveq12d	|- ( ph -> ( ( X F Y ) ` C ) = ( ( _I |` ( Y N X ) ) ` D ) )
8		fvresi	|- ( D e. ( Y N X ) -> ( ( _I |` ( Y N X ) ) ` D ) = D )
9	5 8	syl	|- ( ph -> ( ( _I |` ( Y N X ) ) ` D ) = D )
10	7 9	eqtrd	|- ( ph -> ( ( X F Y ) ` C ) = D )