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

Metamath Proof Explorer

Theorem oppcthinendc

Description: The opposite category of a thin category whose morphisms are all endomorphisms has the same base, hom-sets ( oppcendc ) and composition operation as the original category. (Contributed by Zhi Wang, 16-Oct-2025)

	Ref	Expression
Hypotheses	oppcthinco.o	$⊢ O = oppCat (C)$
	oppcthinco.c	$⊢ φ \to C \in ThinCat$
	oppcthinendc.b	$⊢ B = {Base}_{C}$
	oppcthinendc.h	$⊢ H = Hom (C)$
	oppcthinendc.1	$⊢ (φ \land (x \in B \land y \in B)) \to (x \neq y \to x H y = \emptyset)$
Assertion	oppcthinendc	$⊢ φ \to {comp}_{𝑓} (C) = {comp}_{𝑓} (O)$

Proof

Step	Hyp	Ref	Expression
1		oppcthinco.o	$⊢ O = oppCat (C)$
2		oppcthinco.c	$⊢ φ \to C \in ThinCat$
3		oppcthinendc.b	$⊢ B = {Base}_{C}$
4		oppcthinendc.h	$⊢ H = Hom (C)$
5		oppcthinendc.1	$⊢ (φ \land (x \in B \land y \in B)) \to (x \neq y \to x H y = \emptyset)$
6	1 3 4 5	oppcendc	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (O)$
7	1 2 6	oppcthinco	$⊢ φ \to {comp}_{𝑓} (C) = {comp}_{𝑓} (O)$