Metamath Proof Explorer

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 = ( Base ` C )
fulltermc.h 
|- H = ( Hom ` C )
fulltermc.d 
|- ( ph -> D e. TermCat )
fulltermc.f 
|- ( ph -> F ( C Func D ) G )
Assertion fulltermc 
|- ( ph -> ( F ( C Full D ) G <-> A. x e. B A. y e. B -. ( 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 fulltermc.f 
 |-  ( ph -> F ( C Func D ) G )
5 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
6 3 termcthind 
 |-  ( ph -> D e. ThinCat )
7 1 5 2 6 4 fullthinc 
 |-  ( ph -> ( F ( C Full D ) G <-> A. x e. B A. y e. B ( ( x H y ) = (/) -> ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) = (/) ) ) )
8 3 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> D e. TermCat )
9 eqid 
 |-  ( Base ` D ) = ( Base ` D )
10 1 9 4 funcf1 
 |-  ( ph -> F : B --> ( Base ` D ) )
11 10 ffvelcdmda 
 |-  ( ( ph /\ x e. B ) -> ( F ` x ) e. ( Base ` D ) )
12 11 adantrr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` x ) e. ( Base ` D ) )
13 10 ffvelcdmda 
 |-  ( ( ph /\ y e. B ) -> ( F ` y ) e. ( Base ` D ) )
14 13 adantrl 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` y ) e. ( Base ` D ) )
15 8 9 12 14 5 termchomn0 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> -. ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) = (/) )
16 biimt 
 |-  ( -. ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) = (/) -> ( -. ( x H y ) = (/) <-> ( -. ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) = (/) -> -. ( x H y ) = (/) ) ) )
17 15 16 syl 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( -. ( x H y ) = (/) <-> ( -. ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) = (/) -> -. ( x H y ) = (/) ) ) )
18 con34b 
 |-  ( ( ( x H y ) = (/) -> ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) = (/) ) <-> ( -. ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) = (/) -> -. ( x H y ) = (/) ) )
19 17 18 bitr4di 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( -. ( x H y ) = (/) <-> ( ( x H y ) = (/) -> ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) = (/) ) ) )
20 19 2ralbidva 
 |-  ( ph -> ( A. x e. B A. y e. B -. ( x H y ) = (/) <-> A. x e. B A. y e. B ( ( x H y ) = (/) -> ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) = (/) ) ) )
21 7 20 bitr4d 
 |-  ( ph -> ( F ( C Full D ) G <-> A. x e. B A. y e. B -. ( x H y ) = (/) ) )