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 = ( oppCat ` C )
	oppcterm.c	|- ( ph -> C e. TermCat )
Assertion	oppcterm	|- ( ph -> O e. TermCat )

Proof

Step	Hyp	Ref	Expression
1		oppcterm.o	|- O = ( oppCat ` C )
2		oppcterm.c	|- ( ph -> C e. TermCat )
3	1 2	oppctermhom	|- ( ph -> ( Homf ` C ) = ( Homf ` O ) )
4	1 2	oppctermco	|- ( ph -> ( comf ` C ) = ( comf ` O ) )
5	1	fvexi	|- O e. _V
6	5	a1i	|- ( ph -> O e. _V )
7	3 4 2 6	termcpropd	|- ( ph -> ( C e. TermCat <-> O e. TermCat ) )
8	2 7	mpbid	|- ( ph -> O e. TermCat )