Metamath Proof Explorer

Theorem opf12

Description: The object part of the op functor on functor categories. Lemma for oppfdiag . (Contributed by Zhi Wang, 19-Nov-2025)

Ref Expression
Hypotheses opf11.f 
|- ( ph -> F = ( oppFunc |` ( C Func D ) ) )
opf11.x 
|- ( ph -> X e. ( C Func D ) )
Assertion opf12 
|- ( ph -> ( M ( 2nd ` ( F ` X ) ) N ) = ( N ( 2nd ` X ) M ) )

Proof

Step Hyp Ref Expression
1 opf11.f 
 |-  ( ph -> F = ( oppFunc |` ( C Func D ) ) )
2 opf11.x 
 |-  ( ph -> X e. ( C Func D ) )
3 1 fveq1d 
 |-  ( ph -> ( F ` X ) = ( ( oppFunc |` ( C Func D ) ) ` X ) )
4 2 fvresd 
 |-  ( ph -> ( ( oppFunc |` ( C Func D ) ) ` X ) = ( oppFunc ` X ) )
5 oppfval2 
 |-  ( X e. ( C Func D ) -> ( oppFunc ` X ) = <. ( 1st ` X ) , tpos ( 2nd ` X ) >. )
6 2 5 syl 
 |-  ( ph -> ( oppFunc ` X ) = <. ( 1st ` X ) , tpos ( 2nd ` X ) >. )
7 3 4 6 3eqtrd 
 |-  ( ph -> ( F ` X ) = <. ( 1st ` X ) , tpos ( 2nd ` X ) >. )
8 fvex 
 |-  ( 1st ` X ) e. _V
9 fvex 
 |-  ( 2nd ` X ) e. _V
10 9 tposex 
 |-  tpos ( 2nd ` X ) e. _V
11 8 10 op2ndd 
 |-  ( ( F ` X ) = <. ( 1st ` X ) , tpos ( 2nd ` X ) >. -> ( 2nd ` ( F ` X ) ) = tpos ( 2nd ` X ) )
12 7 11 syl 
 |-  ( ph -> ( 2nd ` ( F ` X ) ) = tpos ( 2nd ` X ) )
13 12 oveqd 
 |-  ( ph -> ( M ( 2nd ` ( F ` X ) ) N ) = ( M tpos ( 2nd ` X ) N ) )
14 ovtpos 
 |-  ( M tpos ( 2nd ` X ) N ) = ( N ( 2nd ` X ) M )
15 13 14 eqtrdi 
 |-  ( ph -> ( M ( 2nd ` ( F ` X ) ) N ) = ( N ( 2nd ` X ) M ) )