Theorem termchom

Description: The hom-set of a terminal category is a singleton of the identity morphism. (Contributed by Zhi Wang, 20-Oct-2025)

	Ref	Expression
Hypotheses	termchom.c	⊢ ( 𝜑 → 𝐶 ∈ TermCat )
	termchom.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	termchom.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	termchom.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	termchom.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	termchom.i	⊢ 1 = ( Id ‘ 𝐶 )
Assertion	termchom	⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = { ( 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	1 2 3 4 5	termchomn0	⊢ ( 𝜑 → ¬ ( 𝑋 𝐻 𝑌 ) = ∅ )
8		neq0	⊢ ( ¬ ( 𝑋 𝐻 𝑌 ) = ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) )
9	7 8	sylib	⊢ ( 𝜑 → ∃ 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) )
10	3	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝑋 ∈ 𝐵 )
11	4	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝑌 ∈ 𝐵 )
12		simpr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) )
13	1	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝐶 ∈ TermCat )
14	13	termcthind	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝐶 ∈ ThinCat )
15	10 11 12 2 5 14	thinchom	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → ( 𝑋 𝐻 𝑌 ) = { 𝑓 } )
16	13 2 10 11 5 12 6	termcid	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝑓 = ( 1 ‘ 𝑋 ) )
17	16	sneqd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → { 𝑓 } = { ( 1 ‘ 𝑋 ) } )
18	15 17	eqtrd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → ( 𝑋 𝐻 𝑌 ) = { ( 1 ‘ 𝑋 ) } )
19	9 18	exlimddv	⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = { ( 1 ‘ 𝑋 ) } )