Theorem termchom2

Description: The hom-set of a terminal category is a singleton of the identity morphism. (Contributed by Zhi Wang, 21-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)$$
	termchom2.z	$$⊢\phi \to Z\in B$$
Assertion	termchom2	$$⊢\phi \to XHY=\left\{\underset{\dot{}}{1}\left(Z\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		termchom2.z	$$⊢\phi \to Z\in B$$
8	1 2 3 4 5 6	termchom	$$⊢\phi \to XHY=\left\{\underset{\dot{}}{1}\left(X\right)\right\}$$
9	1 2 3 7	termcbasmo	$$⊢\phi \to X=Z$$
10	9	fveq2d	$$⊢\phi \to \underset{\dot{}}{1}\left(X\right)=\underset{\dot{}}{1}\left(Z\right)$$
11	10	sneqd	$$⊢\phi \to \left\{\underset{\dot{}}{1}\left(X\right)\right\}=\left\{\underset{\dot{}}{1}\left(Z\right)\right\}$$
12	8 11	eqtrd	$$⊢\phi \to XHY=\left\{\underset{\dot{}}{1}\left(Z\right)\right\}$$