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

Metamath Proof Explorer

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 = oppCat (C)$
	oppcendc.b	$⊢ B = {Base}_{C}$
	oppcmndc.x	$⊢ φ \to B = \{X\}$
Assertion	oppcmndc	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (O)$

Proof

Step	Hyp	Ref	Expression
1		oppcendc.o	$⊢ O = oppCat (C)$
2		oppcendc.b	$⊢ B = {Base}_{C}$
3		oppcmndc.x	$⊢ φ \to B = \{X\}$
4		eqid	$⊢ Hom (C) = Hom (C)$
5	3	oppcmndclem	$⊢ (φ \land (x \in B \land y \in B)) \to (x \neq y \to x Hom (C) y = \emptyset)$
6	1 2 4 5	oppcendc	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (O)$