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	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
	oppcendc.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	oppcmndc.x	⊢ ( 𝜑 → 𝐵 = { 𝑋 } )
Assertion	oppcmndc	⊢ ( 𝜑 → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝑂 ) )

Proof

Step	Hyp	Ref	Expression
1		oppcendc.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2		oppcendc.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		oppcmndc.x	⊢ ( 𝜑 → 𝐵 = { 𝑋 } )
4		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
5	3	oppcmndclem	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ≠ 𝑦 → ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) = ∅ ) )
6	1 2 4 5	oppcendc	⊢ ( 𝜑 → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝑂 ) )