Theorem oppf2

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

	Ref	Expression
Hypothesis	oppf1.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
Assertion	oppf2	Could not format assertion : No typesetting found for |- ( ph -> ( M ( 2nd ` ( oppFunc ` F ) ) N ) = ( N ( 2nd ` F ) M ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		oppf1.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
2		oppfval2	Could not format ( F e. ( C Func D ) -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) : No typesetting found for |- ( F e. ( C Func D ) -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) with typecode |-
3		fvex	$$⊢1^{st}\left(F\right)\in \mathrm{V}$$
4		fvex	$$⊢2^{nd}\left(F\right)\in \mathrm{V}$$
5	4	tposex	$$⊢tpos{2}^{nd}\left(F\right)\in \mathrm{V}$$
6	3 5	op2ndd	Could not format ( ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. -> ( 2nd ` ( oppFunc ` F ) ) = tpos ( 2nd ` F ) ) : No typesetting found for |- ( ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. -> ( 2nd ` ( oppFunc ` F ) ) = tpos ( 2nd ` F ) ) with typecode |-
7	1 2 6	3syl	Could not format ( ph -> ( 2nd ` ( oppFunc ` F ) ) = tpos ( 2nd ` F ) ) : No typesetting found for |- ( ph -> ( 2nd ` ( oppFunc ` F ) ) = tpos ( 2nd ` F ) ) with typecode |-
8	7	oveqd	Could not format ( ph -> ( M ( 2nd ` ( oppFunc ` F ) ) N ) = ( M tpos ( 2nd ` F ) N ) ) : No typesetting found for |- ( ph -> ( M ( 2nd ` ( oppFunc ` F ) ) N ) = ( M tpos ( 2nd ` F ) N ) ) with typecode |-
9		ovtpos	$$⊢Mtpos{2}^{nd}\left(F\right)N=N{2}^{nd}\left(F\right)M$$
10	8 9	eqtrdi	Could not format ( ph -> ( M ( 2nd ` ( oppFunc ` F ) ) N ) = ( N ( 2nd ` F ) M ) ) : No typesetting found for |- ( ph -> ( M ( 2nd ` ( oppFunc ` F ) ) N ) = ( N ( 2nd ` F ) M ) ) with typecode |-