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

Metamath Proof Explorer

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 ) ) )