Theorem oppcterm

Description: The opposite category of a terminal category is a terminal 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	oppcterm	Could not format assertion : No typesetting found for |- ( ph -> O e. TermCat ) with typecode |-

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	1 2	oppctermhom	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(O\right)$$
4	1 2	oppctermco	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(O\right)$$
5	1	fvexi	$$⊢O\in \mathrm{V}$$
6	5	a1i	$$⊢\phi \to O\in \mathrm{V}$$
7	3 4 2 6	termcpropd	Could not format ( ph -> ( C e. TermCat <-> O e. TermCat ) ) : No typesetting found for |- ( ph -> ( C e. TermCat <-> O e. TermCat ) ) with typecode |-
8	2 7	mpbid	Could not format ( ph -> O e. TermCat ) : No typesetting found for |- ( ph -> O e. TermCat ) with typecode |-