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=\mathrm{oppCat}\left(C\right)$$
	oppcthinco.c	$$⊢\phi \to C\in \mathrm{ThinCat}$$
	oppcthinendc.b	$$⊢B={\mathrm{Base}}_C$$
	oppcthinendc.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	oppcthinendc.1	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(x\ne y\to xHy=\varnothing \right)$$
Assertion	oppcthinendc	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(O\right)$$

Proof

Step	Hyp	Ref	Expression
1		oppcthinco.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
2		oppcthinco.c	$$⊢\phi \to C\in \mathrm{ThinCat}$$
3		oppcthinendc.b	$$⊢B={\mathrm{Base}}_C$$
4		oppcthinendc.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
5		oppcthinendc.1	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(x\ne y\to xHy=\varnothing \right)$$
6	1 3 4 5	oppcendc	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(O\right)$$
7	1 2 6	oppcthinco	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(O\right)$$