oppf1

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

		Ref	Expression
	Hypothesis	oppf1.f	$⊢ φ \to F \in (C Func D)$
	Assertion	oppf1	Could not format assertion : No typesetting found for \|- ( ph -> ( 1st ` ( oppFunc ` F ) ) = ( 1st ` F ) ) 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	op1std	Could not format ( ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. -> ( 1st ` ( oppFunc ` F ) ) = ( 1st ` F ) ) : No typesetting found for \|- ( ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. -> ( 1st ` ( oppFunc ` F ) ) = ( 1st ` F ) ) with typecode \|-
7	1 2 6	3syl	Could not format ( ph -> ( 1st ` ( oppFunc ` F ) ) = ( 1st ` F ) ) : No typesetting found for \|- ( ph -> ( 1st ` ( oppFunc ` F ) ) = ( 1st ` F ) ) with typecode \|-

Metamath Proof Explorer