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 df-ss
 |-  ( 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 ) ) )