This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )