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 >. )