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 = ( 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		fullfunc	|- ( C Full D ) C_ ( C Func D )
14	13	ssbri	|- ( F ( C Full D ) G -> F ( C Func D ) G )
15	4 14	syl	|- ( ph -> F ( C Func D ) G )
16	1 2 3 15	fulltermc	|- ( ph -> ( F ( C Full D ) G <-> A. x e. B A. y e. B -. ( x H y ) = (/) ) )
17	4 16	mpbid	|- ( ph -> A. x e. B A. y e. B -. ( x H y ) = (/) )
18	9 12 17 5 6	rspc2dv	|- ( ph -> -. ( X H Y ) = (/) )