Metamath Proof Explorer

Theorem resccat

Description: A class C restricted by the hom-sets of another set E , whose base is a subset of the base of C and whose composition is compatible with C , is a category iff E is a category. Note that the compatibility condition "resccat.1" can be weakened by removing x e. S because f e. ( x J y ) implies these. (Contributed by Zhi Wang, 6-Nov-2025)

Ref Expression
Hypotheses resccat.d 
|- D = ( C |`cat J )
resccat.b 
|- B = ( Base ` C )
resccat.s 
|- S = ( Base ` E )
resccat.j 
|- J = ( Homf ` E )
resccat.x 
|- .x. = ( comp ` C )
resccat.xb 
|- .xb = ( comp ` E )
resccat.1 
|- ( ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) -> ( g ( <. x , y >. .x. z ) f ) = ( g ( <. x , y >. .xb z ) f ) )
resccat.e 
|- ( ph -> E e. V )
resccat.ss 
|- ( ph -> S C_ B )
Assertion resccat 
|- ( ph -> ( D e. Cat <-> E e. Cat ) )

Proof

Step Hyp Ref Expression
1 resccat.d 
 |-  D = ( C |`cat J )
2 resccat.b 
 |-  B = ( Base ` C )
3 resccat.s 
 |-  S = ( Base ` E )
4 resccat.j 
 |-  J = ( Homf ` E )
5 resccat.x 
 |-  .x. = ( comp ` C )
6 resccat.xb 
 |-  .xb = ( comp ` E )
7 resccat.1 
 |-  ( ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) -> ( g ( <. x , y >. .x. z ) f ) = ( g ( <. x , y >. .xb z ) f ) )
8 resccat.e 
 |-  ( ph -> E e. V )
9 resccat.ss 
 |-  ( ph -> S C_ B )
10 7 adantllr 
 |-  ( ( ( ( ph /\ C e. _V ) /\ ( x e. S /\ y e. S /\ z e. S ) ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) -> ( g ( <. x , y >. .x. z ) f ) = ( g ( <. x , y >. .xb z ) f ) )
11 8 adantr 
 |-  ( ( ph /\ C e. _V ) -> E e. V )
12 9 adantr 
 |-  ( ( ph /\ C e. _V ) -> S C_ B )
13 simpr 
 |-  ( ( ph /\ C e. _V ) -> C e. _V )
14 1 2 3 4 5 6 10 11 12 13 resccatlem 
 |-  ( ( ph /\ C e. _V ) -> ( D e. Cat <-> E e. Cat ) )
15 df-resc 
 |-  |`cat = ( c e. _V , h e. _V |-> ( ( c |`s dom dom h ) sSet <. ( Hom ` ndx ) , h >. ) )
16 15 reldmmpo 
 |-  Rel dom |`cat
17 16 ovprc1 
 |-  ( -. C e. _V -> ( C |`cat J ) = (/) )
18 1 17 eqtrid 
 |-  ( -. C e. _V -> D = (/) )
19 0cat 
 |-  (/) e. Cat
20 18 19 eqeltrdi 
 |-  ( -. C e. _V -> D e. Cat )
21 20 adantl 
 |-  ( ( ph /\ -. C e. _V ) -> D e. Cat )
22 fvprc 
 |-  ( -. C e. _V -> ( Base ` C ) = (/) )
23 2 22 eqtrid 
 |-  ( -. C e. _V -> B = (/) )
24 sseq0 
 |-  ( ( S C_ B /\ B = (/) ) -> S = (/) )
25 9 23 24 syl2an 
 |-  ( ( ph /\ -. C e. _V ) -> S = (/) )
26 25 3 eqtr3di 
 |-  ( ( ph /\ -. C e. _V ) -> (/) = ( Base ` E ) )
27 0catg 
 |-  ( ( E e. V /\ (/) = ( Base ` E ) ) -> E e. Cat )
28 8 26 27 syl2an2r 
 |-  ( ( ph /\ -. C e. _V ) -> E e. Cat )
29 21 28 2thd 
 |-  ( ( ph /\ -. C e. _V ) -> ( D e. Cat <-> E e. Cat ) )
30 14 29 pm2.61dan 
 |-  ( ph -> ( D e. Cat <-> E e. Cat ) )