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 oppfvalg 
 |-  ( ( F e. _V /\ G e. _V ) -> ( F oppFunc G ) = if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) )
4 2 3 syl 
 |-  ( F ( C Func D ) G -> ( F oppFunc G ) = if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) )
5 oppfvallem 
 |-  ( F ( C Func D ) G -> ( Rel G /\ Rel dom G ) )
6 5 iftrued 
 |-  ( F ( C Func D ) G -> if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) = <. F , tpos G >. )
7 4 6 eqtrd 
 |-  ( F ( C Func D ) G -> ( F oppFunc G ) = <. F , tpos G >. )