Theorem termchommo

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

	Ref	Expression
Hypotheses	termcbas.c	|- ( ph -> C e. TermCat )
	termcbas.b	|- B = ( Base ` C )
	termcbasmo.x	|- ( ph -> X e. B )
	termcbasmo.y	|- ( ph -> Y e. B )
	termcid.h	|- H = ( Hom ` C )
	termcid.f	|- ( ph -> F e. ( X H Y ) )
	termchommo.x	|- ( ph -> Z e. B )
	termchommo.y	|- ( ph -> W e. B )
	termchommo.f	|- ( ph -> G e. ( Z H W ) )
Assertion	termchommo	|- ( ph -> F = G )

Proof

Step	Hyp	Ref	Expression
1		termcbas.c	|- ( ph -> C e. TermCat )
2		termcbas.b	|- B = ( Base ` C )
3		termcbasmo.x	|- ( ph -> X e. B )
4		termcbasmo.y	|- ( ph -> Y e. B )
5		termcid.h	|- H = ( Hom ` C )
6		termcid.f	|- ( ph -> F e. ( X H Y ) )
7		termchommo.x	|- ( ph -> Z e. B )
8		termchommo.y	|- ( ph -> W e. B )
9		termchommo.f	|- ( ph -> G e. ( Z H W ) )
10	1 2 3 7	termcbasmo	|- ( ph -> X = Z )
11	1 2 4 8	termcbasmo	|- ( ph -> Y = W )
12	10 11	oveq12d	|- ( ph -> ( X H Y ) = ( Z H W ) )
13	9 12	eleqtrrd	|- ( ph -> G e. ( X H Y ) )
14	1	termcthind	|- ( ph -> C e. ThinCat )
15	3 4 6 13 2 5 14	thincmo2	|- ( ph -> F = G )