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	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	termoeu2.a	⊢ ( 𝜑 → 𝐴 ∈ ( TermO ‘ 𝐶 ) )
	termoeu2.i	⊢ ( 𝜑 → 𝐴 ( ≃𝑐 ‘ 𝐶 ) 𝐵 )
Assertion	termoeu2	⊢ ( 𝜑 → 𝐵 ∈ ( TermO ‘ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		termoeu2.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
2		termoeu2.a	⊢ ( 𝜑 → 𝐴 ∈ ( TermO ‘ 𝐶 ) )
3		termoeu2.i	⊢ ( 𝜑 → 𝐴 ( ≃𝑐 ‘ 𝐶 ) 𝐵 )
4		eqid	⊢ ( oppCat ‘ 𝐶 ) = ( oppCat ‘ 𝐶 )
5	4	oppccat	⊢ ( 𝐶 ∈ Cat → ( oppCat ‘ 𝐶 ) ∈ Cat )
6	1 5	syl	⊢ ( 𝜑 → ( oppCat ‘ 𝐶 ) ∈ Cat )
7		oppctermo	⊢ ( 𝐴 ∈ ( TermO ‘ 𝐶 ) ↔ 𝐴 ∈ ( InitO ‘ ( oppCat ‘ 𝐶 ) ) )
8	2 7	sylib	⊢ ( 𝜑 → 𝐴 ∈ ( InitO ‘ ( oppCat ‘ 𝐶 ) ) )
9	4 3	oppccic	⊢ ( 𝜑 → 𝐴 ( ≃𝑐 ‘ ( oppCat ‘ 𝐶 ) ) 𝐵 )
10	6 8 9	initoeu2	⊢ ( 𝜑 → 𝐵 ∈ ( InitO ‘ ( oppCat ‘ 𝐶 ) ) )
11		oppctermo	⊢ ( 𝐵 ∈ ( TermO ‘ 𝐶 ) ↔ 𝐵 ∈ ( InitO ‘ ( oppCat ‘ 𝐶 ) ) )
12	10 11	sylibr	⊢ ( 𝜑 → 𝐵 ∈ ( TermO ‘ 𝐶 ) )