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	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
	oppcterm.c	⊢ ( 𝜑 → 𝐶 ∈ TermCat )
Assertion	oppcterm	⊢ ( 𝜑 → 𝑂 ∈ TermCat )

Proof

Step	Hyp	Ref	Expression
1		oppcterm.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2		oppcterm.c	⊢ ( 𝜑 → 𝐶 ∈ TermCat )
3	1 2	oppctermhom	⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝑂 ) )
4	1 2	oppctermco	⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝑂 ) )
5	1	fvexi	⊢ 𝑂 ∈ V
6	5	a1i	⊢ ( 𝜑 → 𝑂 ∈ V )
7	3 4 2 6	termcpropd	⊢ ( 𝜑 → ( 𝐶 ∈ TermCat ↔ 𝑂 ∈ TermCat ) )
8	2 7	mpbid	⊢ ( 𝜑 → 𝑂 ∈ TermCat )