Theorem termchommo

Description: All morphisms of a terminal category are identical. (Contributed by Zhi Wang, 16-Oct-2025)

	Ref	Expression
Hypotheses	termcbas.c	No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-
	termcbas.b	$$⊢B={\mathrm{Base}}_C$$
	termcbasmo.x	$$⊢\phi \to X\in B$$
	termcbasmo.y	$$⊢\phi \to Y\in B$$
	termcid.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	termcid.f	$$⊢\phi \to F\in \left(XHY\right)$$
	termchommo.x	$$⊢\phi \to Z\in B$$
	termchommo.y	$$⊢\phi \to W\in B$$
	termchommo.f	$$⊢\phi \to G\in \left(ZHW\right)$$
Assertion	termchommo	$$⊢\phi \to F=G$$

Proof

Step	Hyp	Ref	Expression
1		termcbas.c	Could not format ( ph -> C e. TermCat ) : No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-
2		termcbas.b	$$⊢B={\mathrm{Base}}_C$$
3		termcbasmo.x	$$⊢\phi \to X\in B$$
4		termcbasmo.y	$$⊢\phi \to Y\in B$$
5		termcid.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
6		termcid.f	$$⊢\phi \to F\in \left(XHY\right)$$
7		termchommo.x	$$⊢\phi \to Z\in B$$
8		termchommo.y	$$⊢\phi \to W\in B$$
9		termchommo.f	$$⊢\phi \to G\in \left(ZHW\right)$$
10	1 2 3 7	termcbasmo	$$⊢\phi \to X=Z$$
11	1 2 4 8	termcbasmo	$$⊢\phi \to Y=W$$
12	10 11	oveq12d	$$⊢\phi \to XHY=ZHW$$
13	9 12	eleqtrrd	$$⊢\phi \to G\in \left(XHY\right)$$
14	1	termcthind	$$⊢\phi \to C\in \mathrm{ThinCat}$$
15	3 4 6 13 2 5 14	thincmo2	$$⊢\phi \to F=G$$