Metamath Proof Explorer

Theorem fullthinc

Description: A functor to a thin category is full iff empty hom-sets are mapped 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 )
fullthinc.f 
|- ( ph -> F ( C Func D ) G )
Assertion fullthinc 
|- ( ph -> ( F ( C Full D ) G <-> A. x e. B A. y e. B ( ( 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 fullthinc.f 
 |-  ( ph -> F ( C Func D ) G )
6 1 2 3 isfull2 
 |-  ( F ( C Full D ) G <-> ( F ( C Func D ) G /\ A. x e. B A. y e. B ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) ) )
7 foeq2 
 |-  ( ( x H y ) = (/) -> ( ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) <-> ( x G y ) : (/) -onto-> ( ( F ` x ) J ( F ` y ) ) ) )
8 fo00 
 |-  ( ( x G y ) : (/) -onto-> ( ( F ` x ) J ( F ` y ) ) <-> ( ( x G y ) = (/) /\ ( ( F ` x ) J ( F ` y ) ) = (/) ) )
9 8 simprbi 
 |-  ( ( x G y ) : (/) -onto-> ( ( F ` x ) J ( F ` y ) ) -> ( ( F ` x ) J ( F ` y ) ) = (/) )
10 7 9 biimtrdi 
 |-  ( ( x H y ) = (/) -> ( ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) )
11 10 com12 
 |-  ( ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) -> ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) )
12 11 2ralimi 
 |-  ( A. x e. B A. y e. B ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) -> A. x e. B A. y e. B ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) )
13 6 12 simplbiim 
 |-  ( F ( C Full D ) G -> A. x e. B A. y e. B ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) )
14 13 adantl 
 |-  ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ F ( C Full D ) G ) -> A. x e. B A. y e. B ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) )
15 simplr 
 |-  ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ A. x e. B A. y e. B ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) ) -> F ( C Func D ) G )
16 imor 
 |-  ( ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) <-> ( -. ( x H y ) = (/) \/ ( ( F ` x ) J ( F ` y ) ) = (/) ) )
17 simplr 
 |-  ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) -> F ( C Func D ) G )
18 simprl 
 |-  ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) -> x e. B )
19 simprr 
 |-  ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) -> y e. B )
20 1 3 2 17 18 19 funcf2 
 |-  ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) -> ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) )
21 20 adantr 
 |-  ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) )
22 simpr 
 |-  ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> -. ( x H y ) = (/) )
23 22 neqned 
 |-  ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> ( x H y ) =/= (/) )
24 fdomne0 
 |-  ( ( ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) /\ ( x H y ) =/= (/) ) -> ( ( x G y ) =/= (/) /\ ( ( F ` x ) J ( F ` y ) ) =/= (/) ) )
25 21 23 24 syl2anc 
 |-  ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> ( ( x G y ) =/= (/) /\ ( ( F ` x ) J ( F ` y ) ) =/= (/) ) )
26 25 simprd 
 |-  ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> ( ( F ` x ) J ( F ` y ) ) =/= (/) )
27 simplll 
 |-  ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> D e. ThinCat )
28 eqid 
 |-  ( Base ` D ) = ( Base ` D )
29 17 adantr 
 |-  ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> F ( C Func D ) G )
30 1 28 29 funcf1 
 |-  ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> F : B --> ( Base ` D ) )
31 18 adantr 
 |-  ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> x e. B )
32 30 31 ffvelcdmd 
 |-  ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> ( F ` x ) e. ( Base ` D ) )
33 19 adantr 
 |-  ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> y e. B )
34 30 33 ffvelcdmd 
 |-  ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> ( F ` y ) e. ( Base ` D ) )
35 eqidd 
 |-  ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> ( Base ` D ) = ( Base ` D ) )
36 2 a1i 
 |-  ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> J = ( Hom ` D ) )
37 27 32 34 35 36 thincn0eu 
 |-  ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> ( ( ( F ` x ) J ( F ` y ) ) =/= (/) <-> E! f f e. ( ( F ` x ) J ( F ` y ) ) ) )
38 26 37 mpbid 
 |-  ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> E! f f e. ( ( F ` x ) J ( F ` y ) ) )
39 eusn 
 |-  ( E! f f e. ( ( F ` x ) J ( F ` y ) ) <-> E. f ( ( F ` x ) J ( F ` y ) ) = { f } )
40 38 39 sylib 
 |-  ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> E. f ( ( F ` x ) J ( F ` y ) ) = { f } )
41 25 simpld 
 |-  ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> ( x G y ) =/= (/) )
42 foconst 
 |-  ( ( ( x G y ) : ( x H y ) --> { f } /\ ( x G y ) =/= (/) ) -> ( x G y ) : ( x H y ) -onto-> { f } )
43 feq3 
 |-  ( ( ( F ` x ) J ( F ` y ) ) = { f } -> ( ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) <-> ( x G y ) : ( x H y ) --> { f } ) )
44 43 anbi1d 
 |-  ( ( ( F ` x ) J ( F ` y ) ) = { f } -> ( ( ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) /\ ( x G y ) =/= (/) ) <-> ( ( x G y ) : ( x H y ) --> { f } /\ ( x G y ) =/= (/) ) ) )
45 foeq3 
 |-  ( ( ( F ` x ) J ( F ` y ) ) = { f } -> ( ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) <-> ( x G y ) : ( x H y ) -onto-> { f } ) )
46 44 45 imbi12d 
 |-  ( ( ( F ` x ) J ( F ` y ) ) = { f } -> ( ( ( ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) /\ ( x G y ) =/= (/) ) -> ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) ) <-> ( ( ( x G y ) : ( x H y ) --> { f } /\ ( x G y ) =/= (/) ) -> ( x G y ) : ( x H y ) -onto-> { f } ) ) )
47 42 46 mpbiri 
 |-  ( ( ( F ` x ) J ( F ` y ) ) = { f } -> ( ( ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) /\ ( x G y ) =/= (/) ) -> ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) ) )
48 47 exlimiv 
 |-  ( E. f ( ( F ` x ) J ( F ` y ) ) = { f } -> ( ( ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) /\ ( x G y ) =/= (/) ) -> ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) ) )
49 48 imp 
 |-  ( ( E. f ( ( F ` x ) J ( F ` y ) ) = { f } /\ ( ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) /\ ( x G y ) =/= (/) ) ) -> ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) )
50 40 21 41 49 syl12anc 
 |-  ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x H y ) = (/) ) -> ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) )
51 20 adantr 
 |-  ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ ( ( F ` x ) J ( F ` y ) ) = (/) ) -> ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) )
52 feq3 
 |-  ( ( ( F ` x ) J ( F ` y ) ) = (/) -> ( ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) <-> ( x G y ) : ( x H y ) --> (/) ) )
53 52 adantl 
 |-  ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ ( ( F ` x ) J ( F ` y ) ) = (/) ) -> ( ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) <-> ( x G y ) : ( x H y ) --> (/) ) )
54 51 53 mpbid 
 |-  ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ ( ( F ` x ) J ( F ` y ) ) = (/) ) -> ( x G y ) : ( x H y ) --> (/) )
55 f00 
 |-  ( ( x G y ) : ( x H y ) --> (/) <-> ( ( x G y ) = (/) /\ ( x H y ) = (/) ) )
56 54 55 sylib 
 |-  ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ ( ( F ` x ) J ( F ` y ) ) = (/) ) -> ( ( x G y ) = (/) /\ ( x H y ) = (/) ) )
57 56 simprd 
 |-  ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ ( ( F ` x ) J ( F ` y ) ) = (/) ) -> ( x H y ) = (/) )
58 56 simpld 
 |-  ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ ( ( F ` x ) J ( F ` y ) ) = (/) ) -> ( x G y ) = (/) )
59 simpr 
 |-  ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ ( ( F ` x ) J ( F ` y ) ) = (/) ) -> ( ( F ` x ) J ( F ` y ) ) = (/) )
60 8 biimpri 
 |-  ( ( ( x G y ) = (/) /\ ( ( F ` x ) J ( F ` y ) ) = (/) ) -> ( x G y ) : (/) -onto-> ( ( F ` x ) J ( F ` y ) ) )
61 60 7 imbitrrid 
 |-  ( ( x H y ) = (/) -> ( ( ( x G y ) = (/) /\ ( ( F ` x ) J ( F ` y ) ) = (/) ) -> ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) ) )
62 61 imp 
 |-  ( ( ( x H y ) = (/) /\ ( ( x G y ) = (/) /\ ( ( F ` x ) J ( F ` y ) ) = (/) ) ) -> ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) )
63 57 58 59 62 syl12anc 
 |-  ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ ( ( F ` x ) J ( F ` y ) ) = (/) ) -> ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) )
64 50 63 jaodan 
 |-  ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ ( -. ( x H y ) = (/) \/ ( ( F ` x ) J ( F ` y ) ) = (/) ) ) -> ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) )
65 16 64 sylan2b 
 |-  ( ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) /\ ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) ) -> ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) )
66 65 ex 
 |-  ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ ( x e. B /\ y e. B ) ) -> ( ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) -> ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) ) )
67 66 ralimdvva 
 |-  ( ( D e. ThinCat /\ F ( C Func D ) G ) -> ( A. x e. B A. y e. B ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) -> A. x e. B A. y e. B ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) ) )
68 67 imp 
 |-  ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ A. x e. B A. y e. B ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) ) -> A. x e. B A. y e. B ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) )
69 15 68 6 sylanbrc 
 |-  ( ( ( D e. ThinCat /\ F ( C Func D ) G ) /\ A. x e. B A. y e. B ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) ) -> F ( C Full D ) G )
70 14 69 impbida 
 |-  ( ( D e. ThinCat /\ F ( C Func D ) G ) -> ( F ( C Full D ) G <-> A. x e. B A. y e. B ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) ) )
71 4 5 70 syl2anc 
 |-  ( ph -> ( F ( C Full D ) G <-> A. x e. B A. y e. B ( ( x H y ) = (/) -> ( ( F ` x ) J ( F ` y ) ) = (/) ) ) )