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

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		simprr	|- ( ( ph /\ ( x = X /\ y = Y ) ) -> y = Y )
5		simprl	|- ( ( ph /\ ( x = X /\ y = Y ) ) -> x = X )
6	4 5	oveq12d	|- ( ( ph /\ ( x = X /\ y = Y ) ) -> ( y N x ) = ( Y N X ) )
7	6	reseq2d	|- ( ( ph /\ ( x = X /\ y = Y ) ) -> ( _I |` ( y N x ) ) = ( _I |` ( Y N X ) ) )
8		ovexd	|- ( ph -> ( Y N X ) e. _V )
9		resiexg	|- ( ( Y N X ) e. _V -> ( _I |` ( Y N X ) ) e. _V )
10	8 9	syl	|- ( ph -> ( _I |` ( Y N X ) ) e. _V )
11	1 7 2 3 10	ovmpod	|- ( ph -> ( X F Y ) = ( _I |` ( Y N X ) ) )