Theorem oppcmndc

Description: The opposite category of a category whose base set is a singleton or an empty set has the same base and hom-sets as the original category. (Contributed by Zhi Wang, 16-Oct-2025)

	Ref	Expression
Hypotheses	oppcendc.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
	oppcendc.b	$$⊢B={\mathrm{Base}}_C$$
	oppcmndc.x	$$⊢\phi \to B=\left\{X\right\}$$
Assertion	oppcmndc	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(O\right)$$

Proof

Step	Hyp	Ref	Expression
1		oppcendc.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
2		oppcendc.b	$$⊢B={\mathrm{Base}}_C$$
3		oppcmndc.x	$$⊢\phi \to B=\left\{X\right\}$$
4		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
5	3	oppcmndclem	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(x\ne y\to x\mathrm{Hom}\left(C\right)y=\varnothing \right)$$
6	1 2 4 5	oppcendc	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(O\right)$$