Metamath Proof Explorer

Theorem fullthinc2

Description: A full functor to a thin category maps empty hom-sets to empty hom-sets. (Contributed by Zhi Wang, 1-Oct-2024)

Ref Expression
Hypotheses fullthinc.b 
|- B = ( Base ` C )
fullthinc.j 
|- J = ( Hom ` D )
fullthinc.h 
|- H = ( Hom ` C )
fullthinc.d 
|- ( ph -> D e. ThinCat )
fullthinc2.f 
|- ( ph -> F ( C Full D ) G )
fullthinc2.x 
|- ( ph -> X e. B )
fullthinc2.y 
|- ( ph -> Y e. B )
Assertion fullthinc2 
|- ( ph -> ( ( X H Y ) = (/) <-> ( ( F ` X ) J ( F ` Y ) ) = (/) ) )

Proof

Step Hyp Ref Expression
1 fullthinc.b 
 |-  B = ( Base ` C )
2 fullthinc.j 
 |-  J = ( Hom ` D )
3 fullthinc.h 
 |-  H = ( Hom ` C )
4 fullthinc.d 
 |-  ( ph -> D e. ThinCat )
5 fullthinc2.f 
 |-  ( ph -> F ( C Full D ) G )
6 fullthinc2.x 
 |-  ( ph -> X e. B )
7 fullthinc2.y 
 |-  ( ph -> Y e. B )
8 fullfunc 
 |-  ( C Full D ) C_ ( C Func D )
9 8 ssbri 
 |-  ( F ( C Full D ) G -> F ( C Func D ) G )
10 5 9 syl 
 |-  ( ph -> F ( C Func D ) G )
11 1 2 3 4 10 fullthinc 
 |-  ( ph -> ( F ( C Full D ) G <-> A. x e. B A. y e. B ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) ) )
12 5 11 mpbid 
 |-  ( ph -> A. x e. B A. y e. B ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) )
13 oveq12 
 |-  ( ( x = X /\ y = Y ) -> ( x H y ) = ( X H Y ) )
14 13 eqeq1d 
 |-  ( ( x = X /\ y = Y ) -> ( ( x H y ) = (/) <-> ( X H Y ) = (/) ) )
15 simpl 
 |-  ( ( x = X /\ y = Y ) -> x = X )
16 15 fveq2d 
 |-  ( ( x = X /\ y = Y ) -> ( F ` x ) = ( F ` X ) )
17 simpr 
 |-  ( ( x = X /\ y = Y ) -> y = Y )
18 17 fveq2d 
 |-  ( ( x = X /\ y = Y ) -> ( F ` y ) = ( F ` Y ) )
19 16 18 oveq12d 
 |-  ( ( x = X /\ y = Y ) -> ( ( F ` x ) J ( F ` y ) ) = ( ( F ` X ) J ( F ` Y ) ) )
20 19 eqeq1d 
 |-  ( ( x = X /\ y = Y ) -> ( ( ( F ` x ) J ( F ` y ) ) = (/) <-> ( ( F ` X ) J ( F ` Y ) ) = (/) ) )
21 14 20 imbi12d 
 |-  ( ( x = X /\ y = Y ) -> ( ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) <-> ( ( X H Y ) = (/) -> ( ( F ` X ) J ( F ` Y ) ) = (/) ) ) )
22 21 rspc2gv 
 |-  ( ( X e. B /\ Y e. B ) -> ( A. x e. B A. y e. B ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) -> ( ( X H Y ) = (/) -> ( ( F ` X ) J ( F ` Y ) ) = (/) ) ) )
23 22 imp 
 |-  ( ( ( X e. B /\ Y e. B ) /\ A. x e. B A. y e. B ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) ) -> ( ( X H Y ) = (/) -> ( ( F ` X ) J ( F ` Y ) ) = (/) ) )
24 6 7 12 23 syl21anc 
 |-  ( ph -> ( ( X H Y ) = (/) -> ( ( F ` X ) J ( F ` Y ) ) = (/) ) )
25 1 3 2 10 6 7 funcf2 
 |-  ( ph -> ( X G Y ) : ( X H Y ) --> ( ( F ` X ) J ( F ` Y ) ) )
26 25 f002 
 |-  ( ph -> ( ( ( F ` X ) J ( F ` Y ) ) = (/) -> ( X H Y ) = (/) ) )
27 24 26 impbid 
 |-  ( ph -> ( ( X H Y ) = (/) <-> ( ( F ` X ) J ( F ` Y ) ) = (/) ) )