oppfval3

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

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

Step	Hyp	Ref	Expression
1		oppfval3.g	$⊢ φ \to F = ⟨G, K⟩$
2		oppfval3.f	$⊢ φ \to F \in (C Func D)$
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	$⊢ φ \to ⟨G, K⟩ \in (C Func D)$
7		df-br	$⊢ G (C Func D) K \leftrightarrow ⟨G, K⟩ \in (C Func D)$
8	6 7	sylibr	$⊢ φ \to G (C Func D) 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 \|-

Metamath Proof Explorer