Metamath Proof Explorer

Theorem oppfval

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

Ref Expression
Assertion oppfval 
|- ( F ( C Func D ) G -> ( F oppFunc G ) = <. F , tpos G >. )

Proof

Step Hyp Ref Expression
1 relfunc 
 |-  Rel ( C Func D )
2 1 brrelex12i 
 |-  ( F ( C Func D ) G -> ( F e. _V /\ G e. _V ) )
3 simpl 
 |-  ( ( f = F /\ g = G ) -> f = F )
4 simpr 
 |-  ( ( f = F /\ g = G ) -> g = G )
5 4 tposeqd 
 |-  ( ( f = F /\ g = G ) -> tpos g = tpos G )
6 3 5 opeq12d 
 |-  ( ( f = F /\ g = G ) -> <. f , tpos g >. = <. F , tpos G >. )
7 df-oppf 
 |-  oppFunc = ( f e. _V , g e. _V |-> <. f , tpos g >. )
8 opex 
 |-  <. F , tpos G >. e. _V
9 6 7 8 ovmpoa 
 |-  ( ( F e. _V /\ G e. _V ) -> ( F oppFunc G ) = <. F , tpos G >. )
10 2 9 syl 
 |-  ( F ( C Func D ) G -> ( F oppFunc G ) = <. F , tpos G >. )