Theorem oppfdiag1a

Description: A constant functor for opposite categories is the opposite functor of the constant functor for original categories. (Contributed by Zhi Wang, 19-Nov-2025)

	Ref	Expression
Hypotheses	oppfdiag.o	|- O = ( oppCat ` C )
	oppfdiag.p	|- P = ( oppCat ` D )
	oppfdiag.l	|- L = ( C DiagFunc D )
	oppfdiag.c	|- ( ph -> C e. Cat )
	oppfdiag.d	|- ( ph -> D e. Cat )
	oppfdiag1a.a	|- A = ( Base ` C )
	oppfdiag1a.x	|- ( ph -> X e. A )
Assertion	oppfdiag1a	|- ( ph -> ( oppFunc ` ( ( 1st ` L ) ` X ) ) = ( ( 1st ` ( O DiagFunc P ) ) ` X ) )

Proof

Step	Hyp	Ref	Expression
1		oppfdiag.o	|- O = ( oppCat ` C )
2		oppfdiag.p	|- P = ( oppCat ` D )
3		oppfdiag.l	|- L = ( C DiagFunc D )
4		oppfdiag.c	|- ( ph -> C e. Cat )
5		oppfdiag.d	|- ( ph -> D e. Cat )
6		oppfdiag1a.a	|- A = ( Base ` C )
7		oppfdiag1a.x	|- ( ph -> X e. A )
8		eqid	|- ( ( 1st ` L ) ` X ) = ( ( 1st ` L ) ` X )
9	3 4 5 6 7 8	diag1cl	|- ( ph -> ( ( 1st ` L ) ` X ) e. ( D Func C ) )
10	9	fvresd	|- ( ph -> ( ( oppFunc |` ( D Func C ) ) ` ( ( 1st ` L ) ` X ) ) = ( oppFunc ` ( ( 1st ` L ) ` X ) ) )
11		eqidd	|- ( ph -> ( oppFunc |` ( D Func C ) ) = ( oppFunc |` ( D Func C ) ) )
12	1 2 3 4 5 11 6 7	oppfdiag1	|- ( ph -> ( ( oppFunc |` ( D Func C ) ) ` ( ( 1st ` L ) ` X ) ) = ( ( 1st ` ( O DiagFunc P ) ) ` X ) )
13	10 12	eqtr3d	|- ( ph -> ( oppFunc ` ( ( 1st ` L ) ` X ) ) = ( ( 1st ` ( O DiagFunc P ) ) ` X ) )