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 = ( Base ` C )
	fulltermc.h	|- H = ( Hom ` C )
	fulltermc.d	|- ( ph -> D e. TermCat )
	fulltermc2.f	|- ( ph -> F ( C Full D ) G )
	fulltermc2.x	|- ( ph -> X e. B )
	fulltermc2.y	|- ( ph -> Y e. B )
Assertion	fulltermc2	|- ( ph -> -. ( X H Y ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		fulltermc.b	|- B = ( Base ` C )
2		fulltermc.h	|- H = ( Hom ` C )
3		fulltermc.d	|- ( ph -> D e. TermCat )
4		fulltermc2.f	|- ( ph -> F ( C Full D ) G )
5		fulltermc2.x	|- ( ph -> X e. B )
6		fulltermc2.y	|- ( ph -> Y e. B )
7		oveq1	|- ( x = X -> ( x H y ) = ( X H y ) )
8	7	eqeq1d	|- ( x = X -> ( ( x H y ) = (/) <-> ( X H y ) = (/) ) )
9	8	notbid	|- ( x = X -> ( -. ( x H y ) = (/) <-> -. ( X H y ) = (/) ) )
10		oveq2	|- ( y = Y -> ( X H y ) = ( X H Y ) )
11	10	eqeq1d	|- ( y = Y -> ( ( X H y ) = (/) <-> ( X H Y ) = (/) ) )
12	11	notbid	|- ( y = Y -> ( -. ( X H y ) = (/) <-> -. ( X H Y ) = (/) ) )
13		eqid	|- ( Hom ` D ) = ( Hom ` D )
14	1 13	isfull	|- ( F ( C Full D ) G <-> ( F ( C Func D ) G /\ A. x e. B A. y e. B ran ( x G y ) = ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) ) )
15	4 14	sylib	|- ( ph -> ( F ( C Func D ) G /\ A. x e. B A. y e. B ran ( x G y ) = ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) ) )
16	15	simpld	|- ( ph -> F ( C Func D ) G )
17	1 2 3 16	fulltermc	|- ( ph -> ( F ( C Full D ) G <-> A. x e. B A. y e. B -. ( x H y ) = (/) ) )
18	4 17	mpbid	|- ( ph -> A. x e. B A. y e. B -. ( x H y ) = (/) )
19	9 12 18 5 6	rspc2dv	|- ( ph -> -. ( X H Y ) = (/) )