Theorem termchomn0

Description: All hom-sets of a terminal category are non-empty. (Contributed by Zhi Wang, 17-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)$$
Assertion	termchomn0	$$⊢\phi \to \neg XHY=\varnothing$$

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		eqid	$$⊢\mathrm{Id}\left(C\right)=\mathrm{Id}\left(C\right)$$
7	1	termccatd	$$⊢\phi \to C\in \mathrm{Cat}$$
8	2 5 6 7 3	catidcl	$$⊢\phi \to \mathrm{Id}\left(C\right)\left(X\right)\in \left(XHX\right)$$
9	1 2 3 4	termcbasmo	$$⊢\phi \to X=Y$$
10	9	oveq2d	$$⊢\phi \to XHX=XHY$$
11	8 10	eleqtrd	$$⊢\phi \to \mathrm{Id}\left(C\right)\left(X\right)\in \left(XHY\right)$$
12		n0i	$$⊢\mathrm{Id}\left(C\right)\left(X\right)\in \left(XHY\right)\to \neg XHY=\varnothing$$
13	11 12	syl	$$⊢\phi \to \neg XHY=\varnothing$$