Theorem fulltermc

Description: A functor to a terminal category is full iff all hom-sets of the source category are non-empty. (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 |-
	fulltermc.f	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
Assertion	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)$$

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		fulltermc.f	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
5		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
6	3	termcthind	$$⊢\phi \to D\in \mathrm{ThinCat}$$
7	1 5 2 6 4	fullthinc	$$⊢\phi \to \left(F\left(C\mathrm{Full}D\right)G\leftrightarrow \forall x\in B\forall y\in B\left(xHy=\varnothing \to F\left(x\right)\mathrm{Hom}\left(D\right)F\left(y\right)=\varnothing \right)\right)$$
8	3	adantr	Could not format ( ( ph /\ ( x e. B /\ y e. B ) ) -> D e. TermCat ) : No typesetting found for |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> D e. TermCat ) with typecode |-
9		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
10	1 9 4	funcf1	$$⊢\phi \to F:B⟶{\mathrm{Base}}_D$$
11	10	ffvelcdmda	$$⊢\left(\phi \wedge x\in B\right)\to F\left(x\right)\in {\mathrm{Base}}_D$$
12	11	adantrr	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to F\left(x\right)\in {\mathrm{Base}}_D$$
13	10	ffvelcdmda	$$⊢\left(\phi \wedge y\in B\right)\to F\left(y\right)\in {\mathrm{Base}}_D$$
14	13	adantrl	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to F\left(y\right)\in {\mathrm{Base}}_D$$
15	8 9 12 14 5	termchomn0	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \neg F\left(x\right)\mathrm{Hom}\left(D\right)F\left(y\right)=\varnothing$$
16		biimt	$$⊢\neg F\left(x\right)\mathrm{Hom}\left(D\right)F\left(y\right)=\varnothing \to \left(\neg xHy=\varnothing \leftrightarrow \left(\neg F\left(x\right)\mathrm{Hom}\left(D\right)F\left(y\right)=\varnothing \to \neg xHy=\varnothing \right)\right)$$
17	15 16	syl	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(\neg xHy=\varnothing \leftrightarrow \left(\neg F\left(x\right)\mathrm{Hom}\left(D\right)F\left(y\right)=\varnothing \to \neg xHy=\varnothing \right)\right)$$
18		con34b	$$⊢\left(xHy=\varnothing \to F\left(x\right)\mathrm{Hom}\left(D\right)F\left(y\right)=\varnothing \right)\leftrightarrow \left(\neg F\left(x\right)\mathrm{Hom}\left(D\right)F\left(y\right)=\varnothing \to \neg xHy=\varnothing \right)$$
19	17 18	bitr4di	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(\neg xHy=\varnothing \leftrightarrow \left(xHy=\varnothing \to F\left(x\right)\mathrm{Hom}\left(D\right)F\left(y\right)=\varnothing \right)\right)$$
20	19	2ralbidva	$$⊢\phi \to \left(\forall x\in B\forall y\in B\neg xHy=\varnothing \leftrightarrow \forall x\in B\forall y\in B\left(xHy=\varnothing \to F\left(x\right)\mathrm{Hom}\left(D\right)F\left(y\right)=\varnothing \right)\right)$$
21	7 20	bitr4d	$$⊢\phi \to \left(F\left(C\mathrm{Full}D\right)G\leftrightarrow \forall x\in B\forall y\in B\neg xHy=\varnothing \right)$$