Metamath Proof Explorer

Theorem resccatlem

Description: Lemma for resccat . (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 )
resccatlem.c 
|- ( ph -> C e. U )
Assertion resccatlem 
|- ( 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 resccatlem.c 
 |-  ( ph -> C e. U )
11 4 3 homffn 
 |-  J Fn ( S X. S )
12 11 a1i 
 |-  ( ph -> J Fn ( S X. S ) )
13 1 2 10 12 9 reschomf 
 |-  ( ph -> J = ( Homf ` D ) )
14 13 4 eqtr3di 
 |-  ( ph -> ( Homf ` D ) = ( Homf ` E ) )
15 7 ralrimivva 
 |-  ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. .x. z ) f ) = ( g ( <. x , y >. .xb z ) f ) )
16 15 ralrimivvva 
 |-  ( ph -> A. x e. S A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. .x. z ) f ) = ( g ( <. x , y >. .xb z ) f ) )
17 eqid 
 |-  ( comp ` D ) = ( comp ` D )
18 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
19 1 2 10 12 9 rescbas 
 |-  ( ph -> S = ( Base ` D ) )
20 3 a1i 
 |-  ( ph -> S = ( Base ` E ) )
21 17 6 18 19 20 14 comfeq 
 |-  ( ph -> ( ( comf ` D ) = ( comf ` E ) <-> A. x e. S A. y e. S A. z e. S A. f e. ( x ( Hom ` D ) y ) A. g e. ( y ( Hom ` D ) z ) ( g ( <. x , y >. ( comp ` D ) z ) f ) = ( g ( <. x , y >. .xb z ) f ) ) )
22 1 2 10 12 9 reschom 
 |-  ( ph -> J = ( Hom ` D ) )
23 22 oveqd 
 |-  ( ph -> ( x J y ) = ( x ( Hom ` D ) y ) )
24 22 oveqd 
 |-  ( ph -> ( y J z ) = ( y ( Hom ` D ) z ) )
25 1 2 10 12 9 5 rescco 
 |-  ( ph -> .x. = ( comp ` D ) )
26 25 oveqd 
 |-  ( ph -> ( <. x , y >. .x. z ) = ( <. x , y >. ( comp ` D ) z ) )
27 26 oveqd 
 |-  ( ph -> ( g ( <. x , y >. .x. z ) f ) = ( g ( <. x , y >. ( comp ` D ) z ) f ) )
28 27 eqeq1d 
 |-  ( ph -> ( ( g ( <. x , y >. .x. z ) f ) = ( g ( <. x , y >. .xb z ) f ) <-> ( g ( <. x , y >. ( comp ` D ) z ) f ) = ( g ( <. x , y >. .xb z ) f ) ) )
29 24 28 raleqbidv 
 |-  ( ph -> ( A. g e. ( y J z ) ( g ( <. x , y >. .x. z ) f ) = ( g ( <. x , y >. .xb z ) f ) <-> A. g e. ( y ( Hom ` D ) z ) ( g ( <. x , y >. ( comp ` D ) z ) f ) = ( g ( <. x , y >. .xb z ) f ) ) )
30 23 29 raleqbidv 
 |-  ( ph -> ( A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. .x. z ) f ) = ( g ( <. x , y >. .xb z ) f ) <-> A. f e. ( x ( Hom ` D ) y ) A. g e. ( y ( Hom ` D ) z ) ( g ( <. x , y >. ( comp ` D ) z ) f ) = ( g ( <. x , y >. .xb z ) f ) ) )
31 30 3ralbidv 
 |-  ( ph -> ( A. x e. S A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. .x. z ) f ) = ( g ( <. x , y >. .xb z ) f ) <-> A. x e. S A. y e. S A. z e. S A. f e. ( x ( Hom ` D ) y ) A. g e. ( y ( Hom ` D ) z ) ( g ( <. x , y >. ( comp ` D ) z ) f ) = ( g ( <. x , y >. .xb z ) f ) ) )
32 21 31 bitr4d 
 |-  ( ph -> ( ( comf ` D ) = ( comf ` E ) <-> A. x e. S A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. .x. z ) f ) = ( g ( <. x , y >. .xb z ) f ) ) )
33 16 32 mpbird 
 |-  ( ph -> ( comf ` D ) = ( comf ` E ) )
34 1 ovexi 
 |-  D e. _V
35 34 a1i 
 |-  ( ph -> D e. _V )
36 14 33 35 8 catpropd 
 |-  ( ph -> ( D e. Cat <-> E e. Cat ) )