Theorem oppctermhom

Description: The opposite category of a terminal category has the same base and hom-sets as the original category. (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	oppctermhom	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\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		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
4	2 3	termcbas	$$⊢\phi \to \exists x{\mathrm{Base}}_C=\left\{x\right\}$$
5		id	$$⊢{\mathrm{Base}}_C=\left\{x\right\}\to {\mathrm{Base}}_C=\left\{x\right\}$$
6	1 3 5	oppcmndc	$$⊢{\mathrm{Base}}_C=\left\{x\right\}\to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(O\right)$$
7	6	exlimiv	$$⊢\exists x{\mathrm{Base}}_C=\left\{x\right\}\to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(O\right)$$
8	4 7	syl	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(O\right)$$