oppf2

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

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

Step	Hyp	Ref	Expression
1		oppf1.f	$⊢ φ \to F \in (C Func D)$
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} (F) \in V$
4		fvex	$⊢ 2^{nd} (F) \in V$
5	4	tposex	$⊢ tpos 2^{nd} (F) \in 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	$⊢ M tpos 2^{nd} (F) N = N 2^{nd} (F) 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 \|-

Metamath Proof Explorer