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

Metamath Proof Explorer

Theorem oppfval2

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

Ref Expression
Assertion oppfval2 
|- ( F e. ( C Func D ) -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. )

Proof

Step Hyp Ref Expression
1 relfunc 
 |-  Rel ( C Func D )
2 1st2nd 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
3 1 2 mpan 
 |-  ( F e. ( C Func D ) -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
4 3 fveq2d 
 |-  ( F e. ( C Func D ) -> ( oppFunc ` F ) = ( oppFunc ` <. ( 1st ` F ) , ( 2nd ` F ) >. ) )
5 df-ov 
 |-  ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) = ( oppFunc ` <. ( 1st ` F ) , ( 2nd ` F ) >. )
6 4 5 eqtr4di 
 |-  ( F e. ( C Func D ) -> ( oppFunc ` F ) = ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) )
7 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
8 1 7 mpan 
 |-  ( F e. ( C Func D ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
9 oppfval 
 |-  ( ( 1st ` F ) ( C Func D ) ( 2nd ` F ) -> ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. )
10 8 9 syl 
 |-  ( F e. ( C Func D ) -> ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. )
11 6 10 eqtrd 
 |-  ( F e. ( C Func D ) -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. )