Theorem termccisoeu

Description: The isomorphism between terminal categories is unique. (Contributed by Zhi Wang, 26-Oct-2025)

	Ref	Expression
Hypotheses	termcciso.c	|- C = ( CatCat ` U )
	termcciso.b	|- B = ( Base ` C )
	termcciso.x	|- ( ph -> X e. B )
	termcciso.y	|- ( ph -> Y e. B )
	termcciso.t	|- ( ph -> X e. TermCat )
	termccisoeu.y	|- ( ph -> Y e. TermCat )
Assertion	termccisoeu	|- ( ph -> E! f f e. ( X ( Iso ` C ) Y ) )

Proof

Step	Hyp	Ref	Expression
1		termcciso.c	|- C = ( CatCat ` U )
2		termcciso.b	|- B = ( Base ` C )
3		termcciso.x	|- ( ph -> X e. B )
4		termcciso.y	|- ( ph -> Y e. B )
5		termcciso.t	|- ( ph -> X e. TermCat )
6		termccisoeu.y	|- ( ph -> Y e. TermCat )
7	1 2	elbasfv	|- ( X e. B -> U e. _V )
8	3 7	syl	|- ( ph -> U e. _V )
9	1	catccat	|- ( U e. _V -> C e. Cat )
10	8 9	syl	|- ( ph -> C e. Cat )
11	1 2 8	catcbas	|- ( ph -> B = ( U i^i Cat ) )
12	3 11	eleqtrd	|- ( ph -> X e. ( U i^i Cat ) )
13	12	elin1d	|- ( ph -> X e. U )
14	1 8 13 5	termcterm	|- ( ph -> X e. ( TermO ` C ) )
15	4 11	eleqtrd	|- ( ph -> Y e. ( U i^i Cat ) )
16	15	elin1d	|- ( ph -> Y e. U )
17	1 8 16 6	termcterm	|- ( ph -> Y e. ( TermO ` C ) )
18	10 14 17	termoeu1	|- ( ph -> E! f f e. ( X ( Iso ` C ) Y ) )