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=\mathrm{oppCat}\left(C\right)$$
	oppfdiag.p	$$⊢P=\mathrm{oppCat}\left(D\right)$$
	oppfdiag.l	$$⊢L=C{\Delta }_{\mathrm{func}}D$$
	oppfdiag.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	oppfdiag.d	$$⊢\phi \to D\in \mathrm{Cat}$$
	oppfdiag1a.a	$$⊢A={\mathrm{Base}}_C$$
	oppfdiag1a.x	$$⊢\phi \to X\in A$$
Assertion	oppfdiag1a	Could not format assertion : No typesetting found for |- ( ph -> ( oppFunc ` ( ( 1st ` L ) ` X ) ) = ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		oppfdiag.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
2		oppfdiag.p	$$⊢P=\mathrm{oppCat}\left(D\right)$$
3		oppfdiag.l	$$⊢L=C{\Delta }_{\mathrm{func}}D$$
4		oppfdiag.c	$$⊢\phi \to C\in \mathrm{Cat}$$
5		oppfdiag.d	$$⊢\phi \to D\in \mathrm{Cat}$$
6		oppfdiag1a.a	$$⊢A={\mathrm{Base}}_C$$
7		oppfdiag1a.x	$$⊢\phi \to X\in A$$
8		eqid	$$⊢1^{st}\left(L\right)\left(X\right)=1^{st}\left(L\right)\left(X\right)$$
9	3 4 5 6 7 8	diag1cl	$$⊢\phi \to 1^{st}\left(L\right)\left(X\right)\in \left(D\mathrm{Func}C\right)$$
10	9	fvresd	Could not format ( ph -> ( ( oppFunc |` ( D Func C ) ) ` ( ( 1st ` L ) ` X ) ) = ( oppFunc ` ( ( 1st ` L ) ` X ) ) ) : No typesetting found for |- ( ph -> ( ( oppFunc |` ( D Func C ) ) ` ( ( 1st ` L ) ` X ) ) = ( oppFunc ` ( ( 1st ` L ) ` X ) ) ) with typecode |-
11		eqidd	Could not format ( ph -> ( oppFunc |` ( D Func C ) ) = ( oppFunc |` ( D Func C ) ) ) : No typesetting found for |- ( ph -> ( oppFunc |` ( D Func C ) ) = ( oppFunc |` ( D Func C ) ) ) with typecode |-
12	1 2 3 4 5 11 6 7	oppfdiag1	Could not format ( ph -> ( ( oppFunc |` ( D Func C ) ) ` ( ( 1st ` L ) ` X ) ) = ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) : No typesetting found for |- ( ph -> ( ( oppFunc |` ( D Func C ) ) ` ( ( 1st ` L ) ` X ) ) = ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) with typecode |-
13	10 12	eqtr3d	Could not format ( ph -> ( oppFunc ` ( ( 1st ` L ) ` X ) ) = ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) : No typesetting found for |- ( ph -> ( oppFunc ` ( ( 1st ` L ) ` X ) ) = ( ( 1st ` ( O DiagFunc P ) ) ` X ) ) with typecode |-