Theorem fulltermc2

Description: Given a full functor to a terminal category, the source category must not have empty hom-sets. (Contributed by Zhi Wang, 17-Oct-2025) (Proof shortened by Zhi Wang, 6-Nov-2025)

	Ref	Expression
Hypotheses	fulltermc.b	$$⊢B={\mathrm{Base}}_C$$
	fulltermc.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	fulltermc.d	No typesetting found for |- ( ph -> D e. TermCat ) with typecode |-
	fulltermc2.f	$$⊢\phi \to F\left(C\mathrm{Full}D\right)G$$
	fulltermc2.x	$$⊢\phi \to X\in B$$
	fulltermc2.y	$$⊢\phi \to Y\in B$$
Assertion	fulltermc2	$$⊢\phi \to \neg XHY=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		fulltermc.b	$$⊢B={\mathrm{Base}}_C$$
2		fulltermc.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
3		fulltermc.d	Could not format ( ph -> D e. TermCat ) : No typesetting found for |- ( ph -> D e. TermCat ) with typecode |-
4		fulltermc2.f	$$⊢\phi \to F\left(C\mathrm{Full}D\right)G$$
5		fulltermc2.x	$$⊢\phi \to X\in B$$
6		fulltermc2.y	$$⊢\phi \to Y\in B$$
7		oveq1	$$⊢x=X\to xHy=XHy$$
8	7	eqeq1d	$$⊢x=X\to \left(xHy=\varnothing \leftrightarrow XHy=\varnothing \right)$$
9	8	notbid	$$⊢x=X\to \left(\neg xHy=\varnothing \leftrightarrow \neg XHy=\varnothing \right)$$
10		oveq2	$$⊢y=Y\to XHy=XHY$$
11	10	eqeq1d	$$⊢y=Y\to \left(XHy=\varnothing \leftrightarrow XHY=\varnothing \right)$$
12	11	notbid	$$⊢y=Y\to \left(\neg XHy=\varnothing \leftrightarrow \neg XHY=\varnothing \right)$$
13		fullfunc	$$⊢C\mathrm{Full}D\subseteq C\mathrm{Func}D$$
14	13	ssbri	$$⊢F\left(C\mathrm{Full}D\right)G\to F\left(C\mathrm{Func}D\right)G$$
15	4 14	syl	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
16	1 2 3 15	fulltermc	$$⊢\phi \to \left(F\left(C\mathrm{Full}D\right)G\leftrightarrow \forall x\in B\forall y\in B\neg xHy=\varnothing \right)$$
17	4 16	mpbid	$$⊢\phi \to \forall x\in B\forall y\in B\neg xHy=\varnothing$$
18	9 12 17 5 6	rspc2dv	$$⊢\phi \to \neg XHY=\varnothing$$