Theorem termchom

Description: The hom-set of a terminal category is a singleton of the identity morphism. (Contributed by Zhi Wang, 20-Oct-2025)

	Ref	Expression
Hypotheses	termchom.c	No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-
	termchom.b	$$⊢B={\mathrm{Base}}_C$$
	termchom.x	$$⊢\phi \to X\in B$$
	termchom.y	$$⊢\phi \to Y\in B$$
	termchom.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	termchom.i	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
Assertion	termchom	$$⊢\phi \to XHY=\left\{\underset{\dot{}}{1}\left(X\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		termchom.c	Could not format ( ph -> C e. TermCat ) : No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-
2		termchom.b	$$⊢B={\mathrm{Base}}_C$$
3		termchom.x	$$⊢\phi \to X\in B$$
4		termchom.y	$$⊢\phi \to Y\in B$$
5		termchom.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
6		termchom.i	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
7	1 2 3 4 5	termchomn0	$$⊢\phi \to \neg XHY=\varnothing$$
8		neq0	$$⊢\neg XHY=\varnothing \leftrightarrow \exists ff\in \left(XHY\right)$$
9	7 8	sylib	$$⊢\phi \to \exists ff\in \left(XHY\right)$$
10	3	adantr	$$⊢\left(\phi \wedge f\in \left(XHY\right)\right)\to X\in B$$
11	4	adantr	$$⊢\left(\phi \wedge f\in \left(XHY\right)\right)\to Y\in B$$
12		simpr	$$⊢\left(\phi \wedge f\in \left(XHY\right)\right)\to f\in \left(XHY\right)$$
13	1	adantr	Could not format ( ( ph /\ f e. ( X H Y ) ) -> C e. TermCat ) : No typesetting found for |- ( ( ph /\ f e. ( X H Y ) ) -> C e. TermCat ) with typecode |-
14	13	termcthind	$$⊢\left(\phi \wedge f\in \left(XHY\right)\right)\to C\in \mathrm{ThinCat}$$
15	10 11 12 2 5 14	thinchom	$$⊢\left(\phi \wedge f\in \left(XHY\right)\right)\to XHY=\left\{f\right\}$$
16	13 2 10 11 5 12 6	termcid	$$⊢\left(\phi \wedge f\in \left(XHY\right)\right)\to f=\underset{\dot{}}{1}\left(X\right)$$
17	16	sneqd	$$⊢\left(\phi \wedge f\in \left(XHY\right)\right)\to \left\{f\right\}=\left\{\underset{\dot{}}{1}\left(X\right)\right\}$$
18	15 17	eqtrd	$$⊢\left(\phi \wedge f\in \left(XHY\right)\right)\to XHY=\left\{\underset{\dot{}}{1}\left(X\right)\right\}$$
19	9 18	exlimddv	$$⊢\phi \to XHY=\left\{\underset{\dot{}}{1}\left(X\right)\right\}$$