Theorem termccisoeu

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

	Ref	Expression
Hypotheses	termcciso.c	$$⊢C=\mathrm{CatCat}\left(U\right)$$
	termcciso.b	$$⊢B={\mathrm{Base}}_C$$
	termcciso.x	$$⊢\phi \to X\in B$$
	termcciso.y	$$⊢\phi \to Y\in B$$
	termcciso.t	No typesetting found for |- ( ph -> X e. TermCat ) with typecode |-
	termccisoeu.y	No typesetting found for |- ( ph -> Y e. TermCat ) with typecode |-
Assertion	termccisoeu	$$⊢\phi \to \exists !ff\in \left(X\mathrm{Iso}\left(C\right)Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		termcciso.c	$$⊢C=\mathrm{CatCat}\left(U\right)$$
2		termcciso.b	$$⊢B={\mathrm{Base}}_C$$
3		termcciso.x	$$⊢\phi \to X\in B$$
4		termcciso.y	$$⊢\phi \to Y\in B$$
5		termcciso.t	Could not format ( ph -> X e. TermCat ) : No typesetting found for |- ( ph -> X e. TermCat ) with typecode |-
6		termccisoeu.y	Could not format ( ph -> Y e. TermCat ) : No typesetting found for |- ( ph -> Y e. TermCat ) with typecode |-
7	1 2	elbasfv	$$⊢X\in B\to U\in \mathrm{V}$$
8	3 7	syl	$$⊢\phi \to U\in \mathrm{V}$$
9	1	catccat	$$⊢U\in \mathrm{V}\to C\in \mathrm{Cat}$$
10	8 9	syl	$$⊢\phi \to C\in \mathrm{Cat}$$
11	1 2 8	catcbas	$$⊢\phi \to B=U\cap \mathrm{Cat}$$
12	3 11	eleqtrd	$$⊢\phi \to X\in \left(U\cap \mathrm{Cat}\right)$$
13	12	elin1d	$$⊢\phi \to X\in U$$
14	1 8 13 5	termcterm	$$⊢\phi \to X\in \mathrm{TermO}\left(C\right)$$
15	4 11	eleqtrd	$$⊢\phi \to Y\in \left(U\cap \mathrm{Cat}\right)$$
16	15	elin1d	$$⊢\phi \to Y\in U$$
17	1 8 16 6	termcterm	$$⊢\phi \to Y\in \mathrm{TermO}\left(C\right)$$
18	10 14 17	termoeu1	$$⊢\phi \to \exists !ff\in \left(X\mathrm{Iso}\left(C\right)Y\right)$$