This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )