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 ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
oppcthinco.c ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
oppcthinendc.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
oppcthinendc.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
oppcthinendc.1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ≠ 𝑦 → ( 𝑥 𝐻 𝑦 ) = ∅ ) )
Assertion oppcthinendc ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝑂 ) )

Proof

Step Hyp Ref Expression
1 oppcthinco.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2 oppcthinco.c ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
3 oppcthinendc.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
4 oppcthinendc.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
5 oppcthinendc.1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ≠ 𝑦 → ( 𝑥 𝐻 𝑦 ) = ∅ ) )
6 1 3 4 5 oppcendc ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝑂 ) )
7 1 2 6 oppcthinco ⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝑂 ) )