Metamath Proof Explorer

Theorem fullresc

Description: The category formed by structure restriction is the same as the category restriction. (Contributed by Mario Carneiro, 5-Jan-2017)

Ref Expression
Hypotheses fullsubc.b 
|- B = ( Base ` C )
fullsubc.h 
|- H = ( Homf ` C )
fullsubc.c 
|- ( ph -> C e. Cat )
fullsubc.s 
|- ( ph -> S C_ B )
fullsubc.d 
|- D = ( C |`s S )
fullsubc.e 
|- E = ( C |`cat ( H |` ( S X. S ) ) )
Assertion fullresc 
|- ( ph -> ( ( Homf ` D ) = ( Homf ` E ) /\ ( comf ` D ) = ( comf ` E ) ) )

Proof

Step Hyp Ref Expression
1 fullsubc.b 
 |-  B = ( Base ` C )
2 fullsubc.h 
 |-  H = ( Homf ` C )
3 fullsubc.c 
 |-  ( ph -> C e. Cat )
4 fullsubc.s 
 |-  ( ph -> S C_ B )
5 fullsubc.d 
 |-  D = ( C |`s S )
6 fullsubc.e 
 |-  E = ( C |`cat ( H |` ( S X. S ) ) )
7 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
8 4 adantr 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> S C_ B )
9 simprl 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> x e. S )
10 8 9 sseldd 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> x e. B )
11 simprr 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> y e. S )
12 8 11 sseldd 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> y e. B )
13 2 1 7 10 12 homfval 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x H y ) = ( x ( Hom ` C ) y ) )
14 9 11 ovresd 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x ( H |` ( S X. S ) ) y ) = ( x H y ) )
15 2 1 homffn 
 |-  H Fn ( B X. B )
16 xpss12 
 |-  ( ( S C_ B /\ S C_ B ) -> ( S X. S ) C_ ( B X. B ) )
17 4 4 16 syl2anc 
 |-  ( ph -> ( S X. S ) C_ ( B X. B ) )
18 fnssres 
 |-  ( ( H Fn ( B X. B ) /\ ( S X. S ) C_ ( B X. B ) ) -> ( H |` ( S X. S ) ) Fn ( S X. S ) )
19 15 17 18 sylancr 
 |-  ( ph -> ( H |` ( S X. S ) ) Fn ( S X. S ) )
20 6 1 3 19 4 reschom 
 |-  ( ph -> ( H |` ( S X. S ) ) = ( Hom ` E ) )
21 20 oveqdr 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x ( H |` ( S X. S ) ) y ) = ( x ( Hom ` E ) y ) )
22 14 21 eqtr3d 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x H y ) = ( x ( Hom ` E ) y ) )
23 5 1 ressbas2 
 |-  ( S C_ B -> S = ( Base ` D ) )
24 4 23 syl 
 |-  ( ph -> S = ( Base ` D ) )
25 fvex 
 |-  ( Base ` D ) e. _V
26 24 25 eqeltrdi 
 |-  ( ph -> S e. _V )
27 5 7 resshom 
 |-  ( S e. _V -> ( Hom ` C ) = ( Hom ` D ) )
28 26 27 syl 
 |-  ( ph -> ( Hom ` C ) = ( Hom ` D ) )
29 28 oveqdr 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x ( Hom ` C ) y ) = ( x ( Hom ` D ) y ) )
30 13 22 29 3eqtr3rd 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x ( Hom ` D ) y ) = ( x ( Hom ` E ) y ) )
31 30 ralrimivva 
 |-  ( ph -> A. x e. S A. y e. S ( x ( Hom ` D ) y ) = ( x ( Hom ` E ) y ) )
32 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
33 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
34 6 1 3 19 4 rescbas 
 |-  ( ph -> S = ( Base ` E ) )
35 32 33 24 34 homfeq 
 |-  ( ph -> ( ( Homf ` D ) = ( Homf ` E ) <-> A. x e. S A. y e. S ( x ( Hom ` D ) y ) = ( x ( Hom ` E ) y ) ) )
36 31 35 mpbird 
 |-  ( ph -> ( Homf ` D ) = ( Homf ` E ) )
37 eqid 
 |-  ( comp ` C ) = ( comp ` C )
38 5 37 ressco 
 |-  ( S e. _V -> ( comp ` C ) = ( comp ` D ) )
39 26 38 syl 
 |-  ( ph -> ( comp ` C ) = ( comp ` D ) )
40 6 1 3 19 4 37 rescco 
 |-  ( ph -> ( comp ` C ) = ( comp ` E ) )
41 39 40 eqtr3d 
 |-  ( ph -> ( comp ` D ) = ( comp ` E ) )
42 41 36 comfeqd 
 |-  ( ph -> ( comf ` D ) = ( comf ` E ) )
43 36 42 jca 
 |-  ( ph -> ( ( Homf ` D ) = ( Homf ` E ) /\ ( comf ` D ) = ( comf ` E ) ) )