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	⊢ ( 𝜑 → 𝐶 ∈ TermCat )
	termchom.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	termchom.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	termchom.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	termchom.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	termchom.i	⊢ 1 = ( Id ‘ 𝐶 )
	termchom2.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
Assertion	termchom2	⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = { ( 1 ‘ 𝑍 ) } )

Proof

Step	Hyp	Ref	Expression
1		termchom.c	⊢ ( 𝜑 → 𝐶 ∈ TermCat )
2		termchom.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		termchom.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
4		termchom.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
5		termchom.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
6		termchom.i	⊢ 1 = ( Id ‘ 𝐶 )
7		termchom2.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
8	1 2 3 4 5 6	termchom	⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = { ( 1 ‘ 𝑋 ) } )
9	1 2 3 7	termcbasmo	⊢ ( 𝜑 → 𝑋 = 𝑍 )
10	9	fveq2d	⊢ ( 𝜑 → ( 1 ‘ 𝑋 ) = ( 1 ‘ 𝑍 ) )
11	10	sneqd	⊢ ( 𝜑 → { ( 1 ‘ 𝑋 ) } = { ( 1 ‘ 𝑍 ) } )
12	8 11	eqtrd	⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = { ( 1 ‘ 𝑍 ) } )