This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) = (/) )