Theorem termchommo

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

	Ref	Expression
Hypotheses	termcbas.c	⊢ ( 𝜑 → 𝐶 ∈ TermCat )
	termcbas.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	termcbasmo.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	termcbasmo.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	termcid.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	termcid.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
	termchommo.x	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
	termchommo.y	⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
	termchommo.f	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑍 𝐻 𝑊 ) )
Assertion	termchommo	⊢ ( 𝜑 → 𝐹 = 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		termcbas.c	⊢ ( 𝜑 → 𝐶 ∈ TermCat )
2		termcbas.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		termcbasmo.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
4		termcbasmo.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
5		termcid.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
6		termcid.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
7		termchommo.x	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
8		termchommo.y	⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
9		termchommo.f	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑍 𝐻 𝑊 ) )
10	1 2 3 7	termcbasmo	⊢ ( 𝜑 → 𝑋 = 𝑍 )
11	1 2 4 8	termcbasmo	⊢ ( 𝜑 → 𝑌 = 𝑊 )
12	10 11	oveq12d	⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = ( 𝑍 𝐻 𝑊 ) )
13	9 12	eleqtrrd	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑋 𝐻 𝑌 ) )
14	1	termcthind	⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
15	3 4 6 13 2 5 14	thincmo2	⊢ ( 𝜑 → 𝐹 = 𝐺 )