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 Δ_{func} D$
		oppfdiag.c	$⊢ φ \to C \in Cat$
		oppfdiag.d	$⊢ φ \to D \in Cat$
		oppfdiag1a.a	$⊢ A = {Base}_{C}$
		oppfdiag1a.x	$⊢ φ \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 = oppCat (C)$
2		oppfdiag.p	$⊢ P = oppCat (D)$
3		oppfdiag.l	$⊢ L = C Δ_{func} D$
4		oppfdiag.c	$⊢ φ \to C \in Cat$
5		oppfdiag.d	$⊢ φ \to D \in Cat$
6		oppfdiag1a.a	$⊢ A = {Base}_{C}$
7		oppfdiag1a.x	$⊢ φ \to X \in A$
8		eqid	$⊢ 1^{st} (L) (X) = 1^{st} (L) (X)$
9	3 4 5 6 7 8	diag1cl	$⊢ φ \to 1^{st} (L) (X) \in (D Func C)$
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 \|-