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	$$⊢O=\mathrm{oppCat}\left(C\right)$$
	oppcterm.c	No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-
Assertion	oppctermco	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(O\right)$$

Proof

Step	Hyp	Ref	Expression
1		oppcterm.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
2		oppcterm.c	Could not format ( ph -> C e. TermCat ) : No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-
3	2	termcthind	$$⊢\phi \to C\in \mathrm{ThinCat}$$
4	1 2	oppctermhom	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(O\right)$$
5	1 3 4	oppcthinco	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(O\right)$$