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

Metamath Proof Explorer

Theorem oppctermco

Description: The opposite category of a terminal category has the same base, hom-sets and composition operation as the original category. Note that C = O cannot be proved because C might not even be a function. For example, let C be ( { <. ( Basendx ) , { (/) } >. , <. ( Homndx ) , ( (V X. V ) X. { { (/) } } ) >. } u. { <. ( compndx ) , { (/) } >. , <. ( compndx ) , 2o >. } ) ; it should be a terminal category, but the opposite category is not itself. See the definitions df-oppc and df-sets . (Contributed by Zhi Wang, 16-Oct-2025)

Ref Expression
Hypotheses oppcterm.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
oppcterm.c ⊢ ( 𝜑 → 𝐶 ∈ TermCat )
Assertion oppctermco ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝑂 ) )

Proof

Step Hyp Ref Expression
1 oppcterm.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2 oppcterm.c ⊢ ( 𝜑 → 𝐶 ∈ TermCat )
3 2 termcthind ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
4 1 2 oppctermhom ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝑂 ) )
5 1 3 4 oppcthinco ⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝑂 ) )