Metamath Proof Explorer

Theorem oppf2

Description: Value of the morphism part of the opposite functor. (Contributed by Zhi Wang, 19-Nov-2025)

Ref Expression
Hypothesis oppf1.f 
|- ( ph -> F e. ( C Func D ) )
Assertion oppf2 
|- ( ph -> ( M ( 2nd ` ( oppFunc ` F ) ) N ) = ( N ( 2nd ` F ) M ) )

Proof

Step Hyp Ref Expression
1 oppf1.f 
 |-  ( ph -> F e. ( C Func D ) )
2 oppfval2 
 |-  ( F e. ( C Func D ) -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. )
3 fvex 
 |-  ( 1st ` F ) e. _V
4 fvex 
 |-  ( 2nd ` F ) e. _V
5 4 tposex 
 |-  tpos ( 2nd ` F ) e. _V
6 3 5 op2ndd 
 |-  ( ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. -> ( 2nd ` ( oppFunc ` F ) ) = tpos ( 2nd ` F ) )
7 1 2 6 3syl 
 |-  ( ph -> ( 2nd ` ( oppFunc ` F ) ) = tpos ( 2nd ` F ) )
8 7 oveqd 
 |-  ( ph -> ( M ( 2nd ` ( oppFunc ` F ) ) N ) = ( M tpos ( 2nd ` F ) N ) )
9 ovtpos 
 |-  ( M tpos ( 2nd ` F ) N ) = ( N ( 2nd ` F ) M )
10 8 9 eqtrdi 
 |-  ( ph -> ( M ( 2nd ` ( oppFunc ` F ) ) N ) = ( N ( 2nd ` F ) M ) )