Theorem termoeu2

Description: Terminal objects are essentially unique; if A is a terminal object, then so is every object that is isomorphic to A . (Contributed by Zhi Wang, 26-Oct-2025)

	Ref	Expression
Hypotheses	termoeu2.c	|- ( ph -> C e. Cat )
	termoeu2.a	|- ( ph -> A e. ( TermO ` C ) )
	termoeu2.i	|- ( ph -> A ( ~=c ` C ) B )
Assertion	termoeu2	|- ( ph -> B e. ( TermO ` C ) )

Proof

Step	Hyp	Ref	Expression
1		termoeu2.c	|- ( ph -> C e. Cat )
2		termoeu2.a	|- ( ph -> A e. ( TermO ` C ) )
3		termoeu2.i	|- ( ph -> A ( ~=c ` C ) B )
4		eqid	|- ( oppCat ` C ) = ( oppCat ` C )
5	4	oppccat	|- ( C e. Cat -> ( oppCat ` C ) e. Cat )
6	1 5	syl	|- ( ph -> ( oppCat ` C ) e. Cat )
7		oppctermo	|- ( A e. ( TermO ` C ) <-> A e. ( InitO ` ( oppCat ` C ) ) )
8	2 7	sylib	|- ( ph -> A e. ( InitO ` ( oppCat ` C ) ) )
9	4 3	oppccic	|- ( ph -> A ( ~=c ` ( oppCat ` C ) ) B )
10	6 8 9	initoeu2	|- ( ph -> B e. ( InitO ` ( oppCat ` C ) ) )
11		oppctermo	|- ( B e. ( TermO ` C ) <-> B e. ( InitO ` ( oppCat ` C ) ) )
12	10 11	sylibr	|- ( ph -> B e. ( TermO ` C ) )