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

Metamath Proof Explorer

Theorem oppfval3

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

Ref Expression
Hypotheses oppfval3.g 
|- ( ph -> F = <. G , K >. )
oppfval3.f 
|- ( ph -> F e. ( C Func D ) )
Assertion oppfval3 
|- ( ph -> ( oppFunc ` F ) = <. G , tpos K >. )

Proof

Step Hyp Ref Expression
1 oppfval3.g 
 |-  ( ph -> F = <. G , K >. )
2 oppfval3.f 
 |-  ( ph -> F e. ( C Func D ) )
3 1 fveq2d 
 |-  ( ph -> ( oppFunc ` F ) = ( oppFunc ` <. G , K >. ) )
4 df-ov 
 |-  ( G oppFunc K ) = ( oppFunc ` <. G , K >. )
5 3 4 eqtr4di 
 |-  ( ph -> ( oppFunc ` F ) = ( G oppFunc K ) )
6 1 2 eqeltrrd 
 |-  ( ph -> <. G , K >. e. ( C Func D ) )
7 df-br 
 |-  ( G ( C Func D ) K <-> <. G , K >. e. ( C Func D ) )
8 6 7 sylibr 
 |-  ( ph -> G ( C Func D ) K )
9 oppfval 
 |-  ( G ( C Func D ) K -> ( G oppFunc K ) = <. G , tpos K >. )
10 8 9 syl 
 |-  ( ph -> ( G oppFunc K ) = <. G , tpos K >. )
11 5 10 eqtrd 
 |-  ( ph -> ( oppFunc ` F ) = <. G , tpos K >. )