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

Metamath Proof Explorer

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 = oppCat (C)$
		oppcterm.c	No typesetting found for \|- ( ph -> C e. TermCat ) with typecode \|-
	Assertion	oppctermhom	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (O)$

Proof

Step	Hyp	Ref	Expression
1		oppcterm.o	$⊢ O = oppCat (C)$
2		oppcterm.c	Could not format ( ph -> C e. TermCat ) : No typesetting found for \|- ( ph -> C e. TermCat ) with typecode \|-
3		eqid	$⊢ {Base}_{C} = {Base}_{C}$
4	2 3	termcbas	$⊢ φ \to \exists x {Base}_{C} = \{x\}$
5		id	$⊢ {Base}_{C} = \{x\} \to {Base}_{C} = \{x\}$
6	1 3 5	oppcmndc	$⊢ {Base}_{C} = \{x\} \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (O)$
7	6	exlimiv	$⊢ \exists x {Base}_{C} = \{x\} \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (O)$
8	4 7	syl	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (O)$