Theorem oppfval3

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

	Ref	Expression
Hypotheses	oppfval3.g	$$⊢\phi \to F=⟨G,K⟩$$
	oppfval3.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
Assertion	oppfval3	Could not format assertion : No typesetting found for |- ( ph -> ( oppFunc ` F ) = <. G , tpos K >. ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		oppfval3.g	$$⊢\phi \to F=⟨G,K⟩$$
2		oppfval3.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
3	1	fveq2d	Could not format ( ph -> ( oppFunc ` F ) = ( oppFunc ` <. G , K >. ) ) : No typesetting found for |- ( ph -> ( oppFunc ` F ) = ( oppFunc ` <. G , K >. ) ) with typecode |-
4		df-ov	Could not format ( G oppFunc K ) = ( oppFunc ` <. G , K >. ) : No typesetting found for |- ( G oppFunc K ) = ( oppFunc ` <. G , K >. ) with typecode |-
5	3 4	eqtr4di	Could not format ( ph -> ( oppFunc ` F ) = ( G oppFunc K ) ) : No typesetting found for |- ( ph -> ( oppFunc ` F ) = ( G oppFunc K ) ) with typecode |-
6	1 2	eqeltrrd	$$⊢\phi \to ⟨G,K⟩\in \left(C\mathrm{Func}D\right)$$
7		df-br	$$⊢G\left(C\mathrm{Func}D\right)K\leftrightarrow ⟨G,K⟩\in \left(C\mathrm{Func}D\right)$$
8	6 7	sylibr	$$⊢\phi \to G\left(C\mathrm{Func}D\right)K$$
9		oppfval	Could not format ( G ( C Func D ) K -> ( G oppFunc K ) = <. G , tpos K >. ) : No typesetting found for |- ( G ( C Func D ) K -> ( G oppFunc K ) = <. G , tpos K >. ) with typecode |-
10	8 9	syl	Could not format ( ph -> ( G oppFunc K ) = <. G , tpos K >. ) : No typesetting found for |- ( ph -> ( G oppFunc K ) = <. G , tpos K >. ) with typecode |-
11	5 10	eqtrd	Could not format ( ph -> ( oppFunc ` F ) = <. G , tpos K >. ) : No typesetting found for |- ( ph -> ( oppFunc ` F ) = <. G , tpos K >. ) with typecode |-