Metamath Proof Explorer

Theorem resscatc

Description: The restriction of the category of categories to a subset is the category of categories in the subset. Thus, the CatCatU categories for different U are full subcategories of each other. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses resscatc.c 
|- C = ( CatCat ` U )
resscatc.d 
|- D = ( CatCat ` V )
resscatc.1 
|- ( ph -> U e. W )
resscatc.2 
|- ( ph -> V C_ U )
Assertion resscatc 
|- ( ph -> ( ( Homf ` ( C |`s V ) ) = ( Homf ` D ) /\ ( comf ` ( C |`s V ) ) = ( comf ` D ) ) )

Proof

Step Hyp Ref Expression
1 resscatc.c 
 |-  C = ( CatCat ` U )
2 resscatc.d 
 |-  D = ( CatCat ` V )
3 resscatc.1 
 |-  ( ph -> U e. W )
4 resscatc.2 
 |-  ( ph -> V C_ U )
5 eqid 
 |-  ( Base ` D ) = ( Base ` D )
6 3 4 ssexd 
 |-  ( ph -> V e. _V )
7 6 adantr 
 |-  ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) ) ) -> V e. _V )
8 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
9 simprl 
 |-  ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) ) ) -> x e. ( V i^i Cat ) )
10 2 5 6 catcbas 
 |-  ( ph -> ( Base ` D ) = ( V i^i Cat ) )
11 10 adantr 
 |-  ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) ) ) -> ( Base ` D ) = ( V i^i Cat ) )
12 9 11 eleqtrrd 
 |-  ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) ) ) -> x e. ( Base ` D ) )
13 simprr 
 |-  ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) ) ) -> y e. ( V i^i Cat ) )
14 13 11 eleqtrrd 
 |-  ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) ) ) -> y e. ( Base ` D ) )
15 2 5 7 8 12 14 catchom 
 |-  ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) ) ) -> ( x ( Hom ` D ) y ) = ( x Func y ) )
16 eqid 
 |-  ( Base ` C ) = ( Base ` C )
17 3 adantr 
 |-  ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) ) ) -> U e. W )
18 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
19 inass 
 |-  ( ( V i^i U ) i^i Cat ) = ( V i^i ( U i^i Cat ) )
20 1 16 3 catcbas 
 |-  ( ph -> ( Base ` C ) = ( U i^i Cat ) )
21 20 ineq2d 
 |-  ( ph -> ( V i^i ( Base ` C ) ) = ( V i^i ( U i^i Cat ) ) )
22 19 21 eqtr4id 
 |-  ( ph -> ( ( V i^i U ) i^i Cat ) = ( V i^i ( Base ` C ) ) )
23 dfss2 
 |-  ( V C_ U <-> ( V i^i U ) = V )
24 4 23 sylib 
 |-  ( ph -> ( V i^i U ) = V )
25 24 ineq1d 
 |-  ( ph -> ( ( V i^i U ) i^i Cat ) = ( V i^i Cat ) )
26 eqid 
 |-  ( C |`s V ) = ( C |`s V )
27 26 16 ressbas 
 |-  ( V e. _V -> ( V i^i ( Base ` C ) ) = ( Base ` ( C |`s V ) ) )
28 6 27 syl 
 |-  ( ph -> ( V i^i ( Base ` C ) ) = ( Base ` ( C |`s V ) ) )
29 22 25 28 3eqtr3d 
 |-  ( ph -> ( V i^i Cat ) = ( Base ` ( C |`s V ) ) )
30 26 16 ressbasss 
 |-  ( Base ` ( C |`s V ) ) C_ ( Base ` C )
31 29 30 eqsstrdi 
 |-  ( ph -> ( V i^i Cat ) C_ ( Base ` C ) )
32 31 adantr 
 |-  ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) ) ) -> ( V i^i Cat ) C_ ( Base ` C ) )
33 32 9 sseldd 
 |-  ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) ) ) -> x e. ( Base ` C ) )
34 32 13 sseldd 
 |-  ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) ) ) -> y e. ( Base ` C ) )
35 1 16 17 18 33 34 catchom 
 |-  ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) ) ) -> ( x ( Hom ` C ) y ) = ( x Func y ) )
36 26 18 resshom 
 |-  ( V e. _V -> ( Hom ` C ) = ( Hom ` ( C |`s V ) ) )
37 6 36 syl 
 |-  ( ph -> ( Hom ` C ) = ( Hom ` ( C |`s V ) ) )
38 37 oveqdr 
 |-  ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) ) ) -> ( x ( Hom ` C ) y ) = ( x ( Hom ` ( C |`s V ) ) y ) )
39 15 35 38 3eqtr2rd 
 |-  ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) ) ) -> ( x ( Hom ` ( C |`s V ) ) y ) = ( x ( Hom ` D ) y ) )
40 39 ralrimivva 
 |-  ( ph -> A. x e. ( V i^i Cat ) A. y e. ( V i^i Cat ) ( x ( Hom ` ( C |`s V ) ) y ) = ( x ( Hom ` D ) y ) )
41 eqid 
 |-  ( Hom ` ( C |`s V ) ) = ( Hom ` ( C |`s V ) )
42 10 eqcomd 
 |-  ( ph -> ( V i^i Cat ) = ( Base ` D ) )
43 41 8 29 42 homfeq 
 |-  ( ph -> ( ( Homf ` ( C |`s V ) ) = ( Homf ` D ) <-> A. x e. ( V i^i Cat ) A. y e. ( V i^i Cat ) ( x ( Hom ` ( C |`s V ) ) y ) = ( x ( Hom ` D ) y ) ) )
44 40 43 mpbird 
 |-  ( ph -> ( Homf ` ( C |`s V ) ) = ( Homf ` D ) )
45 6 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) /\ z e. ( V i^i Cat ) ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> V e. _V )
46 eqid 
 |-  ( comp ` D ) = ( comp ` D )
47 simplr1 
 |-  ( ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) /\ z e. ( V i^i Cat ) ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> x e. ( V i^i Cat ) )
48 10 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) /\ z e. ( V i^i Cat ) ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> ( Base ` D ) = ( V i^i Cat ) )
49 47 48 eleqtrrd 
 |-  ( ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) /\ z e. ( V i^i Cat ) ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> x e. ( Base ` D ) )
50 simplr2 
 |-  ( ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) /\ z e. ( V i^i Cat ) ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> y e. ( V i^i Cat ) )
51 50 48 eleqtrrd 
 |-  ( ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) /\ z e. ( V i^i Cat ) ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> y e. ( Base ` D ) )
52 simplr3 
 |-  ( ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) /\ z e. ( V i^i Cat ) ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> z e. ( V i^i Cat ) )
53 52 48 eleqtrrd 
 |-  ( ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) /\ z e. ( V i^i Cat ) ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> z e. ( Base ` D ) )
54 simprl 
 |-  ( ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) /\ z e. ( V i^i Cat ) ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> f e. ( x ( Hom ` D ) y ) )
55 2 5 45 8 49 51 catchom 
 |-  ( ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) /\ z e. ( V i^i Cat ) ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> ( x ( Hom ` D ) y ) = ( x Func y ) )
56 54 55 eleqtrd 
 |-  ( ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) /\ z e. ( V i^i Cat ) ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> f e. ( x Func y ) )
57 simprr 
 |-  ( ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) /\ z e. ( V i^i Cat ) ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> g e. ( y ( Hom ` D ) z ) )
58 2 5 45 8 51 53 catchom 
 |-  ( ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) /\ z e. ( V i^i Cat ) ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> ( y ( Hom ` D ) z ) = ( y Func z ) )
59 57 58 eleqtrd 
 |-  ( ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) /\ z e. ( V i^i Cat ) ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> g e. ( y Func z ) )
60 2 5 45 46 49 51 53 56 59 catcco 
 |-  ( ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) /\ z e. ( V i^i Cat ) ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> ( g ( <. x , y >. ( comp ` D ) z ) f ) = ( g o.func f ) )
61 3 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) /\ z e. ( V i^i Cat ) ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> U e. W )
62 eqid 
 |-  ( comp ` C ) = ( comp ` C )
63 31 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) /\ z e. ( V i^i Cat ) ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> ( V i^i Cat ) C_ ( Base ` C ) )
64 63 47 sseldd 
 |-  ( ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) /\ z e. ( V i^i Cat ) ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> x e. ( Base ` C ) )
65 63 50 sseldd 
 |-  ( ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) /\ z e. ( V i^i Cat ) ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> y e. ( Base ` C ) )
66 63 52 sseldd 
 |-  ( ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) /\ z e. ( V i^i Cat ) ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> z e. ( Base ` C ) )
67 1 16 61 62 64 65 66 56 59 catcco 
 |-  ( ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) /\ z e. ( V i^i Cat ) ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> ( g ( <. x , y >. ( comp ` C ) z ) f ) = ( g o.func f ) )
68 26 62 ressco 
 |-  ( V e. _V -> ( comp ` C ) = ( comp ` ( C |`s V ) ) )
69 6 68 syl 
 |-  ( ph -> ( comp ` C ) = ( comp ` ( C |`s V ) ) )
70 69 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) /\ z e. ( V i^i Cat ) ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> ( comp ` C ) = ( comp ` ( C |`s V ) ) )
71 70 oveqd 
 |-  ( ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) /\ z e. ( V i^i Cat ) ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> ( <. x , y >. ( comp ` C ) z ) = ( <. x , y >. ( comp ` ( C |`s V ) ) z ) )
72 71 oveqd 
 |-  ( ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) /\ z e. ( V i^i Cat ) ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> ( g ( <. x , y >. ( comp ` C ) z ) f ) = ( g ( <. x , y >. ( comp ` ( C |`s V ) ) z ) f ) )
73 60 67 72 3eqtr2d 
 |-  ( ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) /\ z e. ( V i^i Cat ) ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> ( g ( <. x , y >. ( comp ` D ) z ) f ) = ( g ( <. x , y >. ( comp ` ( C |`s V ) ) z ) f ) )
74 73 ralrimivva 
 |-  ( ( ph /\ ( x e. ( V i^i Cat ) /\ y e. ( V i^i Cat ) /\ z e. ( V i^i Cat ) ) ) -> A. f e. ( x ( Hom ` D ) y ) A. g e. ( y ( Hom ` D ) z ) ( g ( <. x , y >. ( comp ` D ) z ) f ) = ( g ( <. x , y >. ( comp ` ( C |`s V ) ) z ) f ) )
75 74 ralrimivvva 
 |-  ( ph -> A. x e. ( V i^i Cat ) A. y e. ( V i^i Cat ) A. z e. ( V i^i Cat ) A. f e. ( x ( Hom ` D ) y ) A. g e. ( y ( Hom ` D ) z ) ( g ( <. x , y >. ( comp ` D ) z ) f ) = ( g ( <. x , y >. ( comp ` ( C |`s V ) ) z ) f ) )
76 eqid 
 |-  ( comp ` ( C |`s V ) ) = ( comp ` ( C |`s V ) )
77 44 eqcomd 
 |-  ( ph -> ( Homf ` D ) = ( Homf ` ( C |`s V ) ) )
78 46 76 8 42 29 77 comfeq 
 |-  ( ph -> ( ( comf ` D ) = ( comf ` ( C |`s V ) ) <-> A. x e. ( V i^i Cat ) A. y e. ( V i^i Cat ) A. z e. ( V i^i Cat ) A. f e. ( x ( Hom ` D ) y ) A. g e. ( y ( Hom ` D ) z ) ( g ( <. x , y >. ( comp ` D ) z ) f ) = ( g ( <. x , y >. ( comp ` ( C |`s V ) ) z ) f ) ) )
79 75 78 mpbird 
 |-  ( ph -> ( comf ` D ) = ( comf ` ( C |`s V ) ) )
80 79 eqcomd 
 |-  ( ph -> ( comf ` ( C |`s V ) ) = ( comf ` D ) )
81 44 80 jca 
 |-  ( ph -> ( ( Homf ` ( C |`s V ) ) = ( Homf ` D ) /\ ( comf ` ( C |`s V ) ) = ( comf ` D ) ) )