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)

	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		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
14	1 13	isfull	$$⊢F\left(C\mathrm{Full}D\right)G\leftrightarrow \left(F\left(C\mathrm{Func}D\right)G\wedge \forall x\in B\forall y\in B\mathrm{ran}\left(xGy\right)=F\left(x\right)\mathrm{Hom}\left(D\right)F\left(y\right)\right)$$
15	4 14	sylib	$$⊢\phi \to \left(F\left(C\mathrm{Func}D\right)G\wedge \forall x\in B\forall y\in B\mathrm{ran}\left(xGy\right)=F\left(x\right)\mathrm{Hom}\left(D\right)F\left(y\right)\right)$$
16	15	simpld	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
17	1 2 3 16	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)$$
18	4 17	mpbid	$$⊢\phi \to \forall x\in B\forall y\in B\neg xHy=\varnothing$$
19	9 12 18 5 6	rspc2dv	$$⊢\phi \to \neg XHY=\varnothing$$