Theorem oppf1

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

	Ref	Expression
Hypothesis	oppf1.f	|- ( ph -> F e. ( C Func D ) )
Assertion	oppf1	|- ( ph -> ( 1st ` ( oppFunc ` F ) ) = ( 1st ` F ) )

Proof

Step	Hyp	Ref	Expression
1		oppf1.f	|- ( ph -> F e. ( C Func D ) )
2		oppfval2	|- ( F e. ( C Func D ) -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. )
3		fvex	|- ( 1st ` F ) e. _V
4		fvex	|- ( 2nd ` F ) e. _V
5	4	tposex	|- tpos ( 2nd ` F ) e. _V
6	3 5	op1std	|- ( ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. -> ( 1st ` ( oppFunc ` F ) ) = ( 1st ` F ) )
7	1 2 6	3syl	|- ( ph -> ( 1st ` ( oppFunc ` F ) ) = ( 1st ` F ) )